SigmaLayer/PointerBorn: the ε-Born sandwich and the smooth-horn closure (brick 4b)

Category: dynamical measurement — the smooth-Hamiltonian witness route (specs/pointer-witness-plan.md brick 4, Born half; closes brick 4).

The preparation is honest about what the smooth witness offers: the epistemic state at base point p on the sector, and the pointer conditioned on the ready region —

pointerPrep p q₀ δ = epistemicMeasure p ⊗ (μ_FS[| readyRegion δ]),

a probability measure because the ready region has positive FS measure (readyRegion_pos) — no Dirac calibration posit anywhere, unlike the swap witness, whose exact collapse forced one (collapse_accuracy_bound).

★ The ε-Born sandwich (pointer_born_lower / pointer_born_upper): for every context with continuous rates, every preparation, every outcome,

rⱼ − 2ε ≤ pointerPrep(outcomeSector j) ≤ rⱼ + 2(N−1)ε,

with rⱼ = c.rate p j the context rate at the base point. The lower bound is the sector measure = rⱼ − 2ε exactly (pointerPrep_sector_measure, via the brick-3 slice volume) plus the correlation; the upper bound needs no cell geometry at all — the outcome sectors are pairwise disjoint and the lower bounds of the other N − 1 outcomes crowd out everything above rⱼ + 2(N−1)ε in a probability space.

★★ The smooth-horn closure (strengthened 2026-08-04: evolve_eq/stroke_eq fields added, so the continuity and Liouville claims are now about the bundled protocol rather than about globally-named maps that merely coincided with it) (SmoothWitnessClosure / smoothWitnessClosure, instantiated on the canonical moment-map context by smoothWitnessClosureCanonical): one witness carries, simultaneously — the protocol (two-time law = exponential group property), joint time–state continuity, Liouville preservation, a positive-measure ready state, record creation with the ontic sector selecting the outcome (correlation), structural persistence, and Born up to the stated ε. This is the smooth horn of the no_everywhere_correlation trade-off, exactly as specs/pointer-witness-plan.md scoped it: the piecewise witnesses keep exact records and exact Born at the price of discontinuity; this witness keeps continuity (and the papers' smooth-Hamiltonian architecture, at the formalisable level) at the price of ε.

⚠️ Honest scope. ε is a free parameter of the witness — the bounds hold for every ε > 0, but no limit statement is made here, and the corridor mass (up to 2Nε) genuinely receives no record. The Hamiltonian-generation statement for the full modulated coupling and the Lüders composition remain brick 5; the closure's born fields are sector-measure bounds, not an LLN frequency statement (the LLN layer can consume them exactly as arena_mixed_born_frequency consumed exact weights, a recorded extension).

References

specs/pointer-witness-plan.md (bricks 4, 5); specs/BACKLOG.md (the ★ L row); specs/future-work.md. Reused corpus API: epistemicMeasure/globalBasin_prob slice pattern (SigmaLayer/GlobalBasin.lean), volume_shrunkCell_slice (SigmaLayer/PointerLanding.lean), pointerProtocol + correlation/invariance (SigmaLayer/PointerProtocol.lean), ProbabilityTheory.cond (Mathlib + CsdLean4/Mathlib/Probability/ConditionalProbability.lean staging).

The preparation

noncomputable def CSD.RecordLayer.pointerPrep {N : ℕ} (p : LF4.CPN N) (q₀ : Pointer N) (δ : ℝ) : MeasureTheory.Measure (PointerArena N N)

The smooth witness's preparation: epistemic state at p on the sector, FS conditioned on the ready region on the pointer. Conditioning is legitimate — the ready region has positive measure (readyRegion_pos) — so no Dirac calibration posit enters.

Equations

• CSD.RecordLayer.pointerPrep p q₀ δ = (CSD.RecordLayer.epistemicMeasure p).prod (Matrix.UnitaryGroup.fubiniStudyMeasure q₀)[|CSD.RecordLayer.readyRegion δ]

theorem CSD.RecordLayer.isProbabilityMeasure_pointerPrep {N : ℕ} (p : LF4.CPN N) (q₀ : Pointer N) {δ : ℝ} (hδpos : 0 < δ) : MeasureTheory.IsProbabilityMeasure (pointerPrep p q₀ δ)

theorem CSD.RecordLayer.pointerPrep_sector_measure {N : ℕ} (c : ContextField N) {ε δ : ℝ} (hε : 0 ≤ ε) (hδpos : 0 < δ) (p : LF4.CPN N) (q₀ : Pointer N) (j : Fin N) : (pointerPrep p q₀ δ) (pointerSector c ε δ j) = ENNReal.ofReal (c.rate p j - 2 * ε)

The sector carries exactly its shrunk-slice mass: pointerPrep (pointerSector j) = rⱼ − 2ε. The base-point slice is the brick-3 volume; the ready conditioning contributes the factor 1.

The ε-Born sandwich

theorem CSD.RecordLayer.pointer_born_lower {N : ℕ} (c : ContextField N) (hc : ∀ (j : Fin N), Continuous fun (p : LF4.CPN N) => c.rate p j) {ε δ : ℝ} (hε : 0 < ε) (hδpos : 0 < δ) (hδ : δ ≤ 1 / 2) (p : LF4.CPN N) (q₀ : Pointer N) (j : Fin N) : ENNReal.ofReal (c.rate p j - 2 * ε) ≤ (pointerPrep p q₀ δ) ((pointerProtocol c hc ε hδ).outcomeSector j)

★ The lower Born bound: the outcome sector carries at least the shrunk-cell mass rⱼ − 2ε — sector containment (the landing theorem) plus the exact sector measure.

theorem CSD.RecordLayer.ofReal_finset_sum_le {ι : Type u_1} (s : Finset ι) (f : ι → ℝ) : ENNReal.ofReal (∑ i ∈ s, f i) ≤ ∑ i ∈ s, ENNReal.ofReal (f i)

ofReal is subadditive over finite sums.

theorem CSD.RecordLayer.pointer_born_upper {N : ℕ} [NeZero N] (c : ContextField N) (hc : ∀ (j : Fin N), Continuous fun (p : LF4.CPN N) => c.rate p j) {ε δ : ℝ} (hε : 0 < ε) (hδpos : 0 < δ) (hδ : δ ≤ 1 / 2) (p : LF4.CPN N) (q₀ : Pointer N) (i : Fin N) : (pointerPrep p q₀ δ) ((pointerProtocol c hc ε hδ).outcomeSector i) ≤ ENNReal.ofReal (c.rate p i + 2 * (↑N - 1) * ε)

★ The upper Born bound — with no upper-bound cell geometry: the sectors are pairwise disjoint, the other N − 1 lower bounds crowd out everything above rⱼ + 2(N−1)ε in a probability space.

The smooth-horn closure

structure CSD.RecordLayer.SmoothWitnessClosure {N : ℕ} (c : ContextField N) (ε δ : ℝ) : Type

★★ The smooth-horn closure: one witness carrying, simultaneously — the protocol (two-time law = exponential group property), joint time–state continuity, Liouville preservation, a positive-measure ready state, record creation with the ontic sector selecting the outcome, structural persistence, and Born up to the stated ε. The smooth horn of the no_everywhere_correlation trade-off, complementing (never displacing) the exact-record piecewise closures.

• protocol : MeasurementProtocol (PointerArena N N) N

  The measurement protocol (ramped exponential of the modulated coupling).

• jointly_continuous (s : ℝ) : Continuous (pointerRampedEvolve c ε s)

  Joint time–state continuity of the ramped propagator (definitionally the protocol's evolve — pointerRampedEvolve_eq_protocol).

• liouville (p₀ : LF4.CPN N) (q₀ : Pointer N) : MeasureTheory.MeasurePreserving (pointerEvolve c ε) (pointerLiouville p₀ q₀) (pointerLiouville p₀ q₀)

  Liouville preservation of the measurement stroke.

• ready_pos (p₀ : LF4.CPN N) (q₀ : Pointer N) : (pointerLiouville p₀ q₀) (arenaReady N δ) ≠ 0

  The apparatus-ready state has positive Liouville measure.

• correlates : self.protocol.CorrelatesOn (pointerSector c ε δ)

  Record creation: every pointer sector lands in its outcome's record cylinder.

• invariant : self.protocol.PointerInvariantOn

  Structural persistence: the pointer regions are invariant on the record window.

• born_lower (p : LF4.CPN N) (q₀ : Pointer N) (j : Fin N) : ENNReal.ofReal (c.rate p j - 2 * ε) ≤ (pointerPrep p q₀ δ) (self.protocol.outcomeSector j)

  The lower Born bound rⱼ − 2ε.

• born_upper (p : LF4.CPN N) (q₀ : Pointer N) (j : Fin N) : (pointerPrep p q₀ δ) (self.protocol.outcomeSector j) ≤ ENNReal.ofReal (c.rate p j + 2 * (↑N - 1) * ε)

  The upper Born bound rⱼ + 2(N−1)ε.

• evolve_eq (s : ℝ) (z : ℝ × PointerArena N N) : pointerRampedEvolve c ε s z = self.protocol.evolve s z.1 z.2

  The continuity and Liouville fields are about THIS protocol. Added 2026-08-04 (codebase audit): jointly_continuous and liouville are statements about the global maps pointerRampedEvolve/pointerEvolve, and nothing in the type previously tied them to protocol. That mattered because MeasurementCapstone exposes this closure existentially (Nonempty), which erases which protocol it is — so "the witness is jointly continuous" did not follow from the bundle. These two identifications close the gap: with them, the continuity and measure-preservation claims transfer to protocol.

• stroke_eq : self.protocol.evolve 0 1 = pointerEvolve c ε

  The measurement stroke Φ_{0→1} of this protocol is the propagator liouville speaks about.

noncomputable def CSD.RecordLayer.smoothWitnessClosure {N : ℕ} [NeZero N] (c : ContextField N) (hc : ∀ (j : Fin N), Continuous fun (p : LF4.CPN N) => c.rate p j) {ε δ : ℝ} (hε : 0 < ε) (hδpos : 0 < δ) (hδ : δ ≤ 1 / 2) : SmoothWitnessClosure c ε δ

★★ The smooth-horn closure is inhabited, for every context with continuous rates and every 0 < ε, 0 < δ ≤ 1/2.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CSD.RecordLayer.smoothWitnessClosureCanonical {N : ℕ} [NeZero N] {ε δ : ℝ} (hε : 0 < ε) (hδpos : 0 < δ) (hδ : δ ≤ 1 / 2) : SmoothWitnessClosure (momentContext N) ε δ

The closure on the canonical context — the Fubini–Study moment map, whose rates are continuous by LF4.continuous_momentMap.

Equations

• CSD.RecordLayer.smoothWitnessClosureCanonical hε hδpos hδ = CSD.RecordLayer.smoothWitnessClosure (CSD.RecordLayer.momentContext N) ⋯ hε hδpos hδ