Regular Heptagon

Load Eos

In[]:=
<<EosLoader.wl
Eos3.8.0 (October 13,2024) running under Mathematica 14.1.0 for Mac OS X ARM (64-bit) (July 16, 2024) on Mon 14 Oct 2024 18:26:18.
This version is effective until March 31,2025.

Construction


Verification

In[]:=
Goal
∀
α∈Complexes
α  ToC["G","H"]-ToC["R","H"]0
2
α
 ToC["G","H"]-ToC["S","H"]==0∧​​
3
α
 ToC["G","H"]-ToC["T","H"]==0∧​​
4
α
ToC["G","H"]-ToC["Q","H"]==0∧​​
5
α
ToC["G","H"]-ToC["P","H"]==0∧​​
6
α
ToC["G","H"]-ToC["O","H"]==0;
In[]:=
??ToC
Regular Heptagon/Origami: Step 23
Out[]=
Symbol
ToC[v] converts Eos vector, point, GA 1-Vec to a complex number. ToC[p,o] converts Eos vector Vector[o,p] to complex number.
Attributes
{Locked,ReadProtected}
Full Name
Orikoto`ToC
​
In[]:=
Prove["Regular heptagon",TacticsSplit]
Proof is successful.
Regular Heptagon/Origami: Step 23
Out[]=
{Success,3.69539,
Regular heptagon.pdoc.nb
}
In[]:=
EndSession[];