The area budget with corner help and the bound s < 11/25

For an anchored cover with all twelve full side sections at least s: every side owner loses volume at least s²/2 outside the hexagon (wedge lemma), every corner owner contributes less than r²/46 inside the hexagon (corner cap), and the Lebesgue budget area_budget gives 6 s² < 7 r² - 6 + 3 r²/23 < 26/23, hence s² < 13/69 and s < 11/25.

Cap lemmas for an equilateral triangle

theorem ConwaySoifer.range_eq_triple (Q : EquilateralTriangle) (i j k : Fin 3) (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k) : {Q.vertices i, Q.vertices j, Q.vertices k} = Set.range Q.vertices

theorem ConwaySoifer.det_perm_ne_zero (Q : EquilateralTriangle) (hσ : 0 < Q.side) (i j k : Fin 3) (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k) : triangleDet (Q.vertices i) (Q.vertices j) (Q.vertices k) ≠ 0

theorem ConwaySoifer.carrier_eq_hull_perm (Q : EquilateralTriangle) (i j k : Fin 3) (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k) : Q.carrier = (convexHull ℝ) {Q.vertices i, Q.vertices j, Q.vertices k}

theorem ConwaySoifer.volume_hull_perm (Q : EquilateralTriangle) (i j k : Fin 3) (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k) : MeasureTheory.volume ((convexHull ℝ) {Q.vertices i, Q.vertices j, Q.vertices k}) = ENNReal.ofReal (Q.side ^ 2 / 2)

theorem ConwaySoifer.other_indices (i : Fin 3) : ∃ (j : Fin 3) (k : Fin 3), i ≠ j ∧ i ≠ k ∧ j ≠ k

The other two indices of a vertex, in some order.

theorem ConwaySoifer.cornerCap_volume (Q : EquilateralTriangle) (hσ : 0 < Q.side) (hσ1 : Q.side ≤ 1) (u : Point) (hu : normSq u = 1) {w : Point} (hw : w ∈ Q.carrier) (hw2 : cross u w = 2) : (MeasureTheory.volume (Q.carrier ∩ {p : Point | cross u p ≤ 1})).toReal < Q.side ^ 2 / 46

Universal corner cap: a triangle of side σ ≤ 1 containing a point of level 2 has volume < σ²/46 at levels ≤ 1.

theorem ConwaySoifer.midpointCost_volume (Q : EquilateralTriangle) (hσ : 0 < Q.side) (hσ1 : Q.side ≤ 1) (u : Point) (hu : normSq u = 1) {w : Point} (hw : w ∈ Q.carrier) (hw2 : cross u w = 3 / 2) : Q.side ^ 2 / 8 ≤ (MeasureTheory.volume (Q.carrier ∩ {p : Point | 1 < cross u p})).toReal

Midpoint cost: a triangle of side σ ≤ 1 containing a point of level 3/2 has volume ≥ σ²/8 at levels > 1.

Level forms of the corner cells

def ConwaySoifer.cornerLevel : Fin 3 → Point

cross (cornerLevel j) p is a + b, -a, -b for j = 0, 1, 2.

Equations

• ConwaySoifer.cornerLevel = ![(1, -1), (0, 1), (-1, 0)]

theorem ConwaySoifer.cornerLevel_normSq (j : Fin 3) : normSq (cornerLevel j) = 1

theorem ConwaySoifer.cornerLevel_corner (j : Fin 3) : cross (cornerLevel j) (corner j) = 2

theorem ConwaySoifer.cornerLevel_mid (j : Fin 3) (m : Fin 2) : cross (cornerLevel j) (cornerMid j m) = 3 / 2

theorem ConwaySoifer.hexagon_subset_level (j : Fin 3) : hexagon ⊆ {p : Point | cross (cornerLevel j) p ≤ 1}

The budget

def ConwaySoifer.MinAt.toAnchored {T : Configuration} {r s : ℝ} {i₀ : Fin 6} {r₀ : Bool} (h : MinAt T r s i₀ r₀) : AnchoredCover r

Forget the attained-minimum data while retaining the relabeled subunit cover.

Equations

• h.toAnchored = { triangles := T, common := ⋯, covers := ⋯, subunit := ⋯, anchored := ⋯ }

theorem ConwaySoifer.MinAt.r_pos {T : Configuration} {r s : ℝ} {i₀ : Fin 6} {r₀ : Bool} (h : MinAt T r s i₀ r₀) : 0 < r

theorem ConwaySoifer.MinAt.side_eq {T : Configuration} {r s : ℝ} {i₀ : Fin 6} {r₀ : Bool} (h : MinAt T r s i₀ r₀) (i : Fin 10) : (T i).side = r

theorem ConwaySoifer.MinAt.sidePt_mem {T : Configuration} {r s : ℝ} {i₀ : Fin 6} {r₀ : Bool} (h : MinAt T r s i₀ r₀) (i : Fin 6) (right : Bool) {t : ℝ} (ht0 : 0 ≤ t) (ht : t ≤ s) : linePoint (vertex i) (sideDirection i right) t ∈ (T (sideIndex i)).carrier

The side point at parameter t ≤ s lies in S_i.

theorem ConwaySoifer.MinAt.outside_ge {T : Configuration} {r s : ℝ} {i₀ : Fin 6} {r₀ : Bool} (h : MinAt T r s i₀ r₀) (i : Fin 6) : s ^ 2 ≤ h.toAnchored.outside i

Each side owner loses at least s² (normalised area) outside the hexagon.

theorem ConwaySoifer.MinAt.cornerHelp_lt {T : Configuration} {r s : ℝ} {i₀ : Fin 6} {r₀ : Bool} (h : MinAt T r s i₀ r₀) (j : Fin 3) : h.toAnchored.cornerHelp j < r ^ 2 / 23

Each corner owner helps less than r²/23 inside the hexagon.

theorem ConwaySoifer.MinAt.s_lt {T : Configuration} {r s : ℝ} {i₀ : Fin 6} {r₀ : Bool} (h : MinAt T r s i₀ r₀) : s < 11 / 25

The parameter bound s < 11/25.