§6: the strengthening of Aown for s ≤ 1/14

In local coordinates p = v₀ + x u + y v (u towards v₁, v towards v₅) the owner S₀ of an Aown cover satisfies 0 ≤ x ≤ 2 s (y + 1/2) on the hexagon (face inequality of the full endpoint together with M₀ = v₀ - v/2 ∈ S₀) and y < 3/5 (diameter with M₀), hence |S₀ ∩ H| ≤ (24/25) s in volume units. If another side owner were overfull or contained an external corner midpoint, the area budget would be violated for s ≤ 1/14.

Local coordinates at v₀

def ConwaySoifer.locX (p : Point) : ℝ

The first coefficient in local coordinates at the first hexagon vertex.

Equations

• ConwaySoifer.locX p = 1 - p.1

def ConwaySoifer.locY (p : Point) : ℝ

The second coefficient in local coordinates at the first hexagon vertex.

Equations

• ConwaySoifer.locY p = 1 - p.1 - p.2

theorem ConwaySoifer.loc_decomp (p : Point) : p = vertex 0 + locX p • sideDirection 0 true + locY p • sideDirection 0 false

theorem ConwaySoifer.extMid0_decomp : extMid0 = vertex 0 + 0 • sideDirection 0 true + (-1 / 2) • sideDirection 0 false

theorem ConwaySoifer.sqDist_extMid0 (p : Point) : sqDist p extMid0 = locX p ^ 2 - locX p * (locY p + 1 / 2) + (locY p + 1 / 2) ^ 2

def ConwaySoifer.aownRegion (s : ℝ) : Set Point

The region containing S₀ ∩ H.

Equations

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

def ConwaySoifer.aownBox (s : ℝ) : Set (ℝ × ℝ)

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

Equations

• ConwaySoifer.aownBox s = {q : ℝ × ℝ | 0 ≤ q.2 ∧ q.2 ≤ 3 / 5 ∧ 0 ≤ q.1 ∧ q.1 ≤ 2 * s * (q.2 + 1 / 2)}

theorem ConwaySoifer.isClosed_aownBox (s : ℝ) : IsClosed (aownBox s)

theorem ConwaySoifer.aownBox_section (s y : ℝ) : MeasureTheory.volume ((fun (x : ℝ) => (x, y)) ⁻¹' aownBox s) = (Set.Icc 0 (3 / 5)).indicator (fun (y : ℝ) => ENNReal.ofReal (2 * s * (y + 1 / 2))) y

theorem ConwaySoifer.integral_aown (s : ℝ) : ∫ (y : ℝ) in 0..3 / 5, 2 * s * (y + 1 / 2) = 24 * s / 25

theorem ConwaySoifer.volume_aownBox (s : ℝ) (hs : 0 ≤ s) : MeasureTheory.volume (aownBox s) = ENNReal.ofReal (24 * s / 25)

theorem ConwaySoifer.aownRegion_eq_image (s : ℝ) : aownRegion s = ⇑(areaTriMap (vertex 0) (sideDirection 0 true) (sideDirection 0 false)) '' aownBox s

theorem ConwaySoifer.volume_aownRegion (s : ℝ) (hs : 0 ≤ s) : MeasureTheory.volume (aownRegion s) = ENNReal.ofReal (24 * s / 25)

S₀ ∩ H lies in the region

theorem ConwaySoifer.Canonical.toMinAt {c : ContactCase} {T : Configuration} {r s : ℝ} (H : Canonical c T r s) : MinAt T r s 0 c.right

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

theorem ConwaySoifer.Canonical.aown_inter_le {T : Configuration} {r s : ℝ} (H : Canonical ContactCase.Aown T r s) (hs : s ≤ 1 / 10) : (MeasureTheory.volume ((T 1).carrier ∩ hexagon)).toReal ≤ 24 * s / 25

The budget

noncomputable def ConwaySoifer.sideLoss (T : Configuration) (i : Fin 6) : ℝ

Normalised loss of side owner i.

Equations

• ConwaySoifer.sideLoss T i = 2 * (MeasureTheory.volume ((T (ConwaySoifer.sideIndex i)).carrier \ ConwaySoifer.hexagon)).toReal

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

theorem ConwaySoifer.Canonical.loss_ge_sq {c : ContactCase} {T : Configuration} {r s : ℝ} (H : Canonical c T r s) (i : Fin 6) : s ^ 2 ≤ sideLoss T i

theorem ConwaySoifer.Canonical.loss_overfull {c : ContactCase} {T : Configuration} {r s : ℝ} (H : Canonical c T r s) (i : Fin 6) (hover : r < rayLen (T (sideIndex i)) (vertex i) (sideDirection i false) + rayLen (T (sideIndex i)) (vertex i) (sideDirection i true)) : r ^ 2 / 4 ≤ sideLoss T i

theorem ConwaySoifer.Canonical.loss_mid {c : ContactCase} {T : Configuration} {r s : ℝ} (H : Canonical c T r s) (i : Fin 6) (j : Fin 3) (m : Fin 2) (hm : cornerMid j m ∈ (T (sideIndex i)).carrier) : r ^ 2 / 4 ≤ sideLoss T i

theorem ConwaySoifer.Canonical.aown_budget {T : Configuration} {r s : ℝ} (H : Canonical ContactCase.Aown T r s) (hs : s ≤ 1 / 14) (i : Fin 6) (hi : i ≠ 0) (hD : r ^ 2 / 4 ≤ sideLoss T i) : False

The budget of an Aown cover with s ≤ 1/14: no other side owner can lose r²/4.