AownCut

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

noncomputable def ConwaySoifer.Simplified.aownCut (s : ℝ) : ℝ

The exact rational-function cut parameter used by the Aown large-range obstruction.

Equations

• ConwaySoifer.Simplified.aownCut s = (1 - s ^ 2) / (2 - s)

theorem ConwaySoifer.Simplified.aownCut_bounds {s : ℝ} (hs1 : s ≤ 11 / 25) : s < aownCut s ∧ aownCut s < 1

theorem ConwaySoifer.Simplified.aownCut_support {s : ℝ} (hs : 7 / 20 ≤ s) (hs1 : s ≤ 11 / 25) : 3 ≤ (2 * (aownCut s + s)) ^ 2 ∧ aownCut s ^ 2 - aownCut s * s + s ^ 2 ≤ (aownCut s * (aownCut s + s)) ^ 2