SigmaLayer/PointerProtocol: the smooth witness as a measurement protocol (brick 4a)

Category: 7-SigmaLayer (dynamical measurement) — the smooth-Hamiltonian witness route (specs/pointer-witness-plan.md brick 4, protocol half).

The pointer witness enters the corpus's standard record architecture: a MeasurementProtocol on PointerArena N N whose two-time propagator is the ramped exponential of the selector-modulated coupling,

Φ_{s→t}(x, q) = (x, exp((κ(t) − κ(s)) • (−i • couplingH (w x))) • q),

with κ the C⁰ ramp t ↦ (π/2)·clamp₀¹(t) frozen after the readout time. Everything the piecewise witnesses had to fight for arrives structurally:

• the two-time law is the group property of the exponential (couplingUAt_mul, from Matrix.exp_add_of_commute — the same generator always commutes with itself), against the swap's eight-case crossing analysis;
• persistence is freezing: after the readout time the ramp is constant, the angle increment is 0, the propagator is the identity — PointerInvariantOn is discharged outright (pointerProtocol_pointerInvariantOn), so record_persists_on_interval and readout_persists_on_interval apply verbatim;
• the correlation obligation is the landing theorem: CorrelatesOn (pointerSector …) (pointerProtocol_correlatesOn) with sectors = shrunk cell × ready region, via pointer_landing at the stroke evolve 0 1 = pointerEvolve (pointerProtocol_evolve_stroke);
• ★ the propagator is jointly continuous in time and state (continuous_pointerRampedEvolve, at every start time s; identified with the protocol's evolve by pointerRampedEvolve_eq_protocol) — Corrected 2026-08-04 (codebase audit).: this cited continuous_pointerProtocolEvolve, a name that exists nowhere in the corpus — against not only shearEvolve_not_continuous (state discontinuity) but also the swap witnesses' record-triggered firing, which is discontinuous in time. Route: the entrywise time-Lipschitz estimate (norm_couplingUAt_sub_time, Duhamel with the roles of time and generator swapped) plus the weight estimate, squeezed through tendsto_iff_dist_tendsto_zero; the projective action by the generic open-quotient descent continuous_unitaryFamily_smul.

⚠️ Honest scope. The correlation and invariance are established for this protocol's sectors, which cover 1 − 2Nε of the selector mass, not all of it — the corridor is the no_everywhere_correlation price, as everywhere on this route. The ramp is C⁰ (piecewise-linear in time); upgrading to a C^∞ ramp changes nothing structural and is recorded in the plan as part of brick 5's presentation. The ε-Born sector sandwich is brick 4b, not this module.

References

specs/pointer-witness-plan.md (brick 4); specs/BACKLOG.md (the ★ L row); specs/future-work.md. Reused corpus API: MeasurementProtocol + CorrelatesOn/PointerInvariantOn (RecordLayer/MeasurementProtocol.lean, RecordPersistence.lean), pointer_landing/shrunkCell (RecordLayer/PointerLanding.lean), couplingH/couplingU estimates (RecordLayer/PointerCoupling.lean), Matrix.norm_exp_smul_sub_exp_smul_le + Matrix.conjTranspose_real_smul_skew (DuhamelBound.lean staging), Matrix.exp_add_of_commute (Mathlib).

The propagator at an arbitrary angle

noncomputable def CSD.RecordLayer.couplingUAt {K : ℕ} (a : ℝ) (w : Fin K → ℝ) : Matrix (Fin (K + 1)) (Fin (K + 1)) ℂ

The coupling propagator at angle a: exp(a • (−i • couplingH w)). Brick 2a's couplingU is the stroke value a = π/2.

Equations

• CSD.RecordLayer.couplingUAt a w = NormedSpace.exp (a • -Complex.I • CSD.RecordLayer.couplingH w)

theorem CSD.RecordLayer.couplingUAt_pi_div_two {K : ℕ} (w : Fin K → ℝ) : couplingUAt (Real.pi / 2) w = couplingU w

theorem CSD.RecordLayer.couplingUAt_zero {K : ℕ} (w : Fin K → ℝ) : couplingUAt 0 w = 1

theorem CSD.RecordLayer.couplingUAt_mul {K : ℕ} (a b : ℝ) (w : Fin K → ℝ) : couplingUAt a w * couplingUAt b w = couplingUAt (a + b) w

The angle-additive law — the two-time composition of the smooth witness is the group property of the exponential, not a case analysis.

theorem CSD.RecordLayer.couplingUAt_mem_unitaryGroup {K : ℕ} (a : ℝ) (w : Fin K → ℝ) : couplingUAt a w ∈ Matrix.unitaryGroup (Fin (K + 1)) ℂ

noncomputable def CSD.RecordLayer.couplingUUAt {K : ℕ} (a : ℝ) (w : Fin K → ℝ) : ↥(Matrix.unitaryGroup (Fin (K + 1)) ℂ)

The angle-a propagator as a unitary-group element.

Equations

• CSD.RecordLayer.couplingUUAt a w = ⟨CSD.RecordLayer.couplingUAt a w, ⋯⟩

theorem CSD.RecordLayer.couplingUUAt_zero {K : ℕ} (w : Fin K → ℝ) : couplingUUAt 0 w = 1

theorem CSD.RecordLayer.couplingUUAt_mul {K : ℕ} (a b : ℝ) (w : Fin K → ℝ) : couplingUUAt a w * couplingUUAt b w = couplingUUAt (a + b) w

theorem CSD.RecordLayer.couplingUUAt_pi_div_two {K : ℕ} (w : Fin K → ℝ) : couplingUUAt (Real.pi / 2) w = couplingUU w

The two Lipschitz estimates and joint entry continuity

theorem CSD.RecordLayer.norm_couplingUAt_sub_le {K : ℕ} (a : ℝ) (w w' : Fin K → ℝ) : ‖couplingUAt a w - couplingUAt a w'‖ ≤ (|a| * ∑ j : Fin K, ‖pointerH j‖) * dist w w'

The Duhamel estimate in the weights, at an arbitrary angle.

theorem CSD.RecordLayer.norm_couplingUAt_sub_time {K : ℕ} (a b : ℝ) (w : Fin K → ℝ) : ‖couplingUAt a w - couplingUAt b w‖ ≤ |a - b| * ‖couplingH w‖

The Duhamel estimate in the angle — time and generator with roles swapped: exp(1 • (a•A)) − exp(1 • (b•A)) for the skew generators a•A, b•A.

theorem CSD.RecordLayer.continuous_couplingUAt_entry_joint {K : ℕ} (b d : Fin (K + 1)) : Continuous fun (z : ℝ × (Fin K → ℝ)) => couplingUAt z.1 z.2 b d

Joint continuity of each propagator entry in (angle, weights) — squeezed between the two Lipschitz estimates; no scoped-instance topology appears in the statement.

The generic continuous unitary action

theorem CSD.RecordLayer.continuous_unitaryFamily_smul {K : ℕ} {X : Type u_1} [TopologicalSpace X] {U : X → ↥(Matrix.unitaryGroup (Fin (K + 1)) ℂ)} (hU : Continuous U) : Continuous fun (z : X × Pointer K) => U z.1 • z.2

A continuous family of unitaries acts continuously on the pointer — the open-quotient descent of brick 2b, factored out for reuse: any topological parameter space, any continuous family into the unitary group (Pi topology).

The ramp and the protocol

noncomputable def CSD.RecordLayer.pointerRamp (t : ℝ) : ℝ

The measurement ramp: zero before the interaction, frozen at the quarter-turn stroke after readout.

★ Substituted onto the C^∞ profile 2026-08-04 (BACKLOG.md B1b). This was (π/2)·clamp₀¹(t), piecewise-linear with corners at t ∈ {0,1} — which is why rampedU_schrodinger could only hold on the open window (0,1). It is now (π/2)·smoothTransition t, C^∞ everywhere. The plateau interface is unchanged (pointerRamp_zero, pointerRamp_of_one_le), so the protocol's two-time law, freezing and persistence are untouched; what changes is the generation statement, which now holds at every time and carries the rate factor smoothTransition′(t) — a window-free ODE in place of a constant-generator one on a punctured interval.

Equations

• CSD.RecordLayer.pointerRamp t = CSD.RecordLayer.smoothPointerRamp t

theorem CSD.RecordLayer.pointerRamp_zero : pointerRamp 0 = 0

theorem CSD.RecordLayer.pointerRamp_of_one_le {t : ℝ} (ht : 1 ≤ t) : pointerRamp t = Real.pi / 2

theorem CSD.RecordLayer.pointerRamp_one : pointerRamp 1 = Real.pi / 2

theorem CSD.RecordLayer.continuous_pointerRamp : Continuous pointerRamp

theorem CSD.RecordLayer.contDiff_pointerRamp {n : ℕ∞} : ContDiff ℝ (↑n) pointerRamp

The ramp is C^∞ — new with the B1b substitution; the trapezoid was only Lipschitz.

noncomputable def CSD.RecordLayer.pointerProtocol {N : ℕ} (c : ContextField N) (hc : ∀ (j : Fin N), Continuous fun (p : LF4.CPN N) => c.rate p j) (ε : ℝ) {δ : ℝ} (hδ : δ ≤ 1 / 2) : MeasurementProtocol (PointerArena N N) N

★ The smooth witness as a measurement protocol. Two-time propagator = ramped exponential of the selector-modulated coupling; ready/pointer regions = the brick-0 cylinders. The two-time law is the exponential group property; freezing after readout makes persistence structural.

Equations

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

theorem CSD.RecordLayer.pointerProtocol_evolve_stroke {N : ℕ} (c : ContextField N) (hc : ∀ (j : Fin N), Continuous fun (p : LF4.CPN N) => c.rate p j) (ε : ℝ) {δ : ℝ} (hδ : δ ≤ 1 / 2) : (pointerProtocol c hc ε hδ).evolve 0 1 = pointerEvolve c ε

The full-stroke identification: Φ_{0→1} is the brick-2b propagator.

theorem CSD.RecordLayer.pointerProtocol_outcomeSector {N : ℕ} (c : ContextField N) (hc : ∀ (j : Fin N), Continuous fun (p : LF4.CPN N) => c.rate p j) {ε δ : ℝ} (hδ : δ ≤ 1 / 2) (i : Fin N) : (pointerProtocol c hc ε hδ).outcomeSector i = pointerEvolve c ε ⁻¹' arenaRecord N i

The sector identification: the smooth protocol's outcome sector is the brick-2b propagator's preimage of the record cylinder. Pins down the trigger the relocation reads.

theorem CSD.RecordLayer.pointerProtocol_evolve_apply {N : ℕ} (c : ContextField N) (hc : ∀ (j : Fin N), Continuous fun (p : LF4.CPN N) => c.rate p j) (ε : ℝ) {δ : ℝ} (hδ : δ ≤ 1 / 2) (s t : ℝ) (y : PointerArena N N) : (pointerProtocol c hc ε hδ).evolve s t y = (y.1, couplingUUAt (pointerRamp t - pointerRamp s) (pointerWeights c ε y.1) • y.2)

The propagator, unfolded — the definitional bridge used by every statement below.

noncomputable def CSD.RecordLayer.rampedUU {N : ℕ} (c : ContextField N) (ε s : ℝ) (v : ℝ × LF4.KSigma N) : ↥(Matrix.unitaryGroup (Fin (N + 1)) ℂ)

The ramped unitary family, named so continuity statements carry concrete types.

Equations

• CSD.RecordLayer.rampedUU c ε s v = CSD.RecordLayer.couplingUUAt (CSD.RecordLayer.pointerRamp v.1 - CSD.RecordLayer.pointerRamp s) (CSD.RecordLayer.pointerWeights c ε v.2)

theorem CSD.RecordLayer.continuous_rampedUU {N : ℕ} (c : ContextField N) (hc : ∀ (j : Fin N), Continuous fun (p : LF4.CPN N) => c.rate p j) (ε s : ℝ) : Continuous (rampedUU c ε s)

noncomputable def CSD.RecordLayer.pointerRampedEvolve {N : ℕ} (c : ContextField N) (ε s : ℝ) : ℝ × PointerArena N N → PointerArena N N

The ramped arena propagator as a time–state map: definitionally (pointerProtocol c hc ε hδ).evolve s z.1 z.2 (see pointerRampedEvolve_eq_protocol).

Equations

• CSD.RecordLayer.pointerRampedEvolve c ε s z = (z.2.1, CSD.RecordLayer.rampedUU c ε s (z.1, z.2.1) • z.2.2)

theorem CSD.RecordLayer.pointerRampedEvolve_eq_protocol {N : ℕ} (c : ContextField N) (hc : ∀ (j : Fin N), Continuous fun (p : LF4.CPN N) => c.rate p j) (ε : ℝ) {δ : ℝ} (hδ : δ ≤ 1 / 2) (s : ℝ) (z : ℝ × PointerArena N N) : pointerRampedEvolve c ε s z = (pointerProtocol c hc ε hδ).evolve s z.1 z.2

The named map is the protocol propagator, definitionally.

theorem CSD.RecordLayer.continuous_pointerRampedEvolve {N : ℕ} (c : ContextField N) (hc : ∀ (j : Fin N), Continuous fun (p : LF4.CPN N) => c.rate p j) (ε s : ℝ) : Continuous (pointerRampedEvolve c ε s)

★ Joint continuity in time and state — the property neither piecewise witness has: the shear/swap witnesses jump in the state (shearEvolve_not_continuous) and fire discontinuously in time at the crossing; the smooth witness does neither (pointerRampedEvolve_eq_protocol identifies this map with the protocol's propagator).

Correlation and persistence

def CSD.RecordLayer.pointerSector {N : ℕ} (c : ContextField N) (ε δ : ℝ) (j : Fin N) : Set (PointerArena N N)

The selector sectors of the smooth witness: shrunk cell × ready region.

Equations

• CSD.RecordLayer.pointerSector c ε δ j = CSD.RecordLayer.shrunkCell c ε j ×ˢ CSD.RecordLayer.readyRegion δ

theorem CSD.RecordLayer.measurableSet_pointerSector {N : ℕ} (c : ContextField N) (ε δ : ℝ) (j : Fin N) : MeasurableSet (pointerSector c ε δ j)

theorem CSD.RecordLayer.pointerProtocol_correlatesOn {N : ℕ} (c : ContextField N) (hc : ∀ (j : Fin N), Continuous fun (p : LF4.CPN N) => c.rate p j) {ε δ : ℝ} (hε : 0 < ε) (hδ : δ ≤ 1 / 2) : (pointerProtocol c hc ε hδ).CorrelatesOn (pointerSector c ε δ)

The correlation obligation, discharged: every pointer sector is carried into its outcome's record cylinder — the landing theorem in protocol form.

theorem CSD.RecordLayer.pointerProtocol_pointerInvariantOn {N : ℕ} (c : ContextField N) (hc : ∀ (j : Fin N), Continuous fun (p : LF4.CPN N) => c.rate p j) (ε : ℝ) {δ : ℝ} (hδ : δ ≤ 1 / 2) : (pointerProtocol c hc ε hδ).PointerInvariantOn

Persistence is structural: after readout the ramp is frozen, the propagator is the identity on the record window, so the pointer regions are invariant.