ProfileWitness #
Geometry and verified arithmetic for the Conway–Soifer covering theorem at n = 3.
theorem
ConwaySoifer.Simplified.profile_witness
{Q : EquilateralTriangle}
{s : ℝ}
(hs0 : 0 < s)
(hs : s ≤ 1 / 10)
(hq : 0 < Q.side)
(k : Fin 8)
(n : Fin 3)
(hw : (1, 1) ∈ Q.carrier)
(he : (1, (↑↑k + 1) * s / 4) ∈ Q.carrier)
(hf : (1 - ↑↑k * s / 4, 1) ∈ Q.carrier)
(hp : ((witness s n).2, (witness s n).1) ∈ Q.carrier)
: