RecordLayer/SigmaLocalCoupling: the cell law from a Σ-local coupling

Category: 7-SigmaLayer (the record layer — the premise conversion for Posit 1, BACKLOG #152). TERM-SCOPE(Hamiltonian) — the vector-field sense, at the linear level; specs/TERMS.md.

CellLawForced.lean characterises the cell law by generation: a rate field whose rates are the normalised Hamiltonians of the coordinate phase rotations is the moment map. That premise is about the rates. This module moves the premise onto the measurement coupling, which is where a Σ-local account must put it, and proves the cell law from there.

The coupling

A Σ-local measurement couples the base (the calculation space ℂℙ^{N−1}, the state QM calculates with) to the fibre register through a product Hamiltonian H = Q_A(x) · p_R: a base observable times the register momentum. Hamilton's equations say the register drifts at speed Q_A(x) while the base is moved by the Hamiltonian flow of Q_A — the back-reaction BackReactionNecessity.lean shows a Σ-local measurement must have. Only the base operator A enters here: SigmaLocalCoupling N is a Hermitian A that is einselected in the context's basis, i.e. commutes with every coordinate projector |eᵢ⟩⟨eᵢ| (pointer_invariant_iff_commute: the pointer observables of an interaction are exactly the ones commuting with it).

What is proved

• A_eq_diagonal: einselection makes A diagonal, with real spectrum eig (Hermitian).

• ★★ baseGen_eq_sum: the base generator Q_A = ½ re⟪x, Ax⟫ is ∑ λᵢ · coordEnergy i — a torus Hamiltonian; and ★★ fundamentalForm_torusField: its Hamiltonian vector field is the torus field ∑ λᵢ • phaseGen i. Einselection makes the back-reaction generate the context's torus action, at the eigenvalue speeds. This is Posit 1's "the dynamics generates the torus action", as a theorem given einselection.

• ★ drift_eq_sum_momentMap: the degree-0 drift of the register is the eigenvalue average under the moment map, ⟨A⟩ = ∑ λᵢ Φᵢ.

• ★★★ isCalibrated_forall_iff: a rate field is calibrated against a coupling when the rate-weighted average of the outcome labels (the eigenvalues) equals the register's drift. A rate field calibrated against every einselected coupling is the moment map, and conversely. The forward direction needs only the N projector couplings.

• ★★★ isTorusGenerated_of_calibrated / rate_eq_momentMap_of_calibrated: the context field so calibrated is torus-generated and its rates are the moment map — the premise conversion:

  Posit 1 ⟸ (Σ-local product coupling) ∧ (einselected in the context's basis) ∧ (readout calibrated to the drift for every such coupling).

⚠️ What "the rates read off the coupling" had to mean, and why

The row's phrasing asked for IsGeneratedRateField "for the rates read off the coupling". The obvious reading — divide the i-th summand λᵢ · coordEnergy i by its speed λᵢ and normalise — is vacuous: the unit-speed outcome generator is coordEnergy i whatever the coupling is, so no coupling is consulted and the conclusion is isTorusGenerated_momentContext again. That is recorded here as a finding. The non-vacuous reading is calibration: the labelled readout (outcome i labelled by the eigenvalue λᵢ, the pointer displacement when the system is the eigenstate) averages, over the ontic fibre, to what the coupling actually does to the register. It says nothing about any single outcome's weight; it constrains the mean for each coupling in the context's commutant, and that is enough. The principle is the author's to accept or reword; the Lean content is the equivalence.

Honest scope

• The fibre half is prose. H = Q_A · p_R and q̇_R = Q_A are Hamilton's equations on the arena, whose manifold flow is R-016's business; this module uses only the base operator.
• Which coupling an apparatus realises is R-015, a boundary; the class is named, not derived.
• Linear level, as CellLawForced.lean: fundamentalForm, phaseGen and quadraticEnergy on ℂᴺ, with the ray-level statements through momentMap.

References: specs/BACKLOG.md #152, #151, #19; specs/POSITS.md Posit 1; RecordLayer/CellLawForced.lean (IsPhaseHamiltonian, coordEnergy, phaseGen, generatedRateField_eq_momentMap); RecordLayer/BackReactionNecessity.lean; Empirical/CSD/PointerCommutation.lean (pointer_invariant_iff_commute); Mathlib/Analysis/InnerProductSpace/HamiltonianVectorField.lean (quadraticEnergy_hamiltonian_duality); specs/way-theorem-scoping.md (brick 2, the premise-conversion precedent).

The coupling, by its base operator

structure CSD.RecordLayer.SigmaLocalCoupling (N : ℕ) : Type

A Σ-local product coupling H = Q_A(x) · p_R, recorded by its base operator: a Hermitian matrix on the context's Hilbert space, einselected in the context's basis — it commutes with every coordinate projector |eᵢ⟩⟨eᵢ| = Matrix.single i i 1.

• A : Matrix (Fin N) (Fin N) ℂ

  The base operator.

• hermitian : self.A.IsHermitian

  The base operator is Hermitian.

• einselected (i : Fin N) : Commute (Matrix.single i i 1) self.A

  The context's basis is the pointer basis: every coordinate projector commutes with A.

theorem CSD.RecordLayer.apply_of_ne_of_commute_single {N : ℕ} {A : Matrix (Fin N) (Fin N) ℂ} (hA : ∀ (i : Fin N), Commute (Matrix.single i i 1) A) {i j : Fin N} (h : i ≠ j) : A i j = 0

A matrix commuting with every coordinate projector has no off-diagonal entries.

theorem CSD.RecordLayer.SigmaLocalCoupling.apply_of_ne {N : ℕ} (S : SigmaLocalCoupling N) {i j : Fin N} (h : i ≠ j) : S.A i j = 0

Einselection kills the off-diagonal entries.

noncomputable def CSD.RecordLayer.SigmaLocalCoupling.eig {N : ℕ} (S : SigmaLocalCoupling N) (i : Fin N) : ℝ

The spectrum: the diagonal, real because A is Hermitian.

Equations

• S.eig i = RCLike.re (S.A i i)

theorem CSD.RecordLayer.SigmaLocalCoupling.A_apply_self {N : ℕ} (S : SigmaLocalCoupling N) (i : Fin N) : S.A i i = ↑(S.eig i)

theorem CSD.RecordLayer.SigmaLocalCoupling.A_eq_diagonal {N : ℕ} (S : SigmaLocalCoupling N) : S.A = Matrix.diagonal fun (i : Fin N) => ↑(S.eig i)

Einselection makes the base operator diagonal, with spectrum eig.

noncomputable def CSD.RecordLayer.SigmaLocalCoupling.op {N : ℕ} (S : SigmaLocalCoupling N) : EuclideanSpace ℂ (Fin N) →L[ℂ] EuclideanSpace ℂ (Fin N)

The base operator as an operator on the context's Hilbert space.

Equations

• S.op = Matrix.toEuclideanCLM S.A

theorem CSD.RecordLayer.SigmaLocalCoupling.op_symm {N : ℕ} (S : SigmaLocalCoupling N) (u v : EuclideanSpace ℂ (Fin N)) : inner ℂ (S.op u) v = inner ℂ u (S.op v)

theorem CSD.RecordLayer.SigmaLocalCoupling.op_apply {N : ℕ} (S : SigmaLocalCoupling N) (x : EuclideanSpace ℂ (Fin N)) (i : Fin N) : (S.op x).ofLp i = ↑(S.eig i) * x.ofLp i

The operator acts coordinatewise by the spectrum.

The base generator is a torus Hamiltonian

noncomputable def CSD.RecordLayer.SigmaLocalCoupling.baseGen {N : ℕ} (S : SigmaLocalCoupling N) : EuclideanSpace ℂ (Fin N) → ℝ

The base generator Q_A(x) = ½ re⟪x, A x⟫: the base observable of the coupling, whose Hamiltonian flow is the back-reaction and whose value is the register's drift.

Equations

• S.baseGen = Kahler.quadraticEnergy S.op

theorem CSD.RecordLayer.SigmaLocalCoupling.baseGen_eq_sum {N : ℕ} (S : SigmaLocalCoupling N) (x : EuclideanSpace ℂ (Fin N)) : S.baseGen x = ∑ i : Fin N, S.eig i * coordEnergy i x

★★ Einselection ⇒ the base generator is a torus Hamiltonian: Q_A = ∑ λᵢ · coordEnergy i.

theorem CSD.RecordLayer.SigmaLocalCoupling.fundamentalForm_torusField {N : ℕ} (S : SigmaLocalCoupling N) (x v : EuclideanSpace ℂ (Fin N)) : Kahler.fundamentalForm (∑ i : Fin N, S.eig i • phaseGen i x) v = (fderiv ℝ S.baseGen x) v

★★ Einselection ⇒ the back-reaction is the torus flow at the eigenvalue speeds: the Hamiltonian vector field of the base generator is ∑ λᵢ • phaseGen i, i.e. ι_{∑ λᵢ X_i} ω = dQ_A.

Drift and calibration

noncomputable def CSD.RecordLayer.SigmaLocalCoupling.drift {N : ℕ} (S : SigmaLocalCoupling N) (p : LF4.CPN N) : ℝ

The drift: the base generator normalised to degree 0, the register's speed per unit momentum as a function of the ray — ⟨A⟩ at a unit representative.

Equations

• S.drift p = S.baseGen (Projectivization.rep p) / (‖Projectivization.rep p‖ ^ 2 / 2)

theorem CSD.RecordLayer.SigmaLocalCoupling.drift_eq_sum_momentMap {N : ℕ} (S : SigmaLocalCoupling N) (p : LF4.CPN N) : S.drift p = ∑ i : Fin N, S.eig i * Projectivization.momentMap p i

★ The drift is the eigenvalue average under the moment map: ⟨A⟩ = ∑ λᵢ Φᵢ.

def CSD.RecordLayer.SigmaLocalCoupling.IsCalibrated {N : ℕ} (rate : LF4.CPN N → Fin N → ℝ) (S : SigmaLocalCoupling N) : Prop

A rate field is calibrated against the coupling S when the rate-weighted average of the outcome labels (the eigenvalues) is the register's drift, at every preparation.

Equations

• CSD.RecordLayer.SigmaLocalCoupling.IsCalibrated rate S = ∀ (p : CSD.LF4.CPN N), ∑ i : Fin N, rate p i * S.eig i = S.drift p

noncomputable def CSD.RecordLayer.SigmaLocalCoupling.ofDiagonal {N : ℕ} (d : Fin N → ℝ) : SigmaLocalCoupling N

The diagonal coupling with real spectrum d — in particular the projector couplings d = Pi.single j 1.

Equations

• CSD.RecordLayer.SigmaLocalCoupling.ofDiagonal d = { A := Matrix.diagonal fun (i : Fin N) => ↑(d i), hermitian := ⋯, einselected := ⋯ }

theorem CSD.RecordLayer.SigmaLocalCoupling.eig_ofDiagonal {N : ℕ} (d : Fin N → ℝ) (i : Fin N) : (ofDiagonal d).eig i = d i

theorem CSD.RecordLayer.isCalibrated_forall_iff {N : ℕ} (rate : LF4.CPN N → Fin N → ℝ) : (∀ (S : SigmaLocalCoupling N), SigmaLocalCoupling.IsCalibrated rate S) ↔ rate = Projectivization.momentMap

★★★ The cell law is forced by calibration. A rate field calibrated against every einselected coupling is the moment map, and the moment map is calibrated against every such coupling. The forward direction uses only the N projector couplings.

theorem CSD.RecordLayer.rate_eq_momentMap_of_calibrated {N : ℕ} (c : ContextField N) (h : ∀ (S : SigmaLocalCoupling N), SigmaLocalCoupling.IsCalibrated c.rate S) (p : LF4.CPN N) (i : Fin N) : c.rate p i = Projectivization.momentMap p i

★★★ The premise conversion for Posit 1: a context field calibrated against every einselected Σ-local coupling has the moment map for its rates.

theorem CSD.RecordLayer.isTorusGenerated_of_calibrated {N : ℕ} (c : ContextField N) (h : ∀ (S : SigmaLocalCoupling N), SigmaLocalCoupling.IsCalibrated c.rate S) : IsTorusGenerated c

★★★ A context field calibrated against every einselected Σ-local coupling is torus-generated: calibration implies generation.