The measured observable's Hamiltonian flow on Σ = ℂℙ^{N-1}

Category: 3-Local (The measured observable's Hamiltonian flow on Σ = ℂℙ^{N-1}).

The first physically-meaningful Φ ≠ id in the corpus. A measurement context is a choice of observable Â (the apparatus measures Â), diagonal diag(λ) in its eigenbasis. Its Hamiltonian flow on Σ is the one-parameter unitary group t ↦ exp(i t Â), acting on ℂℙ^{N-1} by obsFlow λ t [ψ] = [exp(i t Â) ψ].

This file establishes that obsFlow is a genuine measure-preserving deterministic flow whose conserved quantities are exactly the Born weights:

• obsFlow_measurePreserving — Φ preserves the Fubini–Study (typicality) measure, via the corpus's U(N)-invariance fubiniStudyMeasure_smul_invariant. So it is an admissible ontic flow (Liouville), unlike a generic relabeling.
• momentMap_obsFlow (headline) — the moment-map coordinates are invariant along the flow: momentMap (obsFlow λ t p) i = momentMap p i. Combined with momentMap_mk_eq_inner_sq (moment coordinate = Born weight ‖⟨eᵢ,ψ⟩‖²) and the Duistermaat–Heckman result (fs_born_volume_ratio_N, Born = FS-volume), this says: the Born weights are the constants of motion of the measured observable's own flow, and equal the typicality volumes. This is the concrete realisation of "the measurement context constrains the volumes in Σ."

Honest scope. The proof of conservation is light (the phases have modulus one). The content is the identification: a measure-preserving Φ ≠ id whose conserved quantities are the Born volumes (momentMap_obsFlow), tying the observable's dynamics to those volumes. The Φ ≠ id claim is now separately witnessed by obsFlow_ne_id (mirroring kFlow_ne_id): because obsFlow is a diagonal phase flow, every computational basis ray [eᵢ] is an eigenvector and is fixed, so the witness is necessarily a superposition ray — the |0⟩+|1⟩ ray, whose two coordinates pick up the distinct phases 1 and -1 (at lam := indicator of index 1, t := π), so its image (1,-1,0,…) is non-collinear with (1,1,0,…). What is not here is the measurement event — the flow conserves the populations (a non-disturbing / compatible measurement at the ontic level), it does not carry microstates into pointer regions and commit an outcome. That measurement-dynamics content is now built in the LF5 layer (CsdLean4/LF5/, single-system projective tier complete: measurementFlow ≠ id, measurement_flow_born_frequency, the per-microstate outcome function vnPointerOutcome); the deeper D1 strata (entangled de-isolation, instance-level dynamics) remain open.

noncomputable def CSD.LF4.obsPhase {N : ℕ} (lam : Fin N → ℝ) (t : ℝ) (i : Fin N) : ℂ

The unit-modulus phase exp(i t λᵢ) of the observable diag(λ) at time t.

Equations

• CSD.LF4.obsPhase lam t i = Complex.exp (Complex.I * ↑(t * lam i))

@[simp]

theorem CSD.LF4.obsPhase_norm {N : ℕ} (lam : Fin N → ℝ) (t : ℝ) (i : Fin N) : ‖obsPhase lam t i‖ = 1

The phase has modulus one (it lies on the unit circle).

theorem CSD.LF4.obsPhase_star_mul {N : ℕ} (lam : Fin N → ℝ) (t : ℝ) (i : Fin N) : star (obsPhase lam t i) * obsPhase lam t i = 1

The defining unitarity of each phase: star (phase) · phase = 1.

noncomputable def CSD.LF4.obsUnitary {N : ℕ} (lam : Fin N → ℝ) (t : ℝ) : ↥(Matrix.unitaryGroup (Fin N) ℂ)

The observable's unitary exp(i t Â) = diag(exp(i t λᵢ)) as an element of U(N).

Equations

• CSD.LF4.obsUnitary lam t = ⟨Matrix.diagonal (CSD.LF4.obsPhase lam t), ⋯⟩

@[simp]

theorem CSD.LF4.obsUnitary_val {N : ℕ} (lam : Fin N → ℝ) (t : ℝ) : ↑(obsUnitary lam t) = Matrix.diagonal (obsPhase lam t)

theorem CSD.LF4.obsUnitary_toEuclideanLin_apply {N : ℕ} (lam : Fin N → ℝ) (t : ℝ) (v : EuclideanSpace ℂ (Fin N)) (i : Fin N) : ((Matrix.toEuclideanLin ↑(obsUnitary lam t)) v).ofLp i = obsPhase lam t i * v.ofLp i

The observable's action on a Hilbert vector is the diagonal phase action.

theorem CSD.LF4.obsUnitary_normSq {N : ℕ} (lam : Fin N → ℝ) (t : ℝ) (v : EuclideanSpace ℂ (Fin N)) : ‖(Matrix.toEuclideanLin ↑(obsUnitary lam t)) v‖ ^ 2 = ‖v‖ ^ 2

The observable's flow is norm-preserving on the Hilbert space (it is unitary), in squared-norm form.

theorem CSD.LF4.obsUnitary_apply_ne_zero {N : ℕ} (lam : Fin N → ℝ) (t : ℝ) {v : EuclideanSpace ℂ (Fin N)} (hv : v ≠ 0) : (Matrix.toEuclideanLin ↑(obsUnitary lam t)) v ≠ 0

The diagonal phase action sends a nonzero vector to a nonzero vector.

noncomputable def CSD.LF4.obsFlow {N : ℕ} (lam : Fin N → ℝ) (t : ℝ) : CPN N → CPN N

The measured observable's Hamiltonian flow on Σ = ℂℙ^{N-1}: obsFlow λ t [ψ] = [exp(i t Â) ψ].

Equations

• CSD.LF4.obsFlow lam t p = CSD.LF4.obsUnitary lam t • p

theorem CSD.LF4.obsFlow_measurePreserving {N : ℕ} (lam : Fin N → ℝ) (t : ℝ) (p₀ : CPN N) : MeasureTheory.MeasurePreserving (obsFlow lam t) (Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (Matrix.UnitaryGroup.fubiniStudyMeasure p₀)

The flow preserves the Fubini–Study (typicality) measure — an admissible ontic flow (Liouville). Direct from the corpus's U(N)-invariance.

Non-triviality witness (Φ ≠ id)

def CSD.LF4.obsIdx0 {N : ℕ} (hN : 1 < N) : Fin N

Index 0 packaged with the 1 < N bound (avoids OfNat (Fin N) 0, no NeZero).

Equations

• CSD.LF4.obsIdx0 hN = ⟨0, ⋯⟩

def CSD.LF4.obsIdx1 {N : ℕ} (hN : 1 < N) : Fin N

Index 1 packaged with the 1 < N bound.

Equations

• CSD.LF4.obsIdx1 hN = ⟨1, hN⟩

theorem CSD.LF4.obsIdx0_ne_obsIdx1 {N : ℕ} (hN : 1 < N) : obsIdx0 hN ≠ obsIdx1 hN

noncomputable def CSD.LF4.obsLamWitness {N : ℕ} (hN : 1 < N) : Fin N → ℝ

The observable witnessing non-triviality: diag(λ) with λ = the indicator of index obsIdx1. At t = π its phases are exp(0) = 1 (index 0) and exp(iπ) = -1 (index 1).

Equations

• CSD.LF4.obsLamWitness hN i = if i = CSD.LF4.obsIdx1 hN then 1 else 0

noncomputable def CSD.LF4.obsTWitness : ℝ

The time witnessing non-triviality: t = π.

Equations

• CSD.LF4.obsTWitness = Real.pi

@[simp]

theorem CSD.LF4.obsPhase_obsLamWitness_zero {N : ℕ} (hN : 1 < N) : obsPhase (obsLamWitness hN) obsTWitness (obsIdx0 hN) = 1

@[simp]

theorem CSD.LF4.obsPhase_obsLamWitness_one {N : ℕ} (hN : 1 < N) : obsPhase (obsLamWitness hN) obsTWitness (obsIdx1 hN) = -1

noncomputable def CSD.LF4.obsWitnessVec {N : ℕ} (hN : 1 < N) : EuclideanSpace ℂ (Fin N)

The |0⟩ + |1⟩ superposition vector — a non-eigenvector of every diagonal phase flow (its two populated coordinates differ in phase under obsLamWitness/obsTWitness).

Equations

• CSD.LF4.obsWitnessVec hN = EuclideanSpace.single (CSD.LF4.obsIdx0 hN) 1 + EuclideanSpace.single (CSD.LF4.obsIdx1 hN) 1

theorem CSD.LF4.obsWitnessVec_apply_zero {N : ℕ} (hN : 1 < N) : (obsWitnessVec hN).ofLp (obsIdx0 hN) = 1

theorem CSD.LF4.obsWitnessVec_apply_one {N : ℕ} (hN : 1 < N) : (obsWitnessVec hN).ofLp (obsIdx1 hN) = 1

theorem CSD.LF4.obsWitnessVec_ne_zero {N : ℕ} (hN : 1 < N) : obsWitnessVec hN ≠ 0

theorem CSD.LF4.obsFlow_ne_id {N : ℕ} (hN : 1 < N) : obsFlow (obsLamWitness hN) obsTWitness ≠ id

The observable's flow is genuinely not the identity (for 1 < N). Because obsFlow is a diagonal phase flow, every computational basis ray [eᵢ] is an eigenvector and is fixed — so the witness must be a superposition. The |0⟩ + |1⟩ ray [obsWitnessVec] is moved: under obsLamWitness/obsTWitness its coordinates 0 and ⟨1,hN⟩ acquire the distinct phases 1 and -1, so the image coordinate vector (1,-1,…) is non-collinear with (1,1,…). Any c • v = (phase·v) forces c = 1 at coordinate 0 and c = -1 at coordinate ⟨1,hN⟩, a contradiction. Mirrors kFlow_ne_id's role as the named non-triviality witness.

theorem CSD.LF4.momentMap_obsFlow {N : ℕ} [NeZero N] (lam : Fin N → ℝ) (t : ℝ) (p : CPN N) (i : Fin N) : momentMap (obsFlow lam t p) i = momentMap p i

Headline: the Born weights are conserved along the observable's flow. The moment-map coordinates (= Born weights, momentMap_mk_eq_inner_sq) are invariant under obsFlow: momentMap (obsFlow λ t p) i = momentMap p i. The measured observable's own dynamics has the Born weights as its constants of motion.

D1c-2: the concrete base SectorData with a physically-meaningful Φ = obsFlow ≠ id

D1c-1 (LF4/KahlerFlow.lean, kSectorDataFlow) discharged the "Φ = id in the concrete Kähler instance" debt with a free T²-fibre translation kFlow: a genuine measure-preserving Φ ≠ id, but dynamically trivial — a fibre shift that acts as the identity on the actual projective state space. This block is the physically-meaningful strengthening: it rebuilds the base instance cpSectorData (Σ = P = ℂℙ^{N-1}, μL = fubiniStudyMeasure, π = id) with Φ := obsFlow lam t, the Hamiltonian flow t ↦ exp(i t Â) of a diagonal observable  = diag(λ) acting on the Fubini–Study Kähler base by obsFlow lam t [ψ] = [exp(i t Â) ψ]. This is dynamics on the real projective state space, not a trivial fibre shift.

Only the three flow-related OnticSetup fields change (Φ, hΦ_pres, and the derived measurable_Φ); μL, Ω0, and their hypotheses are reused verbatim from cpOnticSetup. The SectorData G = U(N)-action fields (measurable_smul_σ, measurable_smul_P, hμL_inv, hπ_equiv) are about the U(N)-action and π = id, never about Φ, so they are reused verbatim from cpSectorData (hμL_inv reads toOntic.μL, which is unchanged = fubiniStudyMeasure p₀).

Strictly stronger than D1c-1. kFlow is a free T²-fibre translation (kFlow_preserves_rays: it fixes every projective ray [ψ]); obsFlow is a Hamiltonian flow on the projective base, moving superposition rays (obsFlow_ne_id: the |0⟩+|1⟩ ray acquires distinct coordinate phases 1, -1). So D1c-2 gives the concrete base instance genuine physical dynamics on the actual Kähler state space.

Honest scope. obsFlow is a single observable's periodic phase flow. It is not the de-isolation / measurement flow Φ_vN (the dilated-space dynamics of LF5, the fuller deferred D1c content), and it is not ergodic / mixing (a periodic phase flow cannot be). SO-1 is untouched — D1c is necessary-but-not-sufficient for deriving the sector + Fubini–Study typicality from the dynamics: SO-1 additionally needs the flow ergodic / mixing to force μFS, which obsFlow is not. So D1c-2 supplies the concrete base instance with genuine physical dynamics; the SO-1 ergodicity content remains the open gap.

noncomputable def CSD.LF4.cpOnticSetupFlow {N : ℕ} [NeZero N] (p₀ : CPN N) (lam : Fin N → ℝ) (t : ℝ) : LF1.OnticSetup (CPN N)

The base OnticSetup with the physically-meaningful flow Φ := obsFlow lam t. Identical to cpOnticSetup p₀ except for the three flow fields: Φ is the observable's Hamiltonian flow on ℂℙ^{N-1}, hΦ_pres is obsFlow_measurePreserving (FS-invariance, genuine Liouville content, not MeasurePreserving.id). μL, Ω0, and their hypotheses are reused.

Equations

• CSD.LF4.cpOnticSetupFlow p₀ lam t = { μL := ⟨Matrix.UnitaryGroup.fubiniStudyMeasure p₀, ⋯⟩, Φ := CSD.LF4.obsFlow lam t, hΦ_pres := ⋯, Ω0 := Set.univ, hΩ0_meas := ⋯, hΩ0_nonzero := ⋯ }

noncomputable def CSD.LF4.cpSectorDataFlow {N : ℕ} [NeZero N] (p₀ : CPN N) (lam : Fin N → ℝ) (t : ℝ) : LF2.SectorData (CPN N) (CPN N) ↥(Matrix.unitaryGroup (Fin N) ℂ)

The concrete base SectorData carrying a physically-meaningful measure-preserving Φ ≠ id. Identical to cpSectorData p₀ except its underlying ontic data is cpOnticSetupFlow p₀ lam t (so Φ = obsFlow lam t, the observable's Hamiltonian flow on the Fubini–Study base). The G = U(N) action fields are reused verbatim from cpSectorData; none of them mention Φ.

Equations

• CSD.LF4.cpSectorDataFlow p₀ lam t = { toOntic := CSD.LF4.cpOnticSetupFlow p₀ lam t, π := id, measurable_π := ⋯, measurable_smul_σ := ⋯, measurable_smul_P := ⋯, hμL_inv := ⋯, hπ_equiv := ⋯ }

@[simp]

theorem CSD.LF4.cpSectorDataFlow_phi {N : ℕ} [NeZero N] (p₀ : CPN N) (lam : Fin N → ℝ) (t : ℝ) : (cpSectorDataFlow p₀ lam t).toOntic.Φ = obsFlow lam t

The instance's flow is exactly obsFlow lam t (definitional).

theorem CSD.LF4.cpSectorDataFlow_phi_ne_id {N : ℕ} [NeZero N] (p₀ : CPN N) (hN : 1 < N) : (cpSectorDataFlow p₀ (obsLamWitness hN) obsTWitness).toOntic.Φ ≠ id

D1c-2 headline. The concrete base SectorData genuinely carries a physically-meaningful Φ ≠ id: the observable's Hamiltonian flow exp(i t Â) on the Fubini–Study Kähler base ℂℙ^{N-1}. Strictly stronger than D1c-1's free T²-fibre translation (kSectorDataFlow_phi_ne_id), which fixes every projective ray. Reuses obsFlow_ne_id (witnesses obsLamWitness hN, obsTWitness).

theorem CSD.LF4.cpSectorDataFlow_phi_measurePreserving {N : ℕ} [NeZero N] (p₀ : CPN N) (lam : Fin N → ℝ) (t : ℝ) : MeasureTheory.MeasurePreserving (cpSectorDataFlow p₀ lam t).toOntic.Φ (Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (Matrix.UnitaryGroup.fubiniStudyMeasure p₀)

The instance's flow is measure-preserving for the Fubini–Study / Liouville volume fubiniStudyMeasure p₀ (the genuine hΦ_pres content surfaced on the SectorData).

theorem CSD.LF4.cpSectorDataFlow_frequency_convergence {N : ℕ} [NeZero N] (p₀ : CPN N) (lam : Fin N → ℝ) (t : ℝ) {Ω : Type u_1} [MeasurableSpace Ω] {Pr : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure Pr] (sample : ℕ → Ω → CPN N) (hsample : ∀ (n : ℕ), Measurable (sample n)) (hlaw : ∀ (n : ℕ), MeasureTheory.Measure.map (sample n) Pr = Matrix.UnitaryGroup.fubiniStudyMeasure p₀) {O : Set (CPN N)} (hO : MeasurableSet O) (hindep : Pairwise (Function.onFun (fun (f g : Ω → ℝ) => ProbabilityTheory.IndepFun f g Pr) fun (n : ℕ) => ((cpSectorDataFlow p₀ lam t).toOntic.Φ ∘ sample n ⁻¹' O).indicator fun (x : Ω) => 1)) : ∀ᵐ (ω : Ω) ∂Pr, Filter.Tendsto (fun (M : ℕ) => (∑ i ∈ Finset.range M, ((cpSectorDataFlow p₀ lam t).toOntic.Φ ∘ sample i ⁻¹' O).indicator (fun (x : Ω) => 1) ω) / ↑M) Filter.atTop (nhds ((Matrix.UnitaryGroup.fubiniStudyMeasure p₀) O).toReal)

Non-vacuity link to LF1. The LF1 deterministic-typicality theorem is non-vacuous on cpSectorDataFlow: for i.i.d. preparation draws, the empirical frequency of a measurable outcome region O evaluated on the states evolved by the instance's own flow (cpSectorDataFlow p₀ lam t).toOntic.Φ converges almost surely to the ontic volume ratio (fubiniStudyMeasure p₀ O).toReal. The moving flow that pins the limit is the SectorData's own physically-meaningful Φ = obsFlow lam t ≠ id, and obsFlow_measurePreserving is what makes law(obsFlow ∘ sampleₙ) = fubiniStudyMeasure p₀. LF1's freq_tendsto_of_iid is cited, not re-proved (the same route as kSectorDataFlow_frequency_convergence).