ThreeWitnesses

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

theorem ConwaySoifer.Simplified.quadratic_at_right {a b c s h : ℝ} (ha : 0 ≤ a) (hsh : s ≤ h) (hslope : 2 * a * h + b ≤ 0) : a * h ^ 2 + b * h + c ≤ a * s ^ 2 + b * s + c

An explicit quadratic decreases up to its right endpoint under this slope bound.

def ConwaySoifer.Simplified.otherMandatory (s : ℝ) : Fin 5 → Point

The five auxiliary mandatory points in the three-witness obstruction.

Equations

• ConwaySoifer.Simplified.otherMandatory s = ![(-1 + 2 * s, 1), (-1, 1), (-1, 0), (0, -1), (1 - s, -1)]

theorem ConwaySoifer.Simplified.witnesses_mem_hexagon {s : ℝ} (hs0 : 0 < s) (hs : s ≤ 1 / 10) (j : Fin 3) : witness s j ∈ hexagon

theorem ConwaySoifer.Simplified.witnesses_violate_profile {s c : ℝ} (hs0 : 0 < s) (hs : s ≤ 1 / 10) (hc0 : 0 ≤ c) (hc : c ≤ 2 * s) (j : Fin 3) : c * ((witness s j).1 - (witness s j).2) ≤ 1 - (witness s j).1 - (witness s j).2

theorem ConwaySoifer.Simplified.witnesses_far {s : ℝ} (hs : s ≤ 1 / 10) (i : Fin 5) (j : Fin 3) : 1 < sqDist (otherMandatory s i) (witness s j)

Fifteen diameter exclusions, each reduced to a decreasing quadratic.