SigmaLayer/PointerLanding: the landing theorem (brick 3)

Category: dynamical measurement — the smooth-Hamiltonian witness route (specs/pointer-witness-plan.md brick 3).

The geometry brick: it discharges the two distance hypotheses that pointerEvolve_pure (brick 2b) left open, and lands the ready pointer in the record region.

• Midpoint separation (cellMid_dist_ge): distinct CDF-cell midpoints on the circle are at least (rⱼ + r_k)/2 apart. The circle distance is bounded below through UnitAddCircle.norm_eq (‖↑x‖ = |x − round x|) and an elementary case analysis on round (abs_sub_round_ge); the two real-line gap bounds are the loSum interval inequalities that already order the corpus's CDF cells. By the triangle inequality, a point of the ε-shrunk cell of j is then at distance ≥ r_k/2 from every other midpoint (shrunk_dist_other) — so on the shrunk cell the weight vector is pure, and no per-cell inclusion geometry is ever needed.
• Record transport is exact in the moment map (momentMap_pointerRot_smul): m_{j+1}(Uⱼ(π/2) • q) = m₀(q) — the quarter rotation carries the ready weight to the record weight pointwise on the whole pointer, so the open ready region maps into the open record region with margin to spare (pointerRot_smul_mem_recordRegion, δ ≤ 1/2).
• ★ The landing theorem (pointer_landing): sector in the shrunk cell of j + pointer ready ⇒ the propagator lands the point in arenaRecord j — a record is created by a continuous, Liouville-preserving propagator, with the ontic sector selecting the outcome. The sector coordinate is conserved (pointerEvolve_fst), and the outcome is exclusive (recordRegion_pairwiseDisjoint, brick 0).
• The Born seed (volume_shrunkCell_slice): at every base point the shrunk cell's fibre slice carries selector volume exactly rⱼ − 2ε (AddCircle.volume_closedBall) — the ε-Born accounting input for brick 4. With Σⱼ rⱼ = 1 and the record regions pairwise disjoint, the sector sandwich rⱼ − 2ε ≤ sector ≤ rⱼ + 2(N−1)ε will follow without any upper-bound cell geometry.

⚠️ Honest scope. Landing is stated for the shrunk-ball event, whose slice volume is rⱼ − 2ε, not the full circleCell of volume rⱼ — the deficit is the transition corridor forced by no_everywhere_correlation, priced explicitly by the witness parameter ε, never hidden. No protocol packaging, sector accounting, or LLN here — that is brick 4. Corridor points (slice measure ≤ 2Nε) receive partial rotations: legitimate pointer states outside every record region; nothing is claimed about them beyond measure preservation.

References

specs/pointer-witness-plan.md (bricks 3, 4); specs/BACKLOG.md (the ★ L row); specs/future-work.md. Reused corpus API: pointerEvolve_pure/pointerWeights (SigmaLayer/PointerWeights.lean), loSum_add_le_loSum/loSum_add_self_le_one (SigmaLayer/BornFibrePartition.lean), circleFibre_volume_univ (SigmaLayer/TorusFibre.lean), Projectivization.inner_toEuclideanLin_unitary (transition-probability staging), UnitAddCircle.norm_eq + AddCircle.volume_closedBall (Mathlib).

The circle-distance lower bound

theorem CSD.RecordLayer.abs_sub_round_ge {c s : ℝ} (hc0 : -1 ≤ c) (hc1 : c ≤ 0) (h0 : s ≤ -c) (h1 : s ≤ 1 + c) : s ≤ |c - ↑(round c)|

If s is below both integer-gap witnesses of c ∈ [−1, 0] — the gap to 0 and the gap to −1 — then s ≤ |c − round c|: whatever integer round picks is one of those two or lies at distance ≥ 1.

theorem CSD.RecordLayer.dist_coe_circle_ge {a b s : ℝ} (hs : 0 ≤ s) (hd : a + s ≤ b) (hw : b + s ≤ 1 + a) : s ≤ dist ↑a ↑b

The circle distance between two coe points is bounded below by any s ≥ 0 that fits in both the direct gap and the wrap-around gap.

theorem CSD.RecordLayer.cellMid_dist_ge {N : ℕ} {r : Fin N → ℝ} (hr : ∀ (i : Fin N), 0 ≤ r i) (hsum : ∑ i : Fin N, r i = 1) {j k : Fin N} (hjk : j ≠ k) : (r j + r k) / 2 ≤ dist (cellMid r j) (cellMid r k)

Midpoint separation: distinct CDF-cell midpoints are at least the mean of the two cell widths apart on the circle — both the direct gap (the loSum ordering) and the wrap-around gap (total mass 1) are that large.

theorem CSD.RecordLayer.shrunk_dist_other {N : ℕ} {r : Fin N → ℝ} (hr : ∀ (i : Fin N), 0 ≤ r i) (hsum : ∑ i : Fin N, r i = 1) {θ : CircleFibre} {j : Fin N} {ε : ℝ} (hε : 0 < ε) (hθ : dist θ (cellMid r j) ≤ r j / 2 - ε) {k : Fin N} (hkj : k ≠ j) : r k / 2 ≤ dist θ (cellMid r k)

Points of the shrunk cell of j are far from every other midpoint — triangle inequality from the midpoint separation; the strict ε-shrinking is exactly what pays for it.

Record transport in the moment map

theorem CSD.RecordLayer.momentMap_pointerRot_smul {K : ℕ} (j : Fin K) (q : Pointer K) : LF4.momentMap (pointerRotU (Real.pi / 2) j • q) j.succ = LF4.momentMap q 0

The quarter turn carries the ready weight to the record weight, exactly: m_{j+1}(Uⱼ(π/2) • q) = m₀(q) for every pointer state q.

theorem CSD.RecordLayer.pointerRot_smul_mem_recordRegion {K : ℕ} {δ : ℝ} (hδ : δ ≤ 1 / 2) {q : Pointer K} (hq : q ∈ readyRegion δ) (j : Fin K) : pointerRotU (Real.pi / 2) j • q ∈ recordRegion j

The open ready region lands inside the open record region with margin: for δ ≤ 1/2, m₀(q) > 1 − δ gives m_{j+1}(Uⱼ(π/2) • q) > 1 − δ ≥ 1/2.

The landing theorem

def CSD.RecordLayer.shrunkCell {N : ℕ} (c : ContextField N) (ε : ℝ) (j : Fin N) : Set (LF4.KSigma N)

The ε-shrunk cell of outcome j, as a sector event: base + selector points whose first fibre coordinate lies within rⱼ/2 − ε of the j-th cell midpoint, rates read at the ontic base point. This is exactly the region where the weight field is pure.

Equations

• CSD.RecordLayer.shrunkCell c ε j = {x : CSD.LF4.KSigma N | dist x.2.1 (CSD.RecordLayer.cellMid (c.rate x.1) j) ≤ c.rate x.1 j / 2 - ε}

theorem CSD.RecordLayer.measurableSet_shrunkCell {N : ℕ} (c : ContextField N) (ε : ℝ) (j : Fin N) : MeasurableSet (shrunkCell c ε j)

theorem CSD.RecordLayer.pointer_landing {N : ℕ} (c : ContextField N) {ε δ : ℝ} (hε : 0 < ε) (hδ : δ ≤ 1 / 2) {y : PointerArena N N} {j : Fin N} (hsec : y.1 ∈ shrunkCell c ε j) (hready : y.2 ∈ readyRegion δ) : pointerEvolve c ε y ∈ arenaRecord N j

★ The landing theorem: sector in the shrunk cell of outcome j, pointer ready (margin δ ≤ 1/2) — the continuous, Liouville-preserving propagator lands the point in the record cylinder of j. The ontic sector selects the outcome; the pointer records it.

The Born seed: the shrunk slice volume

theorem CSD.RecordLayer.volume_shrunkCell_slice {N : ℕ} (c : ContextField N) {ε : ℝ} (hε : 0 ≤ ε) (p : LF4.CPN N) (j : Fin N) : MeasureTheory.volume {θ : LF4.KTorus | dist θ.1 (cellMid (c.rate p) j) ≤ c.rate p j / 2 - ε} = ENNReal.ofReal (c.rate p j - 2 * ε)

The selector volume of the shrunk cell's fibre slice is exactly rⱼ − 2ε, at every base point (when rⱼ < 2ε both sides are 0) — the lower Born bound brick 4 integrates. The 2ε deficit is the transition corridor, priced and visible.