Empirical/CSD: every volume-frequency headline on a canonical i.i.d. trial 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 _ => fsMeasure 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 the canonical process substituted for (Pr, X); 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:

• CSD.RecordLayer.globalBasin (momentContext _) … for the parents that have been migrated to the fibred arena (Bell, GHZ, Hardy, Trine, USD, SIC, SIC3, MUB3, QutritPOVM, and the degenerate-block and Z⊗Z entries), with measurability CSD.RecordLayer.measurableSet_globalBasin and the trial process MeasureTheory.iidTrial / iidMeasure over the epistemic law (Mathlib/MeasureTheory/IidTrials.lean);
• bornRegion ψ' … (rotated / dilated state) for context_born_frequency_volume_canonical, which is deliberately kept as the base-side twin of context_born_frequency_basin_canonical — see below;
• 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.

⚠️ Two base-side statements are kept on purpose (CR-4, 2026-09-06): ContextVolume.context_born_frequency_volume / block_born_frequency_volume and the context_born_frequency_volume_canonical entry here. They are the base-arena engines that the fibred twins are documented against, and the bridge CSD.RecordLayer.globalBasin_toReal_eq_bornRegion_toReal is stated between the two routes; removing them would leave the fibred statements with nothing to be compared to. Everything downstream of them — every witness, capstone and empirical entry — is on the fibred arena.

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 (θ : ℝ) : ∀ᵐ (ω : MeasureTheory.iidSpace (LF4.KSigma 4)) ∂MeasureTheory.iidMeasure (RecordLayer.epistemicMeasure (Projectivization.mk ℂ (bellSingletVec θ) ⋯)), ∀ (i : Fin 4), Filter.Tendsto (fun (m : ℕ) => (∑ k ∈ Finset.range m, (MeasureTheory.iidTrial (LF4.KSigma 4) k ⁻¹' RecordLayer.globalBasin (RecordLayer.momentContext 4) i).indicator (fun (x : MeasureTheory.iidSpace (LF4.KSigma 4)) => 1) ω) / ↑m) Filter.atTop (nhds (‖inner ℂ (EuclideanSpace.single i 1) (bellSingletVec θ)‖ ^ 2))

bell_singlet_born_frequency_volume on the canonical i.i.d. process over the fibred epistemic law.

GHZ (CPN 8)

theorem CSD.Empirical.CSDBridge.GHZVolume.ghz_born_frequency_volume_canonical (Φ : ℝ) : ∀ᵐ (ω : MeasureTheory.iidSpace (LF4.KSigma 8)) ∂MeasureTheory.iidMeasure (RecordLayer.epistemicMeasure (Projectivization.mk ℂ (ghzVec Φ) ⋯)), ∀ (i : Fin 8), Filter.Tendsto (fun (m : ℕ) => (∑ k ∈ Finset.range m, (MeasureTheory.iidTrial (LF4.KSigma 8) k ⁻¹' RecordLayer.globalBasin (RecordLayer.momentContext 8) i).indicator (fun (x : MeasureTheory.iidSpace (LF4.KSigma 8)) => 1) ω) / ↑m) Filter.atTop (nhds (‖inner ℂ (EuclideanSpace.single i 1) (ghzVec Φ)‖ ^ 2))

ghz_born_frequency_volume on the canonical i.i.d. process over the fibred epistemic law.

Hardy (CPN 4)

theorem CSD.Empirical.CSDBridge.HardyVolume.hardy_max_born_frequency_volume_canonical : ∀ᵐ (ω : MeasureTheory.iidSpace (LF4.KSigma 4)) ∂MeasureTheory.iidMeasure (RecordLayer.epistemicMeasure (Projectivization.mk ℂ hardyVolVec hardyVolVec_ne_zero)), ∀ (i : Fin 4), Filter.Tendsto (fun (m : ℕ) => (∑ k ∈ Finset.range m, (MeasureTheory.iidTrial (LF4.KSigma 4) k ⁻¹' RecordLayer.globalBasin (RecordLayer.momentContext 4) i).indicator (fun (x : MeasureTheory.iidSpace (LF4.KSigma 4)) => 1) ω) / ↑m) Filter.atTop (nhds (‖inner ℂ (EuclideanSpace.single i 1) hardyVolVec‖ ^ 2))

hardy_max_born_frequency_volume on the canonical i.i.d. process over the fibred epistemic law.

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 | Projectivization.momentMap p 0 ≤ (Projectivization.mk ℂ (malusVec θ) ⋯).momentMap 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 | Projectivization.momentMap p 0 ≤ (Projectivization.mk ℂ LF4.zPlusVec LF4.zPlusVec_ne_zero).momentMap 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 | Projectivization.momentMap p 0 ≤ (Projectivization.mk ℂ balVec balVec_ne_zero).momentMap 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) : ∀ᵐ (ω : MeasureTheory.iidSpace (LF4.KSigma 6)) ∂MeasureTheory.iidMeasure (RecordLayer.epistemicMeasure (Projectivization.mk ℂ ψ' hψ'0)), ∀ (k : Fin 3), Filter.Tendsto (fun (m : ℕ) => ∑ n : Fin 2, (∑ l ∈ Finset.range m, (MeasureTheory.iidTrial (LF4.KSigma 6) l ⁻¹' RecordLayer.globalBasin (RecordLayer.momentContext 6) (e (n, k))).indicator (fun (x : MeasureTheory.iidSpace (LF4.KSigma 6)) => 1) ω) / ↑m) Filter.atTop (nhds (trinePOVM.weight ψ k))

trine_born_frequency_volume on the canonical i.i.d. process over the fibred epistemic law.

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) : ∀ᵐ (ω : MeasureTheory.iidSpace (LF4.KSigma 6)) ∂MeasureTheory.iidMeasure (RecordLayer.epistemicMeasure (Projectivization.mk ℂ ψ' hψ'0)), ∀ (k : Fin 3), Filter.Tendsto (fun (m : ℕ) => ∑ n : Fin 2, (∑ l ∈ Finset.range m, (MeasureTheory.iidTrial (LF4.KSigma 6) l ⁻¹' RecordLayer.globalBasin (RecordLayer.momentContext 6) (e (n, k))).indicator (fun (x : MeasureTheory.iidSpace (LF4.KSigma 6)) => 1) ω) / ↑m) Filter.atTop (nhds ((QM.USD.usdPOVM s hs0 hs1).weight ψ k))

usd_born_frequency_volume on the canonical i.i.d. process over the fibred epistemic law.

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) : ∀ᵐ (ω : MeasureTheory.iidSpace (LF4.KSigma 8)) ∂MeasureTheory.iidMeasure (RecordLayer.epistemicMeasure (Projectivization.mk ℂ ψ' hψ'0)), ∀ (k : Fin 4), Filter.Tendsto (fun (m : ℕ) => ∑ n : Fin 2, (∑ l ∈ Finset.range m, (MeasureTheory.iidTrial (LF4.KSigma 8) l ⁻¹' RecordLayer.globalBasin (RecordLayer.momentContext 8) (e (n, k))).indicator (fun (x : MeasureTheory.iidSpace (LF4.KSigma 8)) => 1) ω) / ↑m) Filter.atTop (nhds (sicPOVM.weight ψ k))

sic_born_frequency_volume on the canonical i.i.d. process over the fibred epistemic law.

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) : ∀ᵐ (ω : MeasureTheory.iidSpace (LF4.KSigma 27)) ∂MeasureTheory.iidMeasure (RecordLayer.epistemicMeasure (Projectivization.mk ℂ ψ' hψ'0)), ∀ (i : Fin 3 × Fin 3), Filter.Tendsto (fun (m : ℕ) => ∑ n : Fin 3, (∑ l ∈ Finset.range m, (MeasureTheory.iidTrial (LF4.KSigma 27) l ⁻¹' RecordLayer.globalBasin (RecordLayer.momentContext 27) (e (n, i))).indicator (fun (x : MeasureTheory.iidSpace (LF4.KSigma 27)) => 1) ω) / ↑m) Filter.atTop (nhds (sic3POVM.weight ψ i))

sic3_born_frequency_volume on the canonical i.i.d. process over the fibred epistemic law.

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) : ∀ᵐ (ω : MeasureTheory.iidSpace (LF4.KSigma 36)) ∂MeasureTheory.iidMeasure (RecordLayer.epistemicMeasure (Projectivization.mk ℂ ψ' hψ'0)), ∀ (i : Fin 4 × Fin 3), Filter.Tendsto (fun (m : ℕ) => ∑ n : Fin 3, (∑ l ∈ Finset.range m, (MeasureTheory.iidTrial (LF4.KSigma 36) l ⁻¹' RecordLayer.globalBasin (RecordLayer.momentContext 36) (e (n, i))).indicator (fun (x : MeasureTheory.iidSpace (LF4.KSigma 36)) => 1) ω) / ↑m) Filter.atTop (nhds (mub3POVM.weight ψ i))

mub3_born_frequency_volume on the canonical i.i.d. process over the fibred epistemic law.

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) : ∀ᵐ (ω : MeasureTheory.iidSpace (LF4.KSigma 9)) ∂MeasureTheory.iidMeasure (RecordLayer.epistemicMeasure (Projectivization.mk ℂ ψ' hψ'0)), ∀ (k : Fin 3), Filter.Tendsto (fun (m : ℕ) => ∑ n : Fin 3, (∑ l ∈ Finset.range m, (MeasureTheory.iidTrial (LF4.KSigma 9) l ⁻¹' RecordLayer.globalBasin (RecordLayer.momentContext 9) (e (n, k))).indicator (fun (x : MeasureTheory.iidSpace (LF4.KSigma 9)) => 1) ω) / ↑m) Filter.atTop (nhds ((noisyPOVM ε hε0 hε1).weight ψ k))

noisy_born_frequency_volume on the canonical i.i.d. process over the fibred epistemic law.

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.context_born_frequency_basin_canonical {M : ℕ} (B : OrthonormalBasis (Fin (M + 1)) ℂ (EuclideanSpace ℂ (Fin (M + 1)))) (ψ : EuclideanSpace ℂ (Fin (M + 1))) (hψ : ‖ψ‖ = 1) : ∀ᵐ (ω : MeasureTheory.iidSpace (LF4.KSigma (M + 1))) ∂MeasureTheory.iidMeasure (RecordLayer.epistemicMeasure (Projectivization.mk ℂ (B.repr ψ) ⋯)), ∀ (i : Fin (M + 1)), Filter.Tendsto (fun (m : ℕ) => (∑ k ∈ Finset.range m, (MeasureTheory.iidTrial (LF4.KSigma (M + 1)) k ⁻¹' RecordLayer.globalBasin (RecordLayer.momentContext (M + 1)) i).indicator (fun (x : MeasureTheory.iidSpace (LF4.KSigma (M + 1))) => 1) ω) / ↑m) Filter.atTop (nhds (‖inner ℂ (B i) ψ‖ ^ 2))

★ context_born_frequency_basin on the canonical i.i.d. process for the epistemic measure — the fibred twin of context_born_frequency_volume_canonical (CR-4).

theorem CSD.Empirical.CSDBridge.ContextVolume.block_born_frequency_volume_event_canonical {M : ℕ} {ι : Type u_1} [DecidableEq ι] (B : OrthonormalBasis (Fin (M + 1)) ℂ (EuclideanSpace ℂ (Fin (M + 1)))) (ψ : EuclideanSpace ℂ (Fin (M + 1))) (hψ : ‖ψ‖ = 1) (blk : Fin (M + 1) → ι) (a : ι) : ∀ᵐ (ω : MeasureTheory.iidSpace (LF4.KSigma (M + 1))) ∂MeasureTheory.iidMeasure (RecordLayer.epistemicMeasure (Projectivization.mk ℂ (B.repr ψ) ⋯)), Filter.Tendsto (fun (m : ℕ) => (∑ k ∈ Finset.range m, (MeasureTheory.iidTrial (LF4.KSigma (M + 1)) k ⁻¹' ⋃ i ∈ {i : Fin (M + 1) | blk i = a}, RecordLayer.globalBasin (RecordLayer.momentContext (M + 1)) i).indicator (fun (x : MeasureTheory.iidSpace (LF4.KSigma (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. process over the fibred epistemic law. The inhabited block form (the union-event restatement of block_born_frequency_basin, which is superseded for the canonical purpose; its sum-form canonical is omitted).

theorem CSD.Empirical.CSDBridge.ContextVolume.zz_parity_born_frequency_volume_canonical (ψ : EuclideanSpace ℂ (Fin 4)) (hψ : ‖ψ‖ = 1) : ∀ᵐ (ω : MeasureTheory.iidSpace (LF4.KSigma 4)) ∂MeasureTheory.iidMeasure (RecordLayer.epistemicMeasure (Projectivization.mk ℂ ((EuclideanSpace.basisFun (Fin 4) ℂ).repr ψ) ⋯)), Filter.Tendsto (fun (m : ℕ) => ∑ i : Fin (Nat.succ 3) with ![0, 1, 1, 0] i = 0, (∑ k ∈ Finset.range m, (MeasureTheory.iidTrial (LF4.KSigma 4) k ⁻¹' RecordLayer.globalBasin (RecordLayer.momentContext 4) i).indicator (fun (x : MeasureTheory.iidSpace (LF4.KSigma 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. process over the fibred epistemic law.