LF4/AxisBridge: general axis ↦ reference axis for Fubini–Study integrals (context-fixed qubit, A7)

Category: 2-LF4 (Kähler / moment-map layer — sphere-measure infrastructure).

The general-axis bridge: for a unit axis n, any Fubini–Study integral of f ∘ blochProj n equals the same integral with blochProj n replaced by the reference coordinate momentMap · 0 (= blochProj e₀):

∫ f(blochProj n p) dμ_FS = ∫ f(momentMap p 0) dμ_FS.

The mechanism is the existing U(2)-invariance of the Fubini–Study measure (fubiniStudyMeasure_smul_invariant): a unitary U with U • [e₀] = [n] moves the axis, and the measure is unchanged. This is the workhorse that lifts the reference-axis results (hatBox_moment, spreadDensity_normalized) to an arbitrary measurement axis — in particular the general-axis hat-box ∫ |2·blochProj n − 1| dμ_FS = ½ and normalisation ∫ 4·(2·blochProj n − 1)₊ dμ_FS = 1. Foundational-triple, no sorry.

References

LF4/BlochProjection.lean (blochProj, blochProj_smul, blochProj_measurable); LF4/HatBox.lean (hatBox_moment, spreadDensity_normalized — the reference-axis integrals); Mathlib/.../FubiniStudy.lean (fubiniStudyMeasure_smul_invariant); specs/record-layer-plan.md §2.

theorem CSD.LF4.exists_unitary_moment_axis (n : EuclideanSpace ℂ (Fin 2)) (hn0 : n ≠ 0) (hn : ‖n‖ = 1) : ∃ (U : ↥(Matrix.unitaryGroup (Fin 2) ℂ)), ∀ (p : CPN 2), blochProj n (U • p) = momentMap p 0

Axis-alignment. For a unit axis n in ℂ² there is a unitary U sending the reference coordinate to the n-coordinate: blochProj n (U • p) = momentMap p 0 for all p. Obtained from transitivity of the U(2)-action on ℂℙ¹ (U • [e₀] = [n]) plus unitary invariance of the inner product.

theorem CSD.LF4.blochProj_integral_bridge (n : EuclideanSpace ℂ (Fin 2)) (hn0 : n ≠ 0) (hn : ‖n‖ = 1) (p₀ : CPN 2) {f : ℝ → ℝ} (hf : Measurable f) : ∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin 2))), f (blochProj n p) ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀ = ∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin 2))), f (momentMap p 0) ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀

General-axis bridge. For a unit axis n, a Fubini–Study integral of any measurable function of blochProj n equals the same integral with blochProj n replaced by the reference coordinate momentMap · 0. The axis is moved to e₀ by unitary invariance of μ_FS.

theorem CSD.LF4.hatBox_axis (n : EuclideanSpace ℂ (Fin 2)) (hn0 : n ≠ 0) (hn : ‖n‖ = 1) (p₀ : CPN 2) : ∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin 2))), |2 * blochProj n p - 1| ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀ = 1 / 2

General-axis hat-box. The Fubini–Study average of the Bloch height |2·blochProj n − 1| along an arbitrary unit axis n is ½ — Archimedes' hat-box for any axis (via the bridge to the reference-axis hatBox_moment).

theorem CSD.LF4.spreadDensity_normalized_axis (n : EuclideanSpace ℂ (Fin 2)) (hn0 : n ≠ 0) (hn : ‖n‖ = 1) (p₀ : CPN 2) : ∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin 2))), 4 * max (2 * blochProj n p - 1) 0 ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀ = 1

General-axis spread-density normalisation. The CSD spread density 4·(2·blochProj n − 1)₊ along an arbitrary unit axis n integrates to 1 against the Fubini–Study measure.