Bridge #
Geometry and verified arithmetic for the Conway–Soifer covering theorem at n = 3.
theorem
ConwaySoifer.Simplified.bridge_exclusion
{u : ℝ}
(hu0 : 0 < u)
(hu : u ≤ 1 / 3)
(right : Bool)
{Q : EquilateralTriangle}
(hQ : 0 < Q.side)
(hQ1 : Q.side < 1)
(hk : ∀ (j : Fin 6), coreVertex u j ∈ Q.carrier)
(hp : linePoint (vertex 0) (sideDirection 0 right) (2 * u) ∈ Q.carrier)
:
The bridge in both directions at vertex zero, with no computed hypotheses.
theorem
ConwaySoifer.Simplified.bridge_all_exclusion
{u : ℝ}
(hu0 : 0 < u)
(hu : u ≤ 1 / 3)
(i : Fin 6)
(right : Bool)
{Q : EquilateralTriangle}
(hQ : 0 < Q.side)
(hQ1 : Q.side < 1)
(hk : ∀ (j : Fin 6), coreVertex u j ∈ Q.carrier)
(hp : linePoint (vertex i) (sideDirection i right) (2 * u) ∈ Q.carrier)
:
The bridge at all six vertices. Rotating a local triangle does not assume that a 60-degree rotation preserves the side-three target.