Empirical/CSD: every volume-frequency headline on the canonical i.i.d. FS witness

Category: 3-Local (CSD-ontic volume series, trial-witness coverage tranche).

Each headline of the Empirical/CSD/*Volume series quantifies over an abstract i.i.d. trial bundle (Ω, Pr, X, hX, hlaw, hindep). The canonical FS coordinate process of CsdLean4/LF4/TrialWitness.lean (fsTrialMeasure p₀ = Measure.infinitePi (fun _ => fubiniStudyMeasure p₀), fsTrial N n = (· n)) inhabits that bundle for any measurable region family (fsTrial_pairwise_indepFun_indicator). This file wires the witness into every remaining volume headline, so each acquires a _canonical corollary whose hypothesis set is Lean-inhabited, not merely classically satisfiable.

Each _canonical conclusion is the parent's conclusion verbatim with Pr := fsTrialMeasure p₀ and X := fsTrial _ substituted; the body is a bare term-mode application of the parent (no restatement), mirroring LF4.born_frequency_convergence_N_canonical. The region family supplied to the witness is exactly the parent's hindep region family:

• bornRegion ψ' … (rotated / dilated state) for the barycentric-cell parents (Bell, GHZ, Hardy, Trine, USD, SIC, SIC3, MUB3, QutritPOVM, the Context family), with measurability bornRegion_measurable_uncond;
• the moment-map sublevel set {p | momentMap p 0 ≤ momentMap [ψ] 0} for the qubit chain (Malus, Stern-Gerlach), with measurability (momentMap_measurable 0) measurableSet_Iic.

The POVM headline LF4.povm_born_frequency_volume_canonical lives in TrialWitness.lean itself (import-direction constraint: POVMVolume → BornRegionUncond → TrialWitness).

Honest scope

This is coverage / completeness, not new mathematics or a thesis advance: the witness and the discharge mechanism already existed (the i.i.d. trial-witness tranche); this file leaves no volume-frequency headline merely classically-satisfiable. The honest-scope caveat is unchanged: this is the measure-theoretic existence of the i.i.d. sampling law; the physical reading of repeated preparation as FS-typical i.i.d. draws remains the LF1 typicality / the CSD sector posit (SO-1), not derived by constructing the process. Foundational-triple-only; Gleason-free (no busch_effect_gleason).

Bell singlet (CPN 4)

theorem CSD.Empirical.CSDBridge.BellVolume.bell_singlet_born_frequency_volume_canonical (θ : ℝ) (p₀ : LF4.CPN 4) : ∀ᵐ (ω : LF4.fsTrialSpace 4) ∂LF4.fsTrialMeasure p₀, ∀ (i : Fin 4), Filter.Tendsto (fun (m : ℕ) => (∑ k ∈ Finset.range m, (LF4.fsTrial 4 k ⁻¹' LF4.bornRegion (bellSingletVec θ) ⋯ i).indicator (fun (x : LF4.fsTrialSpace 4) => 1) ω) / ↑m) Filter.atTop (nhds (‖inner ℂ (EuclideanSpace.single i 1) (bellSingletVec θ)‖ ^ 2))

bell_singlet_born_frequency_volume on the canonical i.i.d. FS process.

GHZ (CPN 8)

theorem CSD.Empirical.CSDBridge.GHZVolume.ghz_born_frequency_volume_canonical (Φ : ℝ) (p₀ : LF4.CPN 8) : ∀ᵐ (ω : LF4.fsTrialSpace 8) ∂LF4.fsTrialMeasure p₀, ∀ (i : Fin 8), Filter.Tendsto (fun (m : ℕ) => (∑ k ∈ Finset.range m, (LF4.fsTrial 8 k ⁻¹' LF4.bornRegion (ghzVec Φ) ⋯ i).indicator (fun (x : LF4.fsTrialSpace 8) => 1) ω) / ↑m) Filter.atTop (nhds (‖inner ℂ (EuclideanSpace.single i 1) (ghzVec Φ)‖ ^ 2))

ghz_born_frequency_volume on the canonical i.i.d. FS process.

Hardy (CPN 4)

theorem CSD.Empirical.CSDBridge.HardyVolume.hardy_max_born_frequency_volume_canonical (p₀ : LF4.CPN 4) : ∀ᵐ (ω : LF4.fsTrialSpace 4) ∂LF4.fsTrialMeasure p₀, ∀ (i : Fin 4), Filter.Tendsto (fun (m : ℕ) => (∑ k ∈ Finset.range m, (LF4.fsTrial 4 k ⁻¹' LF4.bornRegion hardyVolVec hardyVolVec_ne_zero i).indicator (fun (x : LF4.fsTrialSpace 4) => 1) ω) / ↑m) Filter.atTop (nhds (‖inner ℂ (EuclideanSpace.single i 1) hardyVolVec‖ ^ 2))

hardy_max_born_frequency_volume on the canonical i.i.d. FS process.

Malus / Stern-Gerlach (CPN 2, moment-map sublevel region)

theorem CSD.Empirical.CSDBridge.MalusVolume.csd_malus_law_canonical (θ : ℝ) (p₀ : LF4.CPN 2) : ∀ᵐ (ω : LF4.fsTrialSpace 2) ∂LF4.fsTrialMeasure p₀, Filter.Tendsto (fun (M : ℕ) => (∑ i ∈ Finset.range M, (LF4.fsTrial 2 i ⁻¹' {p : LF4.CPN 2 | LF4.momentMap p 0 ≤ LF4.momentMap (Projectivization.mk ℂ (malusVec θ) ⋯) 0}).indicator (fun (x : LF4.fsTrialSpace 2) => 1) ω) / ↑M) Filter.atTop (nhds (Real.cos (θ / 2) ^ 2))

csd_malus_law on the canonical i.i.d. FS process. The region family is the moment-map sublevel set; measurability via (momentMap_measurable 0) measurableSet_Iic, supplied through a Unit-indexed family.

theorem CSD.Empirical.CSDBridge.SternGerlachVolume.csd_sg_volume_certain_canonical (p₀ : LF4.CPN 2) : ∀ᵐ (ω : LF4.fsTrialSpace 2) ∂LF4.fsTrialMeasure p₀, Filter.Tendsto (fun (M : ℕ) => (∑ i ∈ Finset.range M, (LF4.fsTrial 2 i ⁻¹' {p : LF4.CPN 2 | LF4.momentMap p 0 ≤ LF4.momentMap (Projectivization.mk ℂ LF4.zPlusVec LF4.zPlusVec_ne_zero) 0}).indicator (fun (x : LF4.fsTrialSpace 2) => 1) ω) / ↑M) Filter.atTop (nhds 1)

csd_sg_volume_certain on the canonical i.i.d. FS process.

theorem CSD.Empirical.CSDBridge.SternGerlachVolume.csd_sg_volume_half_canonical (p₀ : LF4.CPN 2) : ∀ᵐ (ω : LF4.fsTrialSpace 2) ∂LF4.fsTrialMeasure p₀, Filter.Tendsto (fun (M : ℕ) => (∑ i ∈ Finset.range M, (LF4.fsTrial 2 i ⁻¹' {p : LF4.CPN 2 | LF4.momentMap p 0 ≤ LF4.momentMap (Projectivization.mk ℂ balVec balVec_ne_zero) 0}).indicator (fun (x : LF4.fsTrialSpace 2) => 1) ω) / ↑M) Filter.atTop (nhds (1 / 2))

csd_sg_volume_half on the canonical i.i.d. FS process.

POVM-dilation barycentric headlines (Trine, USD, SIC, SIC3, MUB3, QutritPOVM)

theorem CSD.Empirical.CSDBridge.TrineVolume.trine_born_frequency_volume_canonical (ψ : EuclideanSpace ℂ (Fin 2)) (e : Fin 2 × Fin 3 ≃ Fin 6) (ψ' : EuclideanSpace ℂ (Fin 6)) (hψ'eq : ψ' = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin trineNaimark.V) ψ)) (hψ'0 : ψ' ≠ 0) (hnorm : ‖ψ'‖ = 1) (p₀ : LF4.CPN 6) : ∀ᵐ (ω : LF4.fsTrialSpace 6) ∂LF4.fsTrialMeasure p₀, ∀ (k : Fin 3), Filter.Tendsto (fun (m : ℕ) => ∑ n : Fin 2, (∑ l ∈ Finset.range m, (LF4.fsTrial 6 l ⁻¹' LF4.bornRegion ψ' hψ'0 (e (n, k))).indicator (fun (x : LF4.fsTrialSpace 6) => 1) ω) / ↑m) Filter.atTop (nhds (trinePOVM.weight ψ k))

trine_born_frequency_volume on the canonical i.i.d. FS process.

theorem CSD.Empirical.CSDBridge.USDVolume.usd_born_frequency_volume_canonical (s : ℝ) (hs0 : 0 ≤ s) (hs1 : s ≤ 1) (ψ : EuclideanSpace ℂ (Fin 2)) (e : Fin 2 × Fin 3 ≃ Fin 6) (ψ' : EuclideanSpace ℂ (Fin 6)) (hψ'eq : ψ' = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin (usdNaimark s hs0 hs1).V) ψ)) (hψ'0 : ψ' ≠ 0) (hnorm : ‖ψ'‖ = 1) (p₀ : LF4.CPN 6) : ∀ᵐ (ω : LF4.fsTrialSpace 6) ∂LF4.fsTrialMeasure p₀, ∀ (k : Fin 3), Filter.Tendsto (fun (m : ℕ) => ∑ n : Fin 2, (∑ l ∈ Finset.range m, (LF4.fsTrial 6 l ⁻¹' LF4.bornRegion ψ' hψ'0 (e (n, k))).indicator (fun (x : LF4.fsTrialSpace 6) => 1) ω) / ↑m) Filter.atTop (nhds ((QM.USD.usdPOVM s hs0 hs1).weight ψ k))

usd_born_frequency_volume on the canonical i.i.d. FS process.

theorem CSD.Empirical.CSDBridge.SICVolume.sic_born_frequency_volume_canonical (ψ : EuclideanSpace ℂ (Fin 2)) (e : Fin 2 × Fin 4 ≃ Fin 8) (ψ' : EuclideanSpace ℂ (Fin 8)) (hψ'eq : ψ' = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin sicNaimark.V) ψ)) (hψ'0 : ψ' ≠ 0) (hnorm : ‖ψ'‖ = 1) (p₀ : LF4.CPN 8) : ∀ᵐ (ω : LF4.fsTrialSpace 8) ∂LF4.fsTrialMeasure p₀, ∀ (k : Fin 4), Filter.Tendsto (fun (m : ℕ) => ∑ n : Fin 2, (∑ l ∈ Finset.range m, (LF4.fsTrial 8 l ⁻¹' LF4.bornRegion ψ' hψ'0 (e (n, k))).indicator (fun (x : LF4.fsTrialSpace 8) => 1) ω) / ↑m) Filter.atTop (nhds (sicPOVM.weight ψ k))

sic_born_frequency_volume on the canonical i.i.d. FS process.

theorem CSD.Empirical.CSDBridge.SIC3Volume.sic3_born_frequency_volume_canonical (ψ : EuclideanSpace ℂ (Fin 3)) (e : Fin 3 × Fin 3 × Fin 3 ≃ Fin 27) (ψ' : EuclideanSpace ℂ (Fin 27)) (hψ'eq : ψ' = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin sic3Naimark.V) ψ)) (hψ'0 : ψ' ≠ 0) (hnorm : ‖ψ'‖ = 1) (p₀ : LF4.CPN 27) : ∀ᵐ (ω : LF4.fsTrialSpace 27) ∂LF4.fsTrialMeasure p₀, ∀ (i : Fin 3 × Fin 3), Filter.Tendsto (fun (m : ℕ) => ∑ n : Fin 3, (∑ l ∈ Finset.range m, (LF4.fsTrial 27 l ⁻¹' LF4.bornRegion ψ' hψ'0 (e (n, i))).indicator (fun (x : LF4.fsTrialSpace 27) => 1) ω) / ↑m) Filter.atTop (nhds (sic3POVM.weight ψ i))

sic3_born_frequency_volume on the canonical i.i.d. FS process.

theorem CSD.Empirical.CSDBridge.MUB3Volume.mub3_born_frequency_volume_canonical (ψ : EuclideanSpace ℂ (Fin 3)) (e : Fin 3 × Fin 4 × Fin 3 ≃ Fin 36) (ψ' : EuclideanSpace ℂ (Fin 36)) (hψ'eq : ψ' = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin mub3Naimark.V) ψ)) (hψ'0 : ψ' ≠ 0) (hnorm : ‖ψ'‖ = 1) (p₀ : LF4.CPN 36) : ∀ᵐ (ω : LF4.fsTrialSpace 36) ∂LF4.fsTrialMeasure p₀, ∀ (i : Fin 4 × Fin 3), Filter.Tendsto (fun (m : ℕ) => ∑ n : Fin 3, (∑ l ∈ Finset.range m, (LF4.fsTrial 36 l ⁻¹' LF4.bornRegion ψ' hψ'0 (e (n, i))).indicator (fun (x : LF4.fsTrialSpace 36) => 1) ω) / ↑m) Filter.atTop (nhds (mub3POVM.weight ψ i))

mub3_born_frequency_volume on the canonical i.i.d. FS process.

theorem CSD.Empirical.CSDBridge.QutritPOVMVolume.noisy_born_frequency_volume_canonical (ε : ℝ) (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) (ψ : EuclideanSpace ℂ (Fin 3)) (e : Fin 3 × Fin 3 ≃ Fin 9) (ψ' : EuclideanSpace ℂ (Fin 9)) (hψ'eq : ψ' = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin (noisyNaimark ε hε0 hε1).V) ψ)) (hψ'0 : ψ' ≠ 0) (hnorm : ‖ψ'‖ = 1) (p₀ : LF4.CPN 9) : ∀ᵐ (ω : LF4.fsTrialSpace 9) ∂LF4.fsTrialMeasure p₀, ∀ (k : Fin 3), Filter.Tendsto (fun (m : ℕ) => ∑ n : Fin 3, (∑ l ∈ Finset.range m, (LF4.fsTrial 9 l ⁻¹' LF4.bornRegion ψ' hψ'0 (e (n, k))).indicator (fun (x : LF4.fsTrialSpace 9) => 1) ω) / ↑m) Filter.atTop (nhds ((noisyPOVM ε hε0 hε1).weight ψ k))

noisy_born_frequency_volume on the canonical i.i.d. FS process.

Projective measurement contexts (CPN (M+1)): the rotated-basis cells

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

context_born_frequency_volume on the canonical i.i.d. FS process. The region family is the rotated-basis cell bornRegion (B.repr ψ) (repr_ne_zero B ψ hψ).

theorem CSD.Empirical.CSDBridge.ContextVolume.block_born_frequency_volume_event_canonical {M : ℕ} {ι : Type u_1} [DecidableEq ι] (p₀ : LF4.CPN (M + 1)) (B : OrthonormalBasis (Fin (M + 1)) ℂ (EuclideanSpace ℂ (Fin (M + 1)))) (ψ : EuclideanSpace ℂ (Fin (M + 1))) (hψ : ‖ψ‖ = 1) (blk : Fin (M + 1) → ι) (a : ι) : ∀ᵐ (ω : LF4.fsTrialSpace (M + 1)) ∂LF4.fsTrialMeasure p₀, Filter.Tendsto (fun (m : ℕ) => (∑ k ∈ Finset.range m, (LF4.fsTrial (M + 1) k ⁻¹' ⋃ i ∈ {i : Fin (M + 1) | blk i = a}, LF4.bornRegion (B.repr ψ) ⋯ i).indicator (fun (x : LF4.fsTrialSpace (M + 1)) => 1) ω) / ↑m) Filter.atTop (nhds (∑ i : Fin (M + 1) with blk i = a, ‖inner ℂ (B i) ψ‖ ^ 2))

block_born_frequency_volume_event on the canonical i.i.d. FS process. The inhabited block form (the union-event restatement of block_born_frequency_volume, which is superseded for the canonical purpose; its sum-form canonical is omitted).

theorem CSD.Empirical.CSDBridge.ContextVolume.zz_parity_born_frequency_volume_canonical (p₀ : LF4.CPN 4) (ψ : EuclideanSpace ℂ (Fin 4)) (hψ : ‖ψ‖ = 1) : ∀ᵐ (ω : LF4.fsTrialSpace 4) ∂LF4.fsTrialMeasure p₀, Filter.Tendsto (fun (m : ℕ) => ∑ i : Fin (Nat.succ 3) with ![0, 1, 1, 0] i = 0, (∑ k ∈ Finset.range m, (LF4.fsTrial 4 k ⁻¹' LF4.bornRegion ((EuclideanSpace.basisFun (Fin 4) ℂ).repr ψ) ⋯ i).indicator (fun (x : LF4.fsTrialSpace 4) => 1) ω) / ↑m) Filter.atTop (nhds (‖inner ℂ (EuclideanSpace.single 0 1) ψ‖ ^ 2 + ‖inner ℂ (EuclideanSpace.single 3 1) ψ‖ ^ 2))

zz_parity_born_frequency_volume on the canonical i.i.d. FS process.