FullOwn #
Geometry and verified arithmetic for the Conway–Soifer covering theorem at n = 3.
theorem
ConwaySoifer.Simplified.full_own_obstruction
{Q : EquilateralTriangle}
{s c : ℝ}
(hs : 0 < s)
(hsc : s < c)
(hQ : 0 < Q.side)
(hv : vertex 0 ∈ Q.carrier)
(hu : (1, -s) ∈ Q.carrier)
(hq : (1, c) ∈ Q.carrier)
(hend : rayLen Q (vertex 0) (sideDirection 0 true) = s)
(hlo : c ^ 2 - c * s + s ^ 2 ≤ (c * (c + s)) ^ 2)
(hhi : 3 ≤ (2 * (c + s)) ^ 2)
:
A full minimal section restricts the face direction to a single cone. One fixed triple proves the side bound on both boundaries of that cone.