LF4/QubitDipole: the dipole correlation for the context-fixed qubit (A7)

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

The reflection R_n = 2|n⟩⟨n| − I as a genuine unitary matrix (Hermitian involution), and the resulting dipole correlation

D = ∫ sign(2·blochProj n − 1)·(2·blochProj ψ − 1) dμ_FS = (2c − 1)/2, c = |⟨n|ψ⟩|².

Mechanism: R_n is a Hermitian unitary (R_n² = I, outerProduct_mul_self_of_unit_norm), so its ℂℙ¹-action preserves μ_FS (fubiniStudyMeasure_smul_invariant) and fixes the n-coordinate. Reflecting the density and averaging, reflect_sq_add (the ℂ² reflection identity) linearises 2(s + s′) − 2 = 2(2c − 1)(2u − 1), and the general-axis hat-box hatBox_axis (∫|2u − 1| = ½) closes it. Foundational-triple, no sorry.

References

LF4/QubitReflection.lean (reflect_sq_add); LF4/AxisBridge.lean (hatBox_axis); LF2/BornWrapper.lean (outerProduct, outerProduct_mul_self_of_unit_norm); specs/record-layer-plan.md §2 (the qubit context-fixed crux, dipole term).

noncomputable def CSD.LF4.reflMat (n : EuclideanSpace ℂ (Fin 2)) : Matrix (Fin 2) (Fin 2) ℂ

The reflection matrix R_n = 2|n⟩⟨n| − I.

Equations

• CSD.LF4.reflMat n = 2 • CSD.LF2.outerProduct n - 1

theorem CSD.LF4.reflMat_conjTranspose (n : EuclideanSpace ℂ (Fin 2)) : (reflMat n).conjTranspose = reflMat n

R_n is Hermitian: (2P − I)ᴴ = 2P − I since P = |n⟩⟨n| is Hermitian and star 2 = 2.

theorem CSD.LF4.reflMat_mul_self (n : EuclideanSpace ℂ (Fin 2)) (hn : ‖n‖ = 1) : reflMat n * reflMat n = 1

R_n is an involution for a unit axis: R_n · R_n = I. Ring calculation (2P − I)² = 4P² − 4P + I = I using idempotence P² = P.

theorem CSD.LF4.reflMat_mem_unitaryGroup (n : EuclideanSpace ℂ (Fin 2)) (hn : ‖n‖ = 1) : reflMat n ∈ Matrix.unitaryGroup (Fin 2) ℂ

R_n lies in the unitary group (Hermitian involution ⇒ star R_n · R_n = R_n² = I).

noncomputable def CSD.LF4.reflU (n : EuclideanSpace ℂ (Fin 2)) (hn : ‖n‖ = 1) : ↥(Matrix.unitaryGroup (Fin 2) ℂ)

The reflection unitary R_n as an element of the unitary group.

Equations

• CSD.LF4.reflU n hn = ⟨CSD.LF4.reflMat n, ⋯⟩

theorem CSD.LF4.toEuclideanLin_outerProduct (n w : EuclideanSpace ℂ (Fin 2)) : (Matrix.toEuclideanLin (LF2.outerProduct n)) w = inner ℂ n w • n

The outer product |n⟩⟨n| acts as w ↦ ⟨n,w⟩ • n. Proved coordinatewise.

theorem CSD.LF4.reflMat_toEuclideanLin (n w : EuclideanSpace ℂ (Fin 2)) : (Matrix.toEuclideanLin (reflMat n)) w = (2 * inner ℂ n w) • n - w

R_n acts as the reflection map: toEuclideanLin R_n w = (2⟨n,w⟩)•n − w, i.e. R_n = 2|n⟩⟨n| − I. Follows from linearity of toEuclideanLin and toEuclideanLin_outerProduct.

theorem CSD.LF4.blochProj_reflU (a n : EuclideanSpace ℂ (Fin 2)) (hn : ‖n‖ = 1) (p : CPN 2) : blochProj a (reflU n hn • p) = ‖inner ℂ a ((2 * inner ℂ n (Projectivization.rep p)) • n - Projectivization.rep p)‖ ^ 2 / ‖Projectivization.rep p‖ ^ 2

The Bloch projection along axis a after reflecting by R_n: blochProj a (R_n•p) = |⟨a, (2⟨n,rep⟩)•n − rep⟩|² / ‖rep‖².

theorem CSD.LF4.blochProj_refl_fixes (n : EuclideanSpace ℂ (Fin 2)) (hn : ‖n‖ = 1) (p : CPN 2) : blochProj n (reflU n hn • p) = blochProj n p

The reflection fixes the n-coordinate: blochProj n (R_n•p) = blochProj n p. Since R_n n = n, we have ⟨n, R_n φ⟩ = ⟨n, φ⟩.

theorem CSD.LF4.blochProj_le_one (a : EuclideanSpace ℂ (Fin 2)) (ha : ‖a‖ = 1) (p : CPN 2) : blochProj a p ≤ 1

Cauchy–Schwarz bound: blochProj a p ≤ 1 for a unit axis a.

theorem CSD.LF4.reflSum (n ψ : EuclideanSpace ℂ (Fin 2)) (hn : ‖n‖ = 1) (hψ : ‖ψ‖ = 1) (p : CPN 2) : blochProj ψ p + blochProj ψ (reflU n hn • p) = 2 * (‖inner ℂ n ψ‖ ^ 2 * blochProj n p) + 2 * ((1 - ‖inner ℂ n ψ‖ ^ 2) * (1 - blochProj n p))

The reflection sum identity (projective form). For unit n, ψ, the sum of the Born weight of ψ and its R_n-reflection is a linear function of the n-coordinate: blochProj ψ p + blochProj ψ (R_n•p) = 2c·u + 2(1−c)(1−u), c = |⟨n,ψ⟩|², u = blochProj n p. The projective lift of reflect_sq_add, via a unit representative of p.

noncomputable def CSD.LF4.rsign (x : ℝ) : ℝ

Real-valued sign function rsign x ∈ {−1,0,1}.

Equations

• CSD.LF4.rsign x = if 0 < x then 1 else if x < 0 then -1 else 0

theorem CSD.LF4.rsign_mul_self (x : ℝ) : rsign x * x = |x|

rsign x * x = |x|.

theorem CSD.LF4.abs_rsign_le_one (x : ℝ) : |rsign x| ≤ 1

|rsign x| ≤ 1.

theorem CSD.LF4.measurable_rsign : Measurable rsign

rsign is measurable.

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

The dipole correlation for the context-fixed qubit. For unit n, ψ, ∫ rsign(2·blochProj n − 1)·(2·blochProj ψ − 1) dμ_FS = (2c − 1)/2, c = |⟨n,ψ⟩|². The R_n reflection (μ_FS-preserving, fixes the n-coordinate) plus reflect_sq_add linearises the paired density, and the general-axis hat-box (hatBox_axis) closes it.