SigmaLayer/HamiltonianSignature: A2's formalisable half

Category: 7-SigmaLayer (Paper C A2 — Hamiltonian ontic dynamics).

The split, stated up front

A2 as written — the ontic flow is generated by a Hamiltonian vector field X_H = ω⁻¹dH — needs the symplectic form and the exterior derivative, which is the §2a-scoped manifold gap (verified a tooling gap, not a falsity: the statement is standard Kähler geometry). What a measure space can express is the signature a Hamiltonian flow leaves behind, and this module proves the witness flow has every piece of it:

1. A canonical conserved energy. onticEnergy H — the expectation re⟨ψ_p, H ψ_p⟩/‖ψ_p‖² at the base point — is well-defined on rays and conserved by the witness flow (onticEnergy_flow_invariant): the flow conserves its own generator, the first Hamiltonian signature.
2. The A5 junction. onticEnergy H is fibre-independent by construction, so it is EpsProjectable _ 0 — it is the canonical h of the exact case H = h∘π (onticEnergy_epsProjectable). A2's conserved energy and A5's projectable Hamiltonian are the same object, as they should be.
3. The commuting phase torus. The diagonal-phase unitaries form an additive (hence commuting) action that preserves every moment-map coordinate (momentMap_phaseDiag_invariant, phaseDiag_add) — the flow-level shadow of "the moment map generates the torus action". The fibre half of the torus signature is the translation flows of ShearWitness.lean (pshift, measure-preserving), already in place.

Together with the already-proved Liouville property (ConstraintDynamics.flow_preserves) and group laws, the honest claim is: every property of "Hamiltonian flow" expressible without the manifold API is proved of the witness flow; the vector-field equation itself is scoped. With this, A2's unscoped content is discharged; what remains of A2 is exactly its §2a-scoped half.

References

SigmaLayer/ApproxProjectability.lean (EpsProjectable — the A5 junction); SigmaLayer/MeasureBridge.lean (productDynamics — the witness flow); LF4/ProjectedDynamics.lean (schrodingerUnitary, schrodingerGen); LF4/MomentMap.lean (momentMap); specs/reconstruction-status.md §2a.

The canonical ontic energy

noncomputable def CSD.RecordLayer.baseEnergy {N : ℕ} (H : Matrix (Fin N) (Fin N) ℂ) (p : LF4.CPN N) : ℝ

The energy at a base point: the expectation of H in the ray's representative, normalised. Well-defined on rays by baseEnergy_mk.

Equations

• CSD.RecordLayer.baseEnergy H p = RCLike.re (inner ℂ (Projectivization.rep p) ((Matrix.toEuclideanLin H) (Projectivization.rep p))) / ‖Projectivization.rep p‖ ^ 2

noncomputable def CSD.RecordLayer.onticEnergy {N : ℕ} (H : Matrix (Fin N) (Fin N) ℂ) : LF4.KSigma N → ℝ

The canonical ontic energy of a Hamiltonian: the base-point expectation, lifted to Σ. Fibre-independent by construction — see onticEnergy_epsProjectable.

Equations

• CSD.RecordLayer.onticEnergy H x = CSD.RecordLayer.baseEnergy H x.1

theorem CSD.RecordLayer.energyRatio_smul {N : ℕ} (H : Matrix (Fin N) (Fin N) ℂ) (c : ℂ) (hc : c ≠ 0) (v : EuclideanSpace ℂ (Fin N)) : RCLike.re (inner ℂ (c • v) ((Matrix.toEuclideanLin H) (c • v))) / ‖c • v‖ ^ 2 = RCLike.re (inner ℂ v ((Matrix.toEuclideanLin H) v)) / ‖v‖ ^ 2

The energy ratio is scale-invariant — the well-definedness computation.

theorem CSD.RecordLayer.baseEnergy_mk {N : ℕ} (H : Matrix (Fin N) (Fin N) ℂ) (ψ : EuclideanSpace ℂ (Fin N)) (hψ : ψ ≠ 0) : baseEnergy H (Projectivization.mk ℂ ψ hψ) = RCLike.re (inner ℂ ψ ((Matrix.toEuclideanLin H) ψ)) / ‖ψ‖ ^ 2

The energy is well-defined on rays: at [ψ] it is the normalised expectation in ψ.

Conservation under commuting unitaries, hence under the flow

theorem CSD.RecordLayer.inner_toEuclideanLin_adjoint' {N : ℕ} (W : Matrix (Fin N) (Fin N) ℂ) (x y : EuclideanSpace ℂ (Fin N)) : inner ℂ ((Matrix.toEuclideanLin W) x) y = inner ℂ x ((Matrix.toEuclideanLin (star W)) y)

Adjoint move for the matrix action (general-N form of the corpus's inner_toEuclideanLin_adjoint).

theorem CSD.RecordLayer.toEuclideanLin_mul_apply {N : ℕ} (A B : Matrix (Fin N) (Fin N) ℂ) (v : EuclideanSpace ℂ (Fin N)) : (Matrix.toEuclideanLin A) ((Matrix.toEuclideanLin B) v) = (Matrix.toEuclideanLin (A * B)) v

Matrix multiplication composes through toEuclideanLin, pointwise.

theorem CSD.RecordLayer.baseEnergy_smul_invariant {N : ℕ} (H : Matrix (Fin N) (Fin N) ℂ) (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (hcomm : ↑U * H = H * ↑U) (p : LF4.CPN N) : baseEnergy H (U • p) = baseEnergy H p

Energy is invariant under any unitary commuting with H — the algebraic core of conservation.

theorem CSD.RecordLayer.onticEnergy_flow_invariant {M : ℕ} (H : Matrix (Fin (M + 1)) (Fin (M + 1)) ℂ) (hH : H.IsHermitian) (p₀ : LF4.CPN (M + 1)) (t : ℝ) (x : LF4.KSigma (M + 1)) : onticEnergy H ((SigmaLayer.productDynamics H hH p₀).flow t x) = onticEnergy H x

★ The witness flow conserves its own generator — the first Hamiltonian signature. The Schrödinger unitary is exp((-it)·H), which commutes with H, so baseEnergy_smul_invariant applies at every time.

theorem CSD.RecordLayer.onticEnergy_epsProjectable {N : ℕ} (H : Matrix (Fin N) (Fin N) ℂ) : EpsProjectable (onticEnergy H) 0

★ The A5 junction: the conserved energy is exactly projectable. onticEnergy H depends on the base point alone, so it is EpsProjectable _ 0 — it is the canonical h of the exact case H = h∘π. A2's conserved quantity and A5's projectable Hamiltonian are the same object.

The commuting phase torus

noncomputable def CSD.RecordLayer.phaseDiag {N : ℕ} (φ : Fin N → ℝ) : ↥(Matrix.unitaryGroup (Fin N) ℂ)

The diagonal-phase unitary diag(e^{iφ₀}, …, e^{iφ_{N-1}}).

Equations

• CSD.RecordLayer.phaseDiag φ = ⟨Matrix.diagonal fun (k : Fin N) => Complex.exp (Complex.I * ↑(φ k)), ⋯⟩

theorem CSD.RecordLayer.phaseDiag_add {N : ℕ} (φ φ' : Fin N → ℝ) : phaseDiag (φ + φ') = phaseDiag φ * phaseDiag φ'

The phase flows are additive, hence commute — the abelian-torus half of the signature.

theorem CSD.RecordLayer.phaseDiag_comm {N : ℕ} (φ φ' : Fin N → ℝ) : phaseDiag φ * phaseDiag φ' = phaseDiag φ' * phaseDiag φ

theorem CSD.RecordLayer.momentMap_phaseDiag_invariant {N : ℕ} (φ : Fin N → ℝ) (p : LF4.CPN N) (k : Fin N) : LF4.momentMap (phaseDiag φ • p) k = LF4.momentMap p k

★ The phase torus preserves every moment-map coordinate — the flow-level shadow of "the moment map generates the torus action" (the generating statement itself needs the symplectic form and is §2a-scoped).