SigmaLayer/DynamicsBridge: projectable dynamics and its Hamiltonian realisation

Category: 7-SigmaLayer (the projective-sector layer (Paper C)).

Bridge assumption B2: the ontic flow is projectable through pi (there is an induced flow on the projective sector). ProjectiveDynamicsBridge bundles the projected flow, its one-parameter-group laws and the projectability equation. For the concrete product model (productDynamics/productSector) the projected flow is exp(-itH)-conjugation on rays, so it is projectable AND has a Hamiltonian realisation: theorem target T5 (HasHamiltonianRealisation) is inhabited for this concrete model, reusing manyToOneSchrodingerSetup_schrodinger_form and expNegITH_unitary_group.

Unitarity of the projected flow is NOT a field of ProjectiveSector; it is the separate target HasUnitaryRealisation / HasHamiltonianRealisation, proved only where a concrete model supplies it.

Consistency witness, not derivation. The concrete model's isolated flow is Φ_t = (e^{-itH}·[p], θ) — unitary Schrödinger evolution is built IN — so "the projected flow is exp(-itH)" is a compatibility fact about the witness, NOT a derivation of unitary dynamics from a fibre-primitive Hamiltonian vector field (Paper C A2/A5, the quantum-effective projectability). The W-series (LF4/PhaseLift.lean) derives the exp(-itH) form from the sector interface + regularity data as a separate, forward result; here it is exhibited on the witness. The sector's own origin remains SO-1 (specs/reconstruction-status.md §7).

structure CSD.SigmaLayer.ProjectiveDynamicsBridge {N : ℕ} {Sigma : Type u} [MeasurableSpace Sigma] {D : ConstraintDynamics Sigma} (Q : ProjectiveSector N D) : Type

Projective dynamics bridge (B2 interface). The projected flow, its measurability, the projectability equation pi (flow t x) = projectedFlow t (pi x), and the one-parameter-group laws of the projected flow.

• projectedFlow : OnticTime → ProjectiveState N → ProjectiveState N

  The induced flow on the projective sector.

• measurable_projectedFlow (t : OnticTime) : Measurable (self.projectedFlow t)

  Each projected time-t map is measurable.

• projectable (t : OnticTime) (x : Sigma) : Q.pi (D.flow t x) = self.projectedFlow t (Q.pi x)

  The ontic flow descends through pi to the projected flow.

• projected_zero (p : ProjectiveState N) : self.projectedFlow 0 p = p

  The projected flow is the identity at time 0.

• projected_add (s t : OnticTime) (p : ProjectiveState N) : self.projectedFlow (s + t) p = self.projectedFlow s (self.projectedFlow t p)

  The projected flow composes additively in time.

The concrete product instance: projectable, Hamiltonian-realised

noncomputable def CSD.SigmaLayer.productProjectedFlow {M : ℕ} (H : Matrix (Fin (M + 1)) (Fin (M + 1)) ℂ) (hH : H.IsHermitian) : OnticTime → ProjectiveState (M + 1) → ProjectiveState (M + 1)

The projected flow of the product model: exp(-itH)-conjugation on rays.

Equations

• CSD.SigmaLayer.productProjectedFlow H hH t p = CSD.LF4.schrodingerUnitary hH t • p

noncomputable def CSD.SigmaLayer.productDynamicsBridge {M : ℕ} (H : Matrix (Fin (M + 1)) (Fin (M + 1)) ℂ) (hH : H.IsHermitian) (p₀ : LF4.CPN (M + 1)) : ProjectiveDynamicsBridge (productSector H hH p₀)

The product model is projectable with exp(-itH)-conjugation as its projected flow (B2 proved). The ontic flow descends through pi = Prod.fst to exp(-itH) • ·, with the projected group laws from expNegITH_unitary_group.

Equations

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

theorem CSD.SigmaLayer.productProjectedFlow_hasHamiltonianRealisation {M : ℕ} (H : Matrix (Fin (M + 1)) (Fin (M + 1)) ℂ) (hH : H.IsHermitian) : HasHamiltonianRealisation (productProjectedFlow H hH)

T5 inhabited for the product model: the projected flow has a Hamiltonian realisation. The projected flow is generated by the Hermitian H via exp(-itH); a concrete inhabitant of HasHamiltonianRealisation, not a postulate.

theorem CSD.SigmaLayer.productProjectedFlow_hasUnitaryRealisation {M : ℕ} (H : Matrix (Fin (M + 1)) (Fin (M + 1)) ℂ) (hH : H.IsHermitian) : HasUnitaryRealisation (productProjectedFlow H hH)

T4 inhabited for the product model: the projected flow has a unitary realisation. The Hamiltonian realisation is in particular a unitary realisation.