AcrossArea

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

def ConwaySoifer.Simplified.acrossTop : Set Point

A fixed triangular region used in the Across area-budget obstruction.

Equations

• ConwaySoifer.Simplified.acrossTop = (convexHull ℝ) {(1, -1), (217 / 240, -217 / 240), (197 / 220, -1)}

theorem ConwaySoifer.Simplified.acrossTop_mem {p : Point} (hy : 1 ≤ locY p) (hh : locY p ≤ 1 + locX p) (hx : locX p ≤ 1 / 80 + locY p / 12) : p ∈ acrossTop

theorem ConwaySoifer.Simplified.volume_acrossTop : MeasureTheory.volume acrossTop = ENNReal.ofReal (529 / 105600)

theorem ConwaySoifer.Simplified.across_inter_small {T : Configuration} {r s : ℝ} (H : Canonical ContactCase.Across T r s) (hs : s ≤ 1 / 80) (hc : 12 * s ≤ rayLen (T 1) (vertex 0) upDir) : 2 * (MeasureTheory.volume ((T 1).carrier ∩ hexagon)).toReal ≤ 2083 / 17600

Exact quadrilateral enclosure, split into its lower trapezoid and upper triangle.

theorem ConwaySoifer.Simplified.across_ext_small {T : Configuration} {r s : ℝ} (H : Canonical ContactCase.Across T r s) (hs : s ≤ 1 / 80) : rayLen (T 1) (vertex 0) upDir < 12 * s