AownArea

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

def ConwaySoifer.Simplified.capRegion (s Y : ℝ) : Set Point

The region containing S₀ ∩ H.

Equations

• One or more equations did not get rendered due to their size.

def ConwaySoifer.Simplified.capBox (s Y : ℝ) : Set (ℝ × ℝ)

The same region in the coordinates (x, y).

Equations

• ConwaySoifer.Simplified.capBox s Y = {q : ℝ × ℝ | 0 ≤ q.2 ∧ q.2 ≤ Y ∧ 0 ≤ q.1 ∧ q.1 ≤ 2 * s * (q.2 + 1 / 2)}

theorem ConwaySoifer.Simplified.isClosed_capBox (s Y : ℝ) : IsClosed (capBox s Y)

theorem ConwaySoifer.Simplified.capBox_section (s Y y : ℝ) : MeasureTheory.volume ((fun (x : ℝ) => (x, y)) ⁻¹' capBox s Y) = (Set.Icc 0 Y).indicator (fun (y : ℝ) => ENNReal.ofReal (2 * s * (y + 1 / 2))) y

theorem ConwaySoifer.Simplified.integral_cap (s Y : ℝ) : ∫ (y : ℝ) in 0..Y, 2 * s * (y + 1 / 2) = s * (Y + Y ^ 2)

theorem ConwaySoifer.Simplified.volume_capBox (s Y : ℝ) (hs : 0 ≤ s) (hY : 0 ≤ Y) : MeasureTheory.volume (capBox s Y) = ENNReal.ofReal (s * (Y + Y ^ 2))

theorem ConwaySoifer.Simplified.capRegion_eq_image (s Y : ℝ) : capRegion s Y = ⇑(areaTriMap (vertex 0) (sideDirection 0 true) (sideDirection 0 false)) '' capBox s Y

theorem ConwaySoifer.Simplified.volume_capRegion (s Y : ℝ) (hs : 0 ≤ s) (hY : 0 ≤ Y) : MeasureTheory.volume (capRegion s Y) = ENNReal.ofReal (s * (Y + Y ^ 2))

noncomputable def ConwaySoifer.Simplified.aownHeight (r : ℝ) : ℝ

The upper cutoff retains the dependence on the common side.

Equations

• ConwaySoifer.Simplified.aownHeight r = √(25 * r ^ 2 / 21) - 1 / 2

theorem ConwaySoifer.Simplified.aownHeight_nonneg {T : Configuration} {r s : ℝ} (H : Canonical ContactCase.Aown T r s) : 0 ≤ aownHeight r

theorem ConwaySoifer.Simplified.aown_cap_subset {T : Configuration} {r s : ℝ} (H : Canonical ContactCase.Aown T r s) (hs : s ≤ 1 / 10) : (T 1).carrier ∩ hexagon ⊆ capRegion s (aownHeight r)

theorem ConwaySoifer.Simplified.aown_cap {T : Configuration} {r s : ℝ} (H : Canonical ContactCase.Aown T r s) (hs : s ≤ 1 / 10) : 2 * (MeasureTheory.volume ((T 1).carrier ∩ hexagon)).toReal ≤ 50 * s / 21 * r ^ 2 - s / 2

The strengthened area cap from the third pass, in normalized area units.

theorem ConwaySoifer.Simplified.aown_loss_zero {T : Configuration} {r s : ℝ} (H : Canonical ContactCase.Aown T r s) (hs : s ≤ 1 / 10) : r ^ 2 - (50 * s / 21 * r ^ 2 - s / 2) ≤ sideLoss T 0

Loss of the minimum-section owner from the strengthened cap.

theorem ConwaySoifer.Simplified.aown_no_cost {T : Configuration} {r s : ℝ} (H : Canonical ContactCase.Aown T r s) (hs : s ≤ 1 / 10) (i : Fin 6) (hi : i ≠ 0) : sideLoss T i < r ^ 2 / 4

No other owner can have midpoint-sized loss on (0, 1/10].

theorem ConwaySoifer.Simplified.aown_strengthening {T : Configuration} {r s : ℝ} (H : Canonical ContactCase.Aown T r s) (hs : s ≤ 1 / 10) : SmallStrengthening ContactCase.Aown T r

The small-Aown strengthening holds through the new closed endpoint.