Angle trisection

Load Eos

In[]:=
Needs["Eos`","EosLoader`"]
Eos3.7.1.1 (March 21,2023) running under Mathematica 13.2.0 for Mac OS X ARM (64-bit) (November 18, 2022) on Mon 27 Mar 2023 18:07:14.

Construction

In[]:=
EosSession["Angle trisector"];
In[]:=
MarkOff[];
In[]:=
NewOrigami[10]
Angle trisector: Step 1
Out[]=
In[]:=
ProofDocFormat["Construction","Subsection",1];
In[]:=
NewPoint["E"{7,10}]
Angle trisector: Step 1
Out[]=
In[]:=
HO["AE",Handle"D"]
Angle trisector: Step 2
Out[]=
In[]:=
Unfold[]
Angle trisector: Step 3
Out[]=
In[]:=
HO["A","D",Mark{"AD","BC"}]
Angle trisector: Step 4
Out[]=
In[]:=
Unfold[]
Angle trisector: Step 5
Out[]=
In[]:=
HO["A","F",Mark{"AD","BC"}]
Angle trisector: Step 6
Out[]=
In[]:=
Unfold[]
Angle trisector: Step 7
Out[]=
In[]:=
HO["F","AE","A","HI"]
Angle trisector: Step 7
Out[]=

,
,

In[]:=
HO[FoldLine3]
Angle trisector: Step 8
Out[]=
In[]:=
ProjectPoint[{"A","H"}]
Angle trisector: Step 8
Out[]=
〈J,K〉
In[]:=
Unfold[]
Angle trisector: Step 9
Out[]=
In[]:=
HO["AJ",Handle"B",MarkFalse]
Angle trisector: Step 10
Out[]=
In[]:=
Unfold[]
Angle trisector: Step 11
Out[]=

Verification