LF4 plan B, Part 2, Slice 4: assembly + discharge of fs_moment_pushforward_uniform

Category: 3-Local (assembly + discharge of fs_moment_pushforward_uniform).

Composes the three closed slices into the moment-marginal headline and discharges the Duistermaat–Heckman axiom for the qubit:

fs_moment_pushforward_uniform_thm : (momentMap · 0)∗ fubiniStudyMeasure p₀ = volume.restrict (Icc 0 1).

Chain:

• L5.2c (bridge) regroupPi_map: regroup4∗ (pi gaussianReal) = gaussian2 × gaussian2, via finSumFinEquiv : Fin 2 ⊕ Fin 2 ≃ Fin 4 (measurePreserving_piCongrLeft + measurePreserving_sumPiEquivProdPi
  • measurePreserving_finTwoArrow); the composite equiv equals regroup4 exactly.
• L5 moment_marginal_uniform_pi: Tpi∗ (pi gaussianReal) = volume.restrict (Ioo 0 1), composing the bridge with blockSqNorm_map_gaussian2_prod (L5.2b) and ratioSqNorm_map_expHalf_prod (L5.3).
• L6 rewrites fubiniStudyMeasure = gaussianCP (Part 1), pushes through gaussianProj/coords to stdGaussian(ℝ⁴) = (pi gaussianReal).map (toLp 2), identifies the moment composition with Tpi a.e. (off the null {0}), and applies L5; Ioo 0 1 → Icc 0 1 since the endpoints are volume-null.

This retires CSD.LF4.fs_moment_pushforward_uniform from the axiom list (it becomes a theorem); the unconditional qubit Born results become foundational-triple-only. See specs/plan-b-detail.md Part 2, Slice 4.

Terminology note (two _uncond senses). The _uncond suffix in this file (fs_born_volume_ratio_qubit_uncond, qubit_born_frequency_convergence_uncond) means "the h_uniform DH hypothesis is discharged". It is distinct from the _uncond of LF4/BornRegionUncond.lean, which means "the genericity hypothesis hpos is removed". The qubit moment-sublevel route here never carried an hpos-style hypothesis (only ψ ≠ 0 and ‖ψ‖ = 1), so no hpos migration applies.

def CSD.LF4.regroup4 (y : Fin 4 → ℝ) : (ℝ × ℝ) × ℝ × ℝ

Regroup Fin 4 → ℝ coordinates into two pairs ((y₀,y₁),(y₂,y₃)).

Equations

• CSD.LF4.regroup4 y = ((y 0, y 1), y 2, y 3)

theorem CSD.LF4.regroupPi_map : MeasureTheory.Measure.map regroup4 (MeasureTheory.Measure.pi fun (x : Fin 4) => ProbabilityTheory.gaussianReal 0 1) = gaussian2.prod gaussian2

L5.2c (the bridge). regroup4∗ (pi gaussianReal) = gaussian2 × gaussian2. Via finSumFinEquiv : Fin 2 ⊕ Fin 2 ≃ Fin 4 (which sends inl 0,inl 1,inr 0,inr 1 to 0,1,2,3), so the composite measure-preserving equiv has underlying map regroup4 (hfun).

noncomputable def CSD.LF4.blockLsq : (ℝ × ℝ) × ℝ × ℝ → ℝ × ℝ

The squared-norm-block map.

Equations

• CSD.LF4.blockLsq = Prod.map (fun (p : ℝ × ℝ) => p.1 ^ 2 + p.2 ^ 2) fun (p : ℝ × ℝ) => p.1 ^ 2 + p.2 ^ 2

noncomputable def CSD.LF4.ratioFn : ℝ × ℝ → ℝ

The ratio map.

Equations

• CSD.LF4.ratioFn q = q.1 / (q.1 + q.2)

noncomputable def CSD.LF4.Tpi : (Fin 4 → ℝ) → ℝ

The full moment-marginal map on Fin 4 → ℝ: Tpi y = (y₀²+y₁²)/(y₀²+y₁²+y₂²+y₃²).

Equations

• CSD.LF4.Tpi = CSD.LF4.ratioFn ∘ CSD.LF4.blockLsq ∘ CSD.LF4.regroup4

theorem CSD.LF4.measurable_regroup4 : Measurable regroup4

theorem CSD.LF4.moment_marginal_uniform_pi : MeasureTheory.Measure.map Tpi (MeasureTheory.Measure.pi fun (x : Fin 4) => ProbabilityTheory.gaussianReal 0 1) = MeasureTheory.volume.restrict (Set.Ioo 0 1)

L5. Tpi∗ (pi gaussianReal) = volume.restrict (Ioo 0 1).

theorem CSD.LF4.pi_gaussianReal_singleton_zero : (MeasureTheory.Measure.pi fun (x : Fin 4) => ProbabilityTheory.gaussianReal 0 1) {0} = 0

The pi gaussianReal measure has no atom at the origin.

theorem CSD.LF4.fs_moment_pushforward_uniform (p₀ : CPN 2) : MeasureTheory.Measure.map (fun (p : CPN 2) => momentMap p 0) (Matrix.UnitaryGroup.fubiniStudyMeasure p₀) = MeasureTheory.volume.restrict (Set.Icc 0 1)

L6 / discharge. The moment-map coordinate pushes the genuine Fubini–Study measure on ℂℙ¹ to the uniform measure on [0,1]. This is the qubit Duistermaat–Heckman / Archimedes fact, now a theorem (no longer an axiom), discharged via the Gaussian-induced realisation of μ_FS (Part 1) and the moment-marginal computation (Slices 1–3). Formerly the axiom fs_moment_pushforward_uniform (DuistermaatHeckman.lean).

theorem CSD.LF4.fs_born_volume_ratio_qubit_uncond (p₀ : CPN 2) (ψ : EuclideanSpace ℂ (Fin 2)) (hψ0 : ψ ≠ 0) (hψ : ‖ψ‖ = 1) : (Matrix.UnitaryGroup.fubiniStudyMeasure p₀) {p : CPN 2 | momentMap p 0 ≤ momentMap (Projectivization.mk ℂ ψ hψ0) 0} = ENNReal.ofReal (‖inner ℂ (EuclideanSpace.single 0 1) ψ‖ ^ 2)

Unconditional qubit Born = Fubini–Study volume ratio on ℂℙ¹. The genuine fubiniStudyMeasure of the moment sublevel set at [ψ] equals the Born weight ‖⟨e₀, ψ⟩‖². Foundational-triple-only (the DH/Archimedes input fs_moment_pushforward_uniform is now a theorem); no busch_effect_gleason.

theorem CSD.LF4.qubit_born_frequency_convergence_uncond (p₀ : CPN 2) (ψ : EuclideanSpace ℂ (Fin 2)) (hψ0 : ψ ≠ 0) (hψ : ‖ψ‖ = 1) {Ω : Type u_1} [MeasurableSpace Ω] {Pr : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure Pr] (X : ℕ → Ω → CPN 2) (hX : ∀ (n : ℕ), Measurable (X n)) (hlaw : ∀ (n : ℕ), MeasureTheory.Measure.map (X n) Pr = Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (hindep : Pairwise (Function.onFun (fun (f g : Ω → ℝ) => ProbabilityTheory.IndepFun f g Pr) fun (n : ℕ) => (X n ⁻¹' {p : CPN 2 | momentMap p 0 ≤ momentMap (Projectivization.mk ℂ ψ hψ0) 0}).indicator fun (x : Ω) => 1)) : ∀ᵐ (ω : Ω) ∂Pr, Filter.Tendsto (fun (M : ℕ) => (∑ i ∈ Finset.range M, (X i ⁻¹' {p : CPN 2 | momentMap p 0 ≤ momentMap (Projectivization.mk ℂ ψ hψ0) 0}).indicator (fun (x : Ω) => 1) ω) / ↑M) Filter.atTop (nhds (‖inner ℂ (EuclideanSpace.single 0 1) ψ‖ ^ 2))

Unconditional Busch-free qubit Born frequency convergence. For i.i.d. trials from the Fubini–Study measure on ℂℙ¹, the empirical frequency of the moment sublevel outcome converges almost surely to the Born weight ‖⟨e₀, ψ⟩‖². Foundational-triple-only; no busch_effect_gleason. The CSD thesis realised unconditionally for the qubit: deterministic typicality + Born = Kähler volume ⟹ frequencies → Born.