SigmaLayer/PointerCoupling: the weighted coupling and its exponential propagator (brick 2a)

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

The selector-modulated coupling is a weighted sum of the plane-swap generators:

couplingH w = Σⱼ wⱼ • hⱼ, hⱼ = |f₀⟩⟨f_{j+1}| + |f_{j+1}⟩⟨f₀|,

Hermitian for every real weight vector (couplingH_isHermitian) — the hⱼ do not commute pairwise (all planes share f₀), so the propagator is the genuine matrix exponential, not a closed form:

couplingU w = exp((π/2) • (−i • couplingH w)),

unitary by the skew-Hermitian exponential theorem (couplingU_mem_unitaryGroup, via Matrix.StoneC1.exp_smul_unitary). Three facts make it the right object:

• On a pure weight it is the brick-1 rotation: couplingU (Pi.single j 1) = pointerRot (π/2) j (couplingU_single) — through ★ pointerRot_eq_exp, the Hamiltonian-generation identification pointerRot θ j = exp(θ • (−i • hⱼ)), proved by ODE uniqueness (Matrix.StoneC1.eq_exp_of_hasDeriv: the closed form solves Y' = Y·A, Y 0 = 1). This was scheduled as brick 5 but is pulled forward: the landing theorem (brick 3) reads the propagator on pure cells through it.
• It is entrywise Lipschitz in the weights (continuous_couplingU_entry): the Duhamel bound ‖exp(t•(−iH)) − exp(t•(−iH₀))‖ ≤ |t|·‖H−H₀‖ plus the entry bound ‖M a b‖ ≤ ‖M‖ (staged Matrix.norm_entry_le_l2_opNorm) give ‖couplingU w − couplingU w'‖ ≤ (π/2)·(Σⱼ‖hⱼ‖)·dist(w,w') — so each entry is a Lipschitz, hence continuous, function of the weight vector, stated in the plain Pi topology (no scoped norm instances leak into the statement).
• Liouville preservation on the pointer is FS unitary invariance (couplingUU_measurePreserving), as always.

⚠️ Honest scope. This is the generator half of brick 2: the weights here are a free parameter w : Fin K → ℝ. The bump weight field w(p,θ) (trapezoids on ε-shrunk context cells) and the joint continuity of the full arena propagator are brick 2b; record landing, Born accounting, and the protocol are bricks 3–4. pointerRot_eq_exp upgrades brick 1's honest-scope note: the closed form is now identified with the exponential of its Hermitian generator — the generation statement at the formalisable level for the single-plane rotation. The moment-map (symplectic) reading of "Hamiltonian" remains prose: Mathlib has no symplectic API (MATHLIB-GAPS.md).

References

specs/pointer-witness-plan.md (bricks 2, 5); specs/BACKLOG.md (the ★ L row); specs/future-work.md. Reused corpus API: Matrix.StoneC1.eq_exp_of_hasDeriv / exp_smul_unitary (Mathlib/Analysis/Matrix/StoneC1.lean staging), Matrix.norm_exp_smul_neg_I_sub_le (DuhamelBound.lean staging), Matrix.norm_entry_le_l2_opNorm (L2OpNormEntry.lean staging, new), pointerH/pointerRot algebra (SigmaLayer/PointerRotation.lean), fubiniStudyMeasure_smul_invariant.

The weighted coupling generator

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

The weighted coupling Σⱼ wⱼ • hⱼ: the selector will set the weights; here they are a free real vector.

Equations

• CSD.RecordLayer.couplingH w = ∑ j : Fin K, ↑(w j) • CSD.RecordLayer.pointerH j

theorem CSD.RecordLayer.couplingH_isHermitian {K : ℕ} (w : Fin K → ℝ) : (couplingH w).IsHermitian

The coupling is Hermitian for every real weight vector.

theorem CSD.RecordLayer.couplingH_skew {K : ℕ} (w : Fin K → ℝ) : star (-Complex.I • couplingH w) = -(-Complex.I • couplingH w)

The Schrödinger generator −i • couplingH w is skew-Hermitian.

theorem CSD.RecordLayer.couplingH_single {K : ℕ} (j : Fin K) : couplingH (Pi.single j 1) = pointerH j

On the pure weight vector of outcome j, the coupling is the plane swap hⱼ.

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

The coupling difference is linear in the weight difference, in norm: ‖couplingH w − couplingH w'‖ ≤ (Σⱼ ‖hⱼ‖) · dist(w, w').

The exponential propagator

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

The coupling propagator at the measurement stroke: exp((π/2) • (−i • couplingH w)). The hⱼ do not commute, so this is the honest matrix exponential — no closed form.

Equations

• CSD.RecordLayer.couplingU w = NormedSpace.exp ((Real.pi / 2) • -Complex.I • CSD.RecordLayer.couplingH w)

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

The coupling propagator is unitary — the skew-Hermitian exponential theorem.

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

The coupling propagator as a unitary-group element.

Equations

• CSD.RecordLayer.couplingUU w = ⟨CSD.RecordLayer.couplingU w, ⋯⟩

theorem CSD.RecordLayer.couplingUU_measurePreserving {K : ℕ} (w : Fin K → ℝ) (q₀ : Pointer K) : MeasureTheory.MeasurePreserving (fun (q : Pointer K) => couplingUU w • q) (Matrix.UnitaryGroup.fubiniStudyMeasure q₀) (Matrix.UnitaryGroup.fubiniStudyMeasure q₀)

Liouville preservation on the pointer: FS unitary invariance.

The generation identification (brick 5's statement, pulled forward)

theorem CSD.RecordLayer.pointerRot_mul_gen {K : ℕ} (t : ℝ) (j : Fin K) : pointerRot t j * -Complex.I • pointerH j = -↑(Real.sin t) • pointerPlane j + -(Complex.I * ↑(Real.cos t)) • pointerH j

The closed-form rotation, multiplied by its claimed generator on the right.

theorem CSD.RecordLayer.pointerRot_eq_exp {K : ℕ} (θ : ℝ) (j : Fin K) : pointerRot θ j = NormedSpace.exp (θ • -Complex.I • pointerH j)

★ The Hamiltonian-generation identification for the plane rotation: the brick-1 closed form is the exponential of its Hermitian generator,

pointerRot θ j = exp(θ • (−i • hⱼ)),

by ODE uniqueness (Matrix.StoneC1.eq_exp_of_hasDeriv): both sides solve Y' = Y·(−i hⱼ) with Y 0 = 1. This discharges the single-plane half of brick 5's generation obligation.

theorem CSD.RecordLayer.couplingU_single {K : ℕ} (j : Fin K) : couplingU (Pi.single j 1) = pointerRot (Real.pi / 2) j

On a pure weight the coupling propagator is the brick-1 quarter rotation — the pure cells of the modulated witness run exactly the fixed-outcome record transport.

Entrywise Lipschitz continuity in the weights

theorem CSD.RecordLayer.norm_couplingU_sub_le {K : ℕ} (w w' : Fin K → ℝ) : ‖couplingU w - couplingU w'‖ ≤ (Real.pi / 2 * ∑ j : Fin K, ‖pointerH j‖) * dist w w'

The Duhamel estimate for the coupling propagator: ‖couplingU w − couplingU w'‖ ≤ (π/2)·(Σⱼ‖hⱼ‖)·dist(w, w').

theorem CSD.RecordLayer.continuous_couplingU_entry {K : ℕ} (a b : Fin (K + 1)) : Continuous fun (w : Fin K → ℝ) => couplingU w a b

Each entry of the coupling propagator is a continuous function of the weight vector — Lipschitz via the Duhamel estimate and the staged entry bound. The statement mentions no matrix norm or matrix topology: it composes freely downstream.