The fixed lattice cover of the whole carrier

A finite portion of the radius-1/16 lattice keeps exactly the centres whose doubled source cylinders stay inside the unit cylinder. Its cardinality, covering and parent-inclusion properties, together with the volume bound for the radius-1/8 ball, are the geometric inputs of the whole-carrier pressure mass.

@[irreducible]

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

A fixed finite portion of the radius-1/16 lattice, keeping only centres whose doubled source cylinders remain inside the unit cylinder.

theorem CKN.Core.Step4.originBSlotLatticeIndices_card_le : originBSlotLatticeIndices.card ≤ 49 ^ 3 * 243

The fixed finite lattice has an explicit absolute cardinality bound.

theorem CKN.Core.Step4.originBSlotLatticeIndices_covers (w : Foundation.Parabolic.ParabolicPoint) (hw : w ∈ Foundation.Parabolic.parabolicCylinder 0 0 (11 / 16)) : ∃ k ∈ originBSlotLatticeIndices, w ∈ Foundation.Parabolic.parabolicCylinder (originLatticeCentre (1 / 16) k).1 (originLatticeCentre (1 / 16) k).2 (1 / 16)

The fixed finite lattice covers the entire origin carrier of radius 11/16, including its top time face.

theorem CKN.Core.Step4.originBSlotLatticeIndices_parent_subset {k : (Fin 3 → ℤ) × ℤ} (hk : k ∈ originBSlotLatticeIndices) : Foundation.Parabolic.parabolicCylinder (originLatticeCentre (1 / 16) k).1 (originLatticeCentre (1 / 16) k).2 (1 / 4) ⊆ Foundation.Parabolic.parabolicCylinder 0 0 1

Every retained centre has its radius-1/4 energy cylinder inside the unit data cylinder. Its source radius is 1/8 and covered-cell radius 1/16.

theorem CKN.Core.Step4.bslot_eighth_ball_volume_le_one : MeasureTheory.volume (Foundation.Parabolic.vec3Ball 0 (1 / 8)) ≤ 1

The radius-1/8 ball has volume at most one.