LF4/QubitBorn: the context-fixed qubit Born rule (A7)

Category: 2-LF4 (Kähler / moment-map layer — qubit context-fixed measurement).

The qubit Born rule, derived from the CSD spread density and the context-fixed hemisphere. For unit preparation ψ and unit measurement axis n, the CSD spread density ρ_ψ = 4·(2·blochProj ψ − 1)₊ weighted by the context-fixed hemisphere indicator ½·(1 + rsign(2·blochProj n − 1)) integrates against the Fubini–Study typicality measure to the Born weight |⟨n|ψ⟩|²:

∫ ½(1 + rsign(2·blochProj n − 1))·4(2·blochProj ψ − 1)₊ dμ_FS = |⟨n|ψ⟩|².

The integrand splits into four pieces evaluated in the preceding modules: ∫(2s−1) = 0, ∫|2s−1| = ½ (hat-box), ∫ rsign(2u−1)(2s−1) = (2c−1)/2 (dipole), ∫ rsign(2u−1)|2s−1| = 0 (cross-term), summing to c = |⟨n|ψ⟩|². Foundational-triple, no sorry.

References

LF4/AxisBridge.lean (hatBox_axis, blochProj_integral_bridge); LF4/QubitDipole.lean (dipole, rsign); LF4/QubitCrossTerm.lean (crossTerm); LF4/HatBox.lean (fs_moment_pushforward_uniform); specs/record-layer-plan.md §2 (the qubit context-fixed crux — the payoff).

theorem CSD.LF4.integral_id_Icc : ∫ (t : ℝ) in Set.Icc 0 1, t = 1 / 2

∫_{[0,1]} t dt = ½.

theorem CSD.LF4.momentMap_integral_half (p₀ : CPN 2) : ∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin 2))), momentMap p 0 ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀ = 1 / 2

The Fubini–Study average of the reference moment coordinate is ½.

theorem CSD.LF4.blochProj_integral_half (a : EuclideanSpace ℂ (Fin 2)) (ha0 : a ≠ 0) (ha : ‖a‖ = 1) (p₀ : CPN 2) : ∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin 2))), blochProj a p ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀ = 1 / 2

The Fubini–Study average of any Bloch projection is ½ (general-axis, via the bridge).

theorem CSD.LF4.four_max_eq (x : ℝ) : 4 * max x 0 = 2 * x + 2 * |x|

4·max(x,0) = 2x + 2|x| (the ρ = 2(m·λ) + 2|m·λ| decomposition).

theorem CSD.LF4.qubitBorn (n ψ : EuclideanSpace ℂ (Fin 2)) (_hn0 : n ≠ 0) (hn : ‖n‖ = 1) (hψ0 : ψ ≠ 0) (hψ : ‖ψ‖ = 1) (p₀ : CPN 2) : ∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin 2))), 1 / 2 * (1 + rsign (2 * blochProj n p - 1)) * (4 * max (2 * blochProj ψ p - 1) 0) ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀ = ‖inner ℂ n ψ‖ ^ 2

The context-fixed qubit Born rule. The CSD spread density 4(2·blochProj ψ − 1)₊ weighted by the context-fixed hemisphere indicator ½(1 + rsign(2·blochProj n − 1)) integrates against the Fubini–Study typicality measure to the Born weight |⟨n|ψ⟩|².