HY-5: routing the general-N Born frequencies through a deterministic Σ-flow

Category: 3-Local (routing the general-N Born frequencies through a deterministic Σ-flow).

The general-N Born-frequency capstones (born_frequency_convergence_N, povm_born_frequency_volume) run the strong law over i.i.d. trials sampled from the bare Fubini–Study measure on ℂℙ^{N-1} — the abstract SLLN engine, with no deterministic evolution. This is the Born-side analogue of the gap the W-series sigmaFlow fix closed on the Schrödinger side (a provenance audit found the Schrödinger chain consumed only the induced ray map, never the Σ-substrate flow).

This module closes it on the Born side: the trials are evolved by the sector's own deterministic flow before their outcome block is scored. Concretely, for the unitaryFlowSetup (M+1) U p₀ sector (Σ = ℂℙ^{N-1}, flow t = (U t • ·), a genuine Φ ≠ id for e.g. U = rotU, cf. rotationSetup_projectedFlow_ne_id), the empirical frequencies of the flow-image Born region converge a.s. to the Born weights. The flow's Liouville-preservation flow_preserves_volume (= the U(N)-invariance of μ_FS) is load-bearing: it pins the law of the evolved trials Φ_t ∘ X back to μ_FS, so the deterministic evolution does not spoil the typicality frequencies. The sector's flow/flow_preserves_volume fields are now consumed by the Born capstone, not just the abstract measure.

Deliverables

• unitaryFlowSetup_born_frequency_evolved — the general-N Born frequencies of trials evolved by the sector flow → ‖⟨eᵢ, ψ⟩‖²;
• povm_born_frequency_volume_evolved — the POVM analogue → P.weight ψ i.

Honest scope

This routes the Born capstone through the sector's deterministic flow, making flow_preserves_volume load-bearing (the Born-side sigmaFlow fix). It does NOT derive the Born weights from the flow, and the trials are still an i.i.d. sampling posit before evolution — the weights-from-dynamics problem (SO-1, the sector-origin problem; distinct from Paper C Axiom A5, the projectability condition) is untouched. Foundational-triple-only / Gleason-free (reuses born_frequency_convergence_N; nothing re-proved).

theorem CSD.LF4.unitaryFlowSetup_born_frequency_evolved {M : ℕ} (U : ℝ → ↥(Matrix.unitaryGroup (Fin (M + 1)) ℂ)) (p₀ : CPN (M + 1)) (t : ℝ) (ψ : EuclideanSpace ℂ (Fin (M + 1))) (hψ0 : ψ ≠ 0) (hψ : ‖ψ‖ = 1) (hpos : ∀ (j : Fin (M + 1)), 0 < ‖inner ℂ (EuclideanSpace.single j 1) ψ‖ ^ 2) {Ω : Type u_1} [MeasurableSpace Ω] {Pr : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure Pr] (X : ℕ → Ω → CPN (M + 1)) (hX : ∀ (n : ℕ), Measurable (X n)) (hlaw : ∀ (n : ℕ), MeasureTheory.Measure.map (X n) Pr = (unitaryFlowSetup (M + 1) U p₀).liouvilleMeasure) (hindep : ∀ (i : Fin (M + 1)), Pairwise (Function.onFun (fun (f g : Ω → ℝ) => ProbabilityTheory.IndepFun f g Pr) fun (n : ℕ) => ((unitaryFlowSetup (M + 1) U p₀).flow t ∘ X n ⁻¹' bornRegion ψ hψ0 i).indicator fun (x : Ω) => 1)) : ∀ᵐ (ω : Ω) ∂Pr, ∀ (i : Fin (M + 1)), Filter.Tendsto (fun (m : ℕ) => (∑ k ∈ Finset.range m, ((unitaryFlowSetup (M + 1) U p₀).flow t ∘ X k ⁻¹' bornRegion ψ hψ0 i).indicator (fun (x : Ω) => 1) ω) / ↑m) Filter.atTop (nhds (‖inner ℂ (EuclideanSpace.single i 1) ψ‖ ^ 2))

General-N Born frequencies of trials EVOLVED by the sector's deterministic flow. For any unitaryFlowSetup (M+1) U p₀ and time t, i.i.d. trials sampled from its liouvilleMeasure and then evolved by the sector's own flow Φ_t = (unitaryFlowSetup …).flow t have empirical frequencies of the Born region converging a.s. to the Born weights ‖⟨eᵢ, ψ⟩‖². The flow's Liouville-preservation (flow_preserves_volume, i.e. U(N)-invariance of μ_FS) pins the law of the evolved trials back to μ_FS — this is where the substrate flow becomes load-bearing on the Born side.

theorem CSD.LF4.povm_born_frequency_volume_evolved {M N : ℕ} {ι : Type u_1} [Fintype ι] [DecidableEq ι] (P : LF2.POVM N ι) (D : NaimarkDilation P) (ψ : EuclideanSpace ℂ (Fin N)) (e : Fin N × ι ≃ Fin (M + 1)) (ψ' : EuclideanSpace ℂ (Fin (M + 1))) (hψ'eq : ψ' = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin D.V) ψ)) (hψ'0 : ψ' ≠ 0) (hnorm : ‖ψ'‖ = 1) (hpos : ∀ (j : Fin (M + 1)), 0 < ‖inner ℂ (EuclideanSpace.single j 1) ψ'‖ ^ 2) (U : ℝ → ↥(Matrix.unitaryGroup (Fin (M + 1)) ℂ)) (p₀ : CPN (M + 1)) (t : ℝ) {Ω : Type u_2} [MeasurableSpace Ω] {Pr : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure Pr] (X : ℕ → Ω → CPN (M + 1)) (hX : ∀ (n : ℕ), Measurable (X n)) (hlaw : ∀ (n : ℕ), MeasureTheory.Measure.map (X n) Pr = (unitaryFlowSetup (M + 1) U p₀).liouvilleMeasure) (hindep : ∀ (j : Fin (M + 1)), Pairwise (Function.onFun (fun (f g : Ω → ℝ) => ProbabilityTheory.IndepFun f g Pr) fun (n : ℕ) => ((unitaryFlowSetup (M + 1) U p₀).flow t ∘ X n ⁻¹' bornRegion ψ' hψ'0 j).indicator fun (x : Ω) => 1)) : ∀ᵐ (ω : Ω) ∂Pr, ∀ (i : ι), Filter.Tendsto (fun (m : ℕ) => ∑ n : Fin N, (∑ k ∈ Finset.range m, ((unitaryFlowSetup (M + 1) U p₀).flow t ∘ X k ⁻¹' bornRegion ψ' hψ'0 (e (n, i))).indicator (fun (x : Ω) => 1) ω) / ↑m) Filter.atTop (nhds (P.weight ψ i))

POVM Born frequencies of trials EVOLVED by the sector's deterministic flow. The povm_born_frequency_volume capstone on trials evolved by the sector flow Φ_t: the empirical frequencies of the pointer blocks converge a.s. to the POVM weights P.weight ψ i. Same block-sum reduction as povm_born_frequency_volume, now on the flow-evolved trials via unitaryFlowSetup_born_frequency_evolved.