§8.1: the small Across regime s ≤ 1/400

Let c be the full section of S₀ from v₀ towards w₀ (direction (0, 1)). The face inequality of the internal endpoint together with (1, c) ∈ S₀ gives 0 ≤ x ≤ s + (s/c) y on S₀ ∩ H in the local coordinates of v₀, and the diameter with v₀ gives y < 6/5; hence |S₀ ∩ H| ≤ 6s/5 + 18 s/(25 c). With M₀ ∈ S₁ the budget forces c < 16 s. The point (1, c) is reached by A₀ or S₁ (closedness); A₀ is excluded since M₀ ∉ A₀, so (1, c) ∈ S₁, hence (1, 16 s) ∈ S₁, and the four points v₁, (-s, 1), M₀, (1, 16 s) are excluded by the checker for s ≤ 1/400.

A generic wedge region at v₀

def ConwaySoifer.wedgeRegion (A B Y : ℝ) : Set Point

The image of the local wedge trapezoid in triangular coordinates.

Equations

• ConwaySoifer.wedgeRegion A B Y = {p : ConwaySoifer.Point | 0 ≤ ConwaySoifer.locY p ∧ ConwaySoifer.locY p ≤ Y ∧ 0 ≤ ConwaySoifer.locX p ∧ ConwaySoifer.locX p ≤ A + B * ConwaySoifer.locY p}

def ConwaySoifer.wedgeBox (A B Y : ℝ) : Set (ℝ × ℝ)

A closed trapezoidal region in local wedge coordinates.

Equations

• ConwaySoifer.wedgeBox A B Y = {q : ℝ × ℝ | 0 ≤ q.2 ∧ q.2 ≤ Y ∧ 0 ≤ q.1 ∧ q.1 ≤ A + B * q.2}

theorem ConwaySoifer.isClosed_wedgeBox (A B Y : ℝ) : IsClosed (wedgeBox A B Y)

theorem ConwaySoifer.wedgeBox_section (A B Y y : ℝ) : MeasureTheory.volume ((fun (x : ℝ) => (x, y)) ⁻¹' wedgeBox A B Y) = (Set.Icc 0 Y).indicator (fun (y : ℝ) => ENNReal.ofReal (A + B * y)) y

theorem ConwaySoifer.integral_wedge (A B Y : ℝ) : ∫ (y : ℝ) in 0..Y, A + B * y = A * Y + B * Y ^ 2 / 2

theorem ConwaySoifer.volume_wedgeBox (A B Y : ℝ) (hA : 0 ≤ A) (hB : 0 ≤ B) (hY : 0 ≤ Y) : MeasureTheory.volume (wedgeBox A B Y) = ENNReal.ofReal (A * Y + B * Y ^ 2 / 2)

theorem ConwaySoifer.wedgeRegion_eq_image (A B Y : ℝ) : wedgeRegion A B Y = ⇑(areaTriMap (vertex 0) (sideDirection 0 true) (sideDirection 0 false)) '' wedgeBox A B Y

theorem ConwaySoifer.volume_wedgeRegion (A B Y : ℝ) (hA : 0 ≤ A) (hB : 0 ≤ B) (hY : 0 ≤ Y) : MeasureTheory.volume (wedgeRegion A B Y) = ENNReal.ofReal (A * Y + B * Y ^ 2 / 2)

The external section c of S₀

def ConwaySoifer.upDir : Point

The direction from v₀ to w₀.

Equations

• ConwaySoifer.upDir = (0, 1)

theorem ConwaySoifer.upDir_unit : sqDist upDir (0, 0) = 1

theorem ConwaySoifer.upPt_eq (t : ℝ) : linePoint (vertex 0) upDir t = (1, t)

theorem ConwaySoifer.upPt_eq_cornerSeg (t : ℝ) : linePoint (vertex 0) upDir t = linePoint (corner 0) (cornerDirection 0 0) (1 - t)

theorem ConwaySoifer.sqDist_vertex0 (p : Point) : sqDist p (vertex 0) = locX p ^ 2 - locX p * locY p + locY p ^ 2

theorem ConwaySoifer.Canonical.across_v0_mem {T : Configuration} {r s : ℝ} (H : Canonical ContactCase.Across T r s) : vertex 0 ∈ (T 1).carrier

theorem ConwaySoifer.Canonical.ext_pos {T : Configuration} {r s : ℝ} (H : Canonical ContactCase.Across T r s) : 0 < rayLen (T 1) (vertex 0) upDir

The external section is positive: no other owner contains v₀.

theorem ConwaySoifer.Canonical.ext_le {T : Configuration} {r s : ℝ} (H : Canonical ContactCase.Across T r s) : rayLen (T 1) (vertex 0) upDir ≤ r

theorem ConwaySoifer.Canonical.across_subset {T : Configuration} {r s : ℝ} (H : Canonical ContactCase.Across T r s) : (T 1).carrier ∩ hexagon ⊆ wedgeRegion s (s / rayLen (T 1) (vertex 0) upDir) (6 / 5)

S₀ ∩ H lies in the wedge region 0 ≤ x ≤ s + (s/c) y, 0 ≤ y ≤ 6/5.

theorem ConwaySoifer.Canonical.across_inter_le {T : Configuration} {r s : ℝ} (H : Canonical ContactCase.Across T r s) : (MeasureTheory.volume ((T 1).carrier ∩ hexagon)).toReal ≤ s * (6 / 5) + s / rayLen (T 1) (vertex 0) upDir * (6 / 5) ^ 2 / 2

theorem ConwaySoifer.Canonical.ext_lt {T : Configuration} {r s : ℝ} (H : Canonical ContactCase.Across T r s) (hs : s ≤ 1 / 400) : rayLen (T 1) (vertex 0) upDir < 16 * s

The budget forces c < 16 s.