CentralWitnesses #
Geometry and verified arithmetic for the Conway–Soifer covering theorem at n = 3.
theorem
ConwaySoifer.Simplified.three_witness_central
{Q : EquilateralTriangle}
{s : ℝ}
(hs0 : 0 < s)
(hs : s ≤ 1 / 10)
(hQ : 0 < Q.side)
(h0 : 0 ∈ Q.carrier)
(hK : ∀ (j : Fin 6), coreVertex s j ∈ Q.carrier)
(hw : ∀ (j : Fin 3), witness s j ∈ Q.carrier)
:
The three new points, together with the already known adaptive core, force side at least one. No enlarged nine-point core is involved.