LocalSideCover #
Geometry and verified arithmetic for the Conway–Soifer covering theorem at n = 3.
theorem
ConwaySoifer.Simplified.local_side_cover_impossible
{s : ℝ}
(hs0 : 0 < s)
(hs : s ≤ 1 / 10)
(C : EquilateralTriangle)
(S : Fin 6 → EquilateralTriangle)
(hC0 : 0 < C.side)
(hC1 : C.side < 1)
(hS0 : 0 < (S 0).side)
(hS1 : ∀ (i : Fin 6), (S i).side < 1)
(hV : (1, 0) ∈ (S 0).carrier)
(hA : (1, -s) ∈ (S 0).carrier)
(hB : (s, 1 - s) ∈ (S 0).carrier)
(hmandatory : ∀ (i : Fin 5), otherMandatory s i ∈ (S ⟨↑i + 1, ⋯⟩).carrier)
(hO : 0 ∈ C.carrier)
(hK : ∀ (j : Fin 6), coreVertex s j ∈ C.carrier)
(hcover : ∀ (j : Fin 3), witness s j ∈ C.carrier ∨ ∃ (i : Fin 6), witness s j ∈ (S i).carrier)
:
The final three-witness argument, after boundary propagation has supplied one mandatory point for each of the five nonreceiving owners.