LF4: the canonical i.i.d. FS trial witness

Category: 3-Local (LF4 Born-from-Kähler-volume engine, trial-witness tranche).

Every capstone of the volume-frequency series (born_frequency_convergence_N / _uncond, povm_born_frequency_volume, the LF5 measurement_flow_born_frequency, the Empirical/CSD/*Volume witnesses) quantifies over an abstract i.i.d. trial bundle (Ω, Pr, X, hX, hlaw, hindep). Until this file no corpus theorem constructed such a process: the hypothesis set was classically satisfiable (standard product-measure existence) but not Lean-inhabited. This file closes that vacuity-shaped residue:

• fsTrialSpace / fsTrialMeasure / fsTrial — the canonical process Ω = ℕ → ℂℙ^{N-1}, Pr = Measure.infinitePi (fun _ => fubiniStudyMeasure p₀), X n = (· n), with marginal law fubiniStudyMeasure p₀ (fsTrial_law, via Measure.infinitePi_map_eval), joint independence (fsTrial_iIndepFun, via iIndepFun_eval_infinitePi), and the pairwise indicator independence in exactly the capstone shape (fsTrial_pairwise_indepFun_indicator).
• born_frequency_convergence_N_canonical — the unconditional general-N Born-frequency capstone applied to the canonical process: the statement quantifies only over (p₀, ψ, hψ0, hψ); the entire trial bundle is discharged. The conclusion is verbatim that of born_frequency_convergence_N_uncond with Pr := fsTrialMeasure p₀ and X := fsTrial.

The LF5 analogue (measurement_flow_born_frequency_canonical) lives in CsdLean4/LF5/CapstoneCanonical.lean (LF5 imports LF4, not conversely).

Honest scope

This is the measure-theoretic existence of the i.i.d. sampling law: the canonical product-measure process witnesses that the trial hypotheses are mutually consistent and realisable inside Lean. The physical reading of repeated preparation as i.i.d. FS-typical draws remains the LF1 typicality posit (the posited-sector / typicality datum (SO-1)); constructing the process does not derive that posit. Foundational-triple-only; Gleason-free (no busch_effect_gleason).

@[reducible, inline]

abbrev CSD.LF4.fsTrialSpace (N : ℕ) : Type

The canonical trial space for FS-typical sampling on ℂℙ^{N-1}: infinite sequences of projective points, one per trial.

Equations

• CSD.LF4.fsTrialSpace N = (ℕ → CSD.LF4.CPN N)

noncomputable def CSD.LF4.fsTrialMeasure {N : ℕ} (p₀ : CPN N) : MeasureTheory.Measure (fsTrialSpace N)

The canonical trial measure: the infinite product of fubiniStudyMeasure p₀ over the trial index. The i.i.d. sampling law itself.

Equations

• CSD.LF4.fsTrialMeasure p₀ = MeasureTheory.Measure.infinitePi fun (x : ℕ) => Matrix.UnitaryGroup.fubiniStudyMeasure p₀

instance CSD.LF4.instIsProbabilityMeasureFsTrialMeasure {N : ℕ} (p₀ : CPN N) : MeasureTheory.IsProbabilityMeasure (fsTrialMeasure p₀)

def CSD.LF4.fsTrial (N n : ℕ) : fsTrialSpace N → CPN N

The canonical trial process: trial n reads coordinate n.

Equations

• CSD.LF4.fsTrial N n ω = ω n

theorem CSD.LF4.fsTrial_measurable {N : ℕ} (n : ℕ) : Measurable (fsTrial N n)

Each canonical trial is measurable (hX).

theorem CSD.LF4.fsTrial_law {N : ℕ} (p₀ : CPN N) (n : ℕ) : MeasureTheory.Measure.map (fsTrial N n) (fsTrialMeasure p₀) = Matrix.UnitaryGroup.fubiniStudyMeasure p₀

Each canonical trial has law fubiniStudyMeasure p₀ (hlaw).

theorem CSD.LF4.fsTrial_iIndepFun {N : ℕ} (p₀ : CPN N) : ProbabilityTheory.iIndepFun (fsTrial N) (fsTrialMeasure p₀)

The canonical trials are jointly independent.

theorem CSD.LF4.fsTrial_pairwise_indepFun_indicator {N : ℕ} (p₀ : CPN N) {ι : Type u_1} (S : ι → Set (CPN N)) (hS : ∀ (i : ι), MeasurableSet (S i)) (i : ι) : Pairwise (Function.onFun (fun (f g : fsTrialSpace N → ℝ) => ProbabilityTheory.IndepFun f g (fsTrialMeasure p₀)) fun (n : ℕ) => (fsTrial N n ⁻¹' S i).indicator fun (x : fsTrialSpace N) => 1)

Pairwise independence of the per-trial outcome-region indicators, for any family of measurable regions — the exact hindep shape every volume-frequency capstone consumes.

theorem CSD.LF4.born_frequency_convergence_N_canonical {M : ℕ} (p₀ : CPN (M + 1)) (ψ : EuclideanSpace ℂ (Fin (M + 1))) (hψ0 : ψ ≠ 0) (hψ : ‖ψ‖ = 1) : ∀ᵐ (ω : fsTrialSpace (M + 1)) ∂fsTrialMeasure p₀, ∀ (i : Fin (M + 1)), Filter.Tendsto (fun (m : ℕ) => (∑ k ∈ Finset.range m, (fsTrial (M + 1) k ⁻¹' bornRegion ψ hψ0 i).indicator (fun (x : fsTrialSpace (M + 1)) => 1) ω) / ↑m) Filter.atTop (nhds (‖inner ℂ (EuclideanSpace.single i 1) ψ‖ ^ 2))

General-N Born-frequency convergence on the canonical i.i.d. FS process. born_frequency_convergence_N_uncond with the trial bundle discharged by the canonical witness: the statement quantifies only over the reference point p₀ and the preparation (ψ, hψ0, hψ). The conclusion is verbatim the original's with Pr := fsTrialMeasure p₀, X := fsTrial (M + 1). Foundational-triple-only, Gleason-free.

theorem CSD.LF4.povm_born_frequency_volume_canonical {N : ℕ} {ι : Type u_1} [Fintype ι] [DecidableEq ι] {M : ℕ} (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) (p₀ : CPN (M + 1)) : ∀ᵐ (ω : fsTrialSpace (M + 1)) ∂fsTrialMeasure p₀, ∀ (i : ι), Filter.Tendsto (fun (m : ℕ) => ∑ n : Fin N, (∑ k ∈ Finset.range m, (fsTrial (M + 1) k ⁻¹' bornRegion ψ' hψ'0 (e (n, i))).indicator (fun (x : fsTrialSpace (M + 1)) => 1) ω) / ↑m) Filter.atTop (nhds (P.weight ψ i))

POVM Born-frequency convergence on the canonical i.i.d. FS process (P.4). povm_born_frequency_volume with the trial bundle discharged by the canonical witness on the dilated sector Σ' = ℂℙ^{N·|ι|−1}: the statement quantifies only over (P, D, ψ, e, ψ', hψ'eq, hψ'0, hnorm, hpos, p₀). The conclusion is verbatim the original's with Pr := fsTrialMeasure p₀, X := fsTrial (M + 1). The region family is the dilated-state bornRegion ψ' hψ'0 (measurability via bornRegion_measurable_uncond). Foundational-triple-only, Gleason-free.

(This canonical form lives here, not in POVMVolume.lean, because the import chain runs POVMVolume → BornRegionUncond → TrialWitness; placing it upstream would create a cycle.)