Receiver

Geometry and verified arithmetic for the Conway–Soifer covering theorem at n = 3.

theorem ConwaySoifer.Simplified.receiver_forbidden_segment {Q : EquilateralTriangle} {s x : ℝ} (hs0 : 0 < s) (hs : s ≤ 1 / 10) (hx : s < x) (hx1 : x ≤ 1 / 2) (hside : 0 < Q.side) (hV : (1, 0) ∈ Q.carrier) (hA : (1, -s) ∈ Q.carrier) (hB : (s, 1 - s) ∈ Q.carrier) (hP : (x, 1 - s - x) ∈ Q.carrier) : 1 ≤ Q.side

noncomputable def ConwaySoifer.Simplified.witness (s : ℝ) : Fin 3 → Point

The three mandatory receiver points for the local obstruction.

Equations

• ConwaySoifer.Simplified.witness s = ![((1 - 9 * s / 5) * (9 / 10), (1 - 9 * s / 5) * (1 / 10)), ((1 - s) * (2 / 5), (1 - s) * (3 / 5)), (1 / 2, 1 / 2 - s)]

theorem ConwaySoifer.Simplified.receiver_three_witnesses {Q : EquilateralTriangle} {s : ℝ} (hs0 : 0 < s) (hs : s ≤ 1 / 10) (hside : 0 < Q.side) (hV : (1, 0) ∈ Q.carrier) (hA : (1, -s) ∈ Q.carrier) (hB : (s, 1 - s) ∈ Q.carrier) (j : Fin 3) (hq : witness s j ∈ Q.carrier) : 1 ≤ Q.side

All three new witnesses are excluded from the receiving side triangle by the same corner-section lemma. The first uses one convex combination.