LF5: the measurement-flow capstone on the canonical i.i.d. FS trial witness

Category: 3-Local (LF5 measurement-dynamics layer, trial-witness tranche).

measurement_flow_born_frequency (LF5-E) quantifies over an abstract i.i.d. trial bundle (Ω, Pr, X, hX, hlaw, hindep) on the dilated sector ℂℙ^{N·N−1}. This module discharges that bundle with the canonical coordinate process of CsdLean4/LF4/TrialWitness.lean (fsTrialMeasure p₀ = Measure.infinitePi (fun _ => fubiniStudyMeasure p₀), fsTrial (M + 1) n = (· n)): the canonical capstone quantifies only over the measurement context (hN, e), the preparation (ψ, hψ), the dilated state (ψ', hψ'eq, hψ'0), and the reference point p₀. The five-conjunct conclusion is verbatim that of measurement_flow_born_frequency with Pr := fsTrialMeasure p₀ and X := fsTrial (M + 1).

Honest scope

As in TrialWitness.lean: this is the measure-theoretic existence of the i.i.d. sampling law, turning the LF5-E hypothesis set from classically satisfiable into Lean-inhabited. The physical reading of repeated preparation as i.i.d. FS-typical draws on the dilated sector remains the LF1 typicality posit (SO-1, here on Σ'); the canonical process does not derive it. Foundational-triple-only, Gleason-free.

theorem CSD.LF5.measurement_flow_born_frequency_canonical {N M : ℕ} [NeZero N] (hN : 1 < N) (e : Fin N × Fin N ≃ Fin (M + 1)) (ψ : EuclideanSpace ℂ (Fin N)) (hψ : ‖ψ‖ = 1) (ψ' : EuclideanSpace ℂ (Fin (M + 1))) (hψ'eq : ψ' = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin (vnDilationV N)) ψ)) (hψ'0 : ψ' ≠ 0) (p₀ : LF4.CPN (M + 1)) : measurementFlow N e ≠ id ∧ MeasureTheory.MeasurePreserving (measurementFlow N e) (Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (Matrix.UnitaryGroup.fubiniStudyMeasure p₀) ∧ (∀ (φ : EuclideanSpace ℂ (Fin N)) (hφ : φ ≠ 0), measurementFlow N e (Projectivization.mk ℂ ((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin (embedGround N)) φ)) ⋯) = Projectivization.mk ℂ ((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin (vnDilationV N)) φ)) ⋯) ∧ (∀ (i : Fin N), ‖inner ℂ (EuclideanSpace.single i 1) ψ‖ ^ 2 = ∑ n : Fin N, ((Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (LF4.bornRegion ψ' hψ'0 (e (n, i)))).toReal) ∧ ∀ᵐ (ω : LF4.fsTrialSpace (M + 1)) ∂LF4.fsTrialMeasure p₀, ∀ (i : Fin N), Filter.Tendsto (fun (m : ℕ) => ∑ n : Fin N, (∑ k ∈ Finset.range m, (LF4.fsTrial (M + 1) k ⁻¹' LF4.bornRegion ψ' hψ'0 (e (n, i))).indicator (fun (x : LF4.fsTrialSpace (M + 1)) => 1) ω) / ↑m) Filter.atTop (nhds (‖inner ℂ (EuclideanSpace.single i 1) ψ‖ ^ 2))

The LF5-E capstone on the canonical i.i.d. FS trial witness. All five conjuncts of measurement_flow_born_frequency, with the trial bundle discharged by the canonical process: only the measurement context, the preparation, the dilated state, and the FS reference point remain as hypotheses.