LF4/BlochProjection: the general-axis Born weight on ℂℙ^{N-1} (context-fixed qubit, A7)

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

The general-axis Bloch projection blochProj a p = |⟨a, rep p⟩|² / ‖rep p‖²: for a unit axis a and a projective point p = [φ], this is the Born weight |⟨a|φ⟩|² of the state along a. It generalises momentMap p i = |⟨eᵢ|φ⟩|² (the reference-axis case a = eᵢ) to an arbitrary axis, and is the shared foundation for the context-fixed qubit measurement (Paper C A7, specs/record-layer-plan.md §2): the hemispheres H±(n) are cut by blochProj n, and the spread density from a prep ψ is a function of blochProj ψ.

Key facts, all foundational-triple, no sorry:

• blochProj_mk — scale-invariance (well-defined on the projective point);
• toEuclideanLin_unitary_norm — the unitary matrix action is an isometry (from Projectivization.inner_toEuclideanLin_unitary);
• blochProj_smul — U(N)-equivariance: blochProj a (U • p) = |⟨a, U·rep p⟩|² / ‖rep p‖²;
• blochProj_measurable — Borel measurability (mirrors momentMap_measurable).

References

LF4/MomentMap.lean (momentMap, momentMap_mk, momentRatio_smul — the reference-axis case); LF4/BornFS.lean (momentMap_measurable); Thermo/CanonicalTypicality.lean (smul_eq_mk); specs/record-layer-plan.md §2 (the qubit context-fixed crux).

noncomputable def CSD.LF4.blochProj {N : ℕ} (a : EuclideanSpace ℂ (Fin N)) (p : CPN N) : ℝ

General-axis Bloch projection. blochProj a p = |⟨a, rep p⟩|² / ‖rep p‖² — for a unit axis a, the Born weight |⟨a|φ⟩|² of the state p = [φ] along a. Well-defined on the projective point (scale-invariant; see blochProj_mk). Generalises momentMap p i (the case a = eᵢ).

Equations

• CSD.LF4.blochProj a p = ‖inner ℂ a (Projectivization.rep p)‖ ^ 2 / ‖Projectivization.rep p‖ ^ 2

theorem CSD.LF4.blochRatio_smul {N : ℕ} (a : EuclideanSpace ℂ (Fin N)) (c : ℂ) (hc : c ≠ 0) (v : EuclideanSpace ℂ (Fin N)) : ‖inner ℂ a (c • v)‖ ^ 2 / ‖c • v‖ ^ 2 = ‖inner ℂ a v‖ ^ 2 / ‖v‖ ^ 2

The ratio |⟨a, c•v⟩|²/‖c•v‖² is invariant under nonzero rescaling of v (projective well-definedness of blochProj).

theorem CSD.LF4.blochProj_mk {N : ℕ} (a ψ : EuclideanSpace ℂ (Fin N)) (hψ : ψ ≠ 0) : blochProj a (Projectivization.mk ℂ ψ hψ) = ‖inner ℂ a ψ‖ ^ 2 / ‖ψ‖ ^ 2

Scale-invariance / representative form: blochProj a [ψ] = |⟨a, ψ⟩|² / ‖ψ‖² for any nonzero representative ψ of the projective point.

theorem CSD.LF4.blochProj_mk_unit {N : ℕ} (a ψ : EuclideanSpace ℂ (Fin N)) (hψ0 : ψ ≠ 0) (hψ : ‖ψ‖ = 1) : blochProj a (Projectivization.mk ℂ ψ hψ0) = ‖inner ℂ a ψ‖ ^ 2

For a unit axis and unit representative, blochProj a [ψ] = |⟨a, ψ⟩|².

theorem CSD.LF4.blochProj_nonneg {N : ℕ} (a : EuclideanSpace ℂ (Fin N)) (p : CPN N) : 0 ≤ blochProj a p

Each Bloch projection is nonnegative.

theorem CSD.LF4.toEuclideanLin_unitary_norm {N : ℕ} (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (v : EuclideanSpace ℂ (Fin N)) : ‖(Matrix.toEuclideanLin ↑U) v‖ = ‖v‖

The unitary matrix action is an isometry: ‖U·v‖ = ‖v‖, from Projectivization.inner_toEuclideanLin_unitary at x = y = v.

theorem CSD.LF4.blochProj_smul {N : ℕ} [NeZero N] (a : EuclideanSpace ℂ (Fin N)) (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (p : CPN N) : blochProj a (U • p) = ‖inner ℂ a ((Matrix.toEuclideanLin ↑U) (Projectivization.rep p))‖ ^ 2 / ‖Projectivization.rep p‖ ^ 2

U(N)-equivariance of the Bloch projection. blochProj a (U • p) = |⟨a, U·rep p⟩|² / ‖rep p‖²: pushing the point by U acts as U on the representative, and U is an isometry so the denominator is unchanged.

theorem CSD.LF4.blochProj_measurable {N : ℕ} (a : EuclideanSpace ℂ (Fin N)) : Measurable fun (p : CPN N) => blochProj a p

Borel measurability of the Bloch projection (mirrors momentMap_measurable).