Empirical/CSD: Malus's law (spin-1/2) as a derived Kähler-volume frequency

Category: 3-Local (CSD-ontic layer; genuine volume derivation, not a transport tag).

The parametric generalisation of Empirical/CSD/SternGerlachVolume.lean: the operational spin-1/2 Malus law P(+ | θ, |+z⟩) = cos²(θ/2) realised as a derived Fubini–Study volume frequency on the ontic Σ = ℂℙ¹, carving-free and Gleason-free.

Construction

For a measurement axis at polar angle θ from the +z preparation axis, the +-eigenstate is ψ_θ = cos(θ/2)|0⟩ + sin(θ/2)|1⟩, so the Born amplitude is ⟨e₀, ψ_θ⟩ = cos(θ/2) and the Born weight ‖⟨e₀, ψ_θ⟩‖² = cos²(θ/2). The volume capstone LF4.qubit_born_frequency_convergence_uncond then gives, for i.i.d. Fubini–Study trials, that the empirical frequency of the moment-sublevel outcome region cut by [ψ_θ] converges almost surely to cos²(θ/2), with volume = Born computed via the Duistermaat–Heckman theorem fs_moment_pushforward_uniform (no carving, no busch_effect_gleason).

Specialisations

csd_malus_law subsumes the two Stern-Gerlach values of SternGerlachVolume.lean:

• θ = 0 ⟹ cos²(0) = 1 (P(+z | +z) = 1);
• θ = π/2 ⟹ cos²(π/4) = 1/2 (the canonical 50/50 split).

What is and is not claimed

Derived (Lean-checked, carving-free, Gleason-free). The limit value cos²(θ/2) is the genuine Fubini–Study volume of the moment-sublevel region, foundational triple only.

Not claimed (the interpretive §14 boundary). Identifying the moment-sublevel region with the physical "the spin-θ + detector fired" outcome is the interpretive §14 labelling — a permanent interpretive boundary (⚠️ RESIDUE(R-007)): the formal operator → Σ-volume dictionary is proved (LF4/ObservableCorrespondenceN.lean), and only the detector-labelling of the region stays outside the theorem layer. This file derives the Born number as a Kähler volume.

Experimental verification

• Malus 1809 (optical, classical analogue); the spin-1/2 cos²(θ/2) form is the canonical sequential Stern-Gerlach prediction (Stern, Gerlach 1922; standard QM textbooks, e.g. Sakurai 1985).

The θ-rotated single-qubit state

noncomputable def CSD.Empirical.CSDBridge.MalusVolume.malusVec (θ : ℝ) : EuclideanSpace ℂ (Fin 2)

The spin-θ +-eigenstate cos(θ/2)|0⟩ + sin(θ/2)|1⟩, with ⟨e₀, malusVec θ⟩ = cos(θ/2).

Equations

• CSD.Empirical.CSDBridge.MalusVolume.malusVec θ = EuclideanSpace.single 0 ↑(Real.cos (θ / 2)) + EuclideanSpace.single 1 ↑(Real.sin (θ / 2))

theorem CSD.Empirical.CSDBridge.MalusVolume.malusVec_ofLp_zero (θ : ℝ) : (malusVec θ).ofLp 0 = ↑(Real.cos (θ / 2))

theorem CSD.Empirical.CSDBridge.MalusVolume.malusVec_ofLp_one (θ : ℝ) : (malusVec θ).ofLp 1 = ↑(Real.sin (θ / 2))

theorem CSD.Empirical.CSDBridge.MalusVolume.malusVec_norm (θ : ℝ) : ‖malusVec θ‖ = 1

theorem CSD.Empirical.CSDBridge.MalusVolume.malusVec_ne_zero (θ : ℝ) : malusVec θ ≠ 0

Malus's law as a derived volume frequency

theorem CSD.Empirical.CSDBridge.MalusVolume.csd_malus_law (θ : ℝ) (p₀ : LF4.CPN 2) {Ω : Type u_1} [MeasurableSpace Ω] {Pr : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure Pr] (X : ℕ → Ω → LF4.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 : LF4.CPN 2 | LF4.momentMap p 0 ≤ LF4.momentMap (Projectivization.mk ℂ (malusVec θ) ⋯) 0}).indicator fun (x : Ω) => 1)) : ∀ᵐ (ω : Ω) ∂Pr, Filter.Tendsto (fun (M : ℕ) => (∑ i ∈ Finset.range M, (X i ⁻¹' {p : LF4.CPN 2 | LF4.momentMap p 0 ≤ LF4.momentMap (Projectivization.mk ℂ (malusVec θ) ⋯) 0}).indicator (fun (x : Ω) => 1) ω) / ↑M) Filter.atTop (nhds (Real.cos (θ / 2) ^ 2))

CSD Malus's law as a derived Kähler-volume frequency. For i.i.d. trials drawing microstates from the Fubini–Study typicality measure on Σ = ℂℙ¹, the empirical frequency of the moment-sublevel outcome region cut by the spin-θ +-eigenstate [malusVec θ] converges almost surely to cos²(θ/2) — the operational spin-1/2 Malus law.

The limit is ‖⟨e₀, malusVec θ⟩‖² = ‖cos(θ/2)‖² = cos²(θ/2), with volume = Born derived from the moment map (no carving), foundational triple only (no busch_effect_gleason). Specialises to 1 at θ = 0 and 1/2 at θ = π/2. The identification of the region with the physical spin-θ outcome is LF4-todo §14.