Core #
Geometry and verified arithmetic for the Conway–Soifer covering theorem at n = 3.
theorem
ConwaySoifer.Simplified.core_exclusion
{u : ℝ}
(hu0 : 0 < u)
(hu : u ≤ 1 / 2)
(i j : Fin 6)
{Q : EquilateralTriangle}
(hQ : 0 < Q.side)
(hQ1 : Q.side < 1)
(hv : vertex i ∈ Q.carrier)
(hp : linePoint (vertex i) (sideDirection i false) u ∈ Q.carrier)
(hn : linePoint (vertex i) (sideDirection i true) u ∈ Q.carrier)
(hk : coreVertex u j ∈ Q.carrier)
:
Adaptive-core exclusion, for every side owner and every core vertex.