From the common half-collar scale to every clipped cell

Bounds at closed carrier centres for radii at most 1/256 imply the unrestricted clipped-cell bound. The explicit cover count is absorbed once into the affine pressure coefficient.

An absolute lattice cover for thin pressure collars

The doubled cells have radius 1/512, below both prescribed half-collars. The existing shifted-centre construction keeps every centre in the carrier.

@[irreducible]

def CKN.Core.Step4.originASlotThinCoverBox : Finset ((Fin 3 → ℤ) × ℤ)

The lattice indices that a cell of radius 1/1024 can carry while meeting the origin carrier of radius R < 3/4.

Equations

• CKN.Core.Step4.originASlotThinCoverBox = (Fintype.piFinset fun (x : Fin 3) => Finset.Icc (-1538) 1538) ×ˢ Finset.Icc (-1179648) 2

theorem CKN.Core.Step4.originASlotThinCoverBox_card : originASlotThinCoverBox.card = 34366557335620983

The index box has 3077³ · 1179651 members.

theorem CKN.Core.Step4.originASlotThinCoverBox_mem {R a : ℝ} (hR : 0 < R) (hRlt : R < 3 / 4) (ha : a = 1 / 1024) {k : (Fin 3 → ℤ) × ℤ} {w : Foundation.Parabolic.ParabolicPoint} (hcell : w ∈ Foundation.Parabolic.parabolicCylinder (originLatticeCentre a k).1 (originLatticeCentre a k).2 a) (hcarrier : w ∈ Foundation.Parabolic.parabolicCylinder 0 0 R) : k ∈ originASlotThinCoverBox

A lattice cell of radius 1/1024 that meets the carrier of radius R has its index in the absolute box.

theorem CKN.Core.Step4.originASlot_carrier_subset_thin_cells {R a : ℝ} (hR : 0 < R) (hRlt : R < 3 / 4) (ha : a = 1 / 1024) : Foundation.Parabolic.parabolicCylinder 0 0 R ⊆ ⋃ k ∈ originASlotThinCoverBox, Foundation.Parabolic.parabolicCylinder (originASlotShiftedCentre R (originLatticeCentre a k) a).1 (originASlotShiftedCentre R (originLatticeCentre a k) a).2 (2 * a)

The origin carrier is covered by the doubled margin cells attached to the lattice indices of the absolute box. Every centre used lies in the carrier and every radius used is 1/512.

def CKN.Core.Step4.originASlotThinCellThreshold (Cbase : ℝ) : ℝ

The Calderón–Zygmund threshold at which every clipped cell of the origin carrier inherits the thin-cell A slot: the number of thin cells used to cover the carrier, times the constant of the thin-cell estimate.

Equations

• CKN.Core.Step4.originASlotThinCellThreshold Cbase = 34366557335620983 * (|Cbase| + 1)

theorem CKN.Core.Step4.originKPAffineASlot_thin_cover_count_mul_le {q ε Cbase C_CZ : ℝ} {KU KD : ENNReal} (hthreshold : originASlotThinCellThreshold Cbase ≤ C_CZ) : 34366557335620983 * originKPAffineASlot q Cbase ε KU KD ≤ originKPAffineASlot q C_CZ ε KU KD

The threshold multiplies the affine slot by the cover count.

theorem CKN.Core.Step4.originASlot_clipped_cell_of_thin_cells {q τ R₁ ε Cbase C_CZ : ℝ} {KU KD : ENNReal} (hq : 5 / 2 < q) (hτ : 25 / 3 ≤ τ) (hτhi : τ ≤ 25) (hR₁ : 0 < R₁) (hR₁lt : R₁ < 3 / 4) (hthreshold : originASlotThinCellThreshold Cbase ≤ C_CZ) {Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hDp : Measurable Dp) (i : Fin 3) (hmargin : ∀ w ∈ closure (Foundation.Parabolic.parabolicCylinder 0 0 R₁), ∀ (ρ : ℝ), 0 < ρ → ρ ≤ 1 / 256 → ∫⁻ (s : ℝ) in Set.Ioc (w.2 - ρ ^ 2) w.2 ∩ Set.Ioc (-R₁ ^ 2) 0, MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball w.1 ρ ∩ Foundation.Parabolic.vec3Ball 0 R₁)) ^ (6 / 5) ≤ originKPAffineASlot q Cbase ε KU KD * ENNReal.ofReal (ρ ^ (5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q)))) (z : Foundation.Parabolic.ParabolicPoint) {r : ℝ} (hr : 0 < r) : ∫⁻ (s : ℝ) in Set.Ioc (z.2 - r ^ 2) z.2 ∩ Set.Ioc (-R₁ ^ 2) 0, MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 r ∩ Foundation.Parabolic.vec3Ball 0 R₁)) ^ (6 / 5) ≤ originKPAffineASlot q C_CZ ε KU KD * ENNReal.ofReal (r ^ (5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q)))

Thin cells control every cell. Given the clipped A-slot estimate of prop:bootstrap on thin cells at the constant Cbase, every clipped cell — any centre, any positive radius — obeys the same estimate at any constant above originASlotThinCellThreshold Cbase.