Documentation

CsdLean4.LF4.QubitCrossTerm

LF4/QubitCrossTerm: the cross-term vanishes (context-fixed qubit, A7) #

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

The cross-term T = ∫ rsign(2·blochProj n − 1)·|2·blochProj ψ − 1| dμ_FS = 0 — the vanishing of the monopole–hemisphere correlation. The antipode symmetry: pushing the Haar integral by right-multiplication U ↦ U·W (where W sends [e₀] to the orthogonal [e₁]) flips both coordinates u ↦ 1−u, s ↦ 1−s via the orthonormal-complement Parseval flip (inner_unitary_flip), so the integrand negates and T = −T.

Foundational-triple, no sorry.

References #

LF4/QubitDipole.lean (rsign, blochProj_le_one); Empirical/CSD/UncertaintyVolume.lean (context_vol_sum_two); Mathlib/.../FubiniStudyUnique.lean (Haar right-invariance, fubiniStudyMeasure_unique); specs/record-layer-plan.md §2 (the qubit context-fixed crux).

source
noncomputable def CSD.LF4.unitaryONB (U : ↥(Matrix.unitaryGroup (Fin 2) ℂ)) :
OrthonormalBasis (Fin 2) ℂ (EuclideanSpace ℂ (Fin 2))

The image of the standard basis of ℂ² under a unitary, packaged as an OrthonormalBasis (orthonormal since U is an isometry; spans since cardinality = dimension).

Equations
Instances For
    source
    @[simp]
    theorem CSD.LF4.unitaryONB_apply (U : ↥(Matrix.unitaryGroup (Fin 2) ℂ)) (i : Fin 2) :
    (unitaryONB U) i = (Matrix.toEuclideanLin ↑U) (EuclideanSpace.single i 1)
    source
    theorem CSD.LF4.inner_unitary_flip (a : EuclideanSpace ℂ (Fin 2)) (ha : ‖a‖ = 1) (U : ↥(Matrix.unitaryGroup (Fin 2) ℂ)) :
    ‖inner ℂ a ((Matrix.toEuclideanLin ↑U) (EuclideanSpace.single 0 1))‖ ^ 2 + ‖inner ℂ a ((Matrix.toEuclideanLin ↑U) (EuclideanSpace.single 1 1))‖ ^ 2 = 1

    Orthonormal-complement flip. For a unit axis a and a unitary U, the Born weights along the two image-basis directions sum to one: |⟨a, U e₀⟩|² + |⟨a, U e₁⟩|² = 1. Parseval over the orthonormal basis unitaryONB U.

    source
    theorem CSD.LF4.rsign_neg (x : ℝ) :
    rsign (-x) = -rsign x

    rsign is odd: rsign (−x) = − rsign x.

    source
    theorem CSD.LF4.fubiniStudy_eq (p₀ p₁ : CPN 2) :
    Matrix.UnitaryGroup.fubiniStudyMeasure p₀ = Matrix.UnitaryGroup.fubiniStudyMeasure p₁

    The Fubini–Study measure is independent of the base point (uniqueness of the invariant law).

    source
    noncomputable def CSD.LF4.swapMat :
    Matrix (Fin 2) (Fin 2) ℂ

    The e₀ ↔ e₁ swap matrix (Pauli-X).

    Equations
    Instances For
      source
      theorem CSD.LF4.swapMat_mem :
      swapMat ∈ Matrix.unitaryGroup (Fin 2) ℂ
      source
      noncomputable def CSD.LF4.swapU :
      ↥(Matrix.unitaryGroup (Fin 2) ℂ)

      The swap unitary as a group element.

      Equations
      Instances For
        source
        theorem CSD.LF4.single_zero_ne :
        EuclideanSpace.single 0 1 ≠ 0
        source
        theorem CSD.LF4.single_one_ne :
        EuclideanSpace.single 1 1 ≠ 0
        source
        theorem CSD.LF4.toEuclideanLin_swapMat_e0 :
        (Matrix.toEuclideanLin swapMat) (EuclideanSpace.single 0 1) = EuclideanSpace.single 1 1

        The swap sends e₀ to e₁.

        source
        theorem CSD.LF4.swapU_smul_e0 :
        swapU • Projectivization.mk ℂ (EuclideanSpace.single 0 1) single_zero_ne = Projectivization.mk ℂ (EuclideanSpace.single 1 1) single_one_ne

        swapU • [e₀] = [e₁].

        source
        theorem CSD.LF4.blochProj_smul_single (a : EuclideanSpace ℂ (Fin 2)) (U : ↥(Matrix.unitaryGroup (Fin 2) ℂ)) (i : Fin 2) (hi : EuclideanSpace.single i 1 ≠ 0) :
        blochProj a (U • Projectivization.mk ℂ (EuclideanSpace.single i 1) hi) = ‖inner ℂ a ((Matrix.toEuclideanLin ↑U) (EuclideanSpace.single i 1))‖ ^ 2

        The Bloch projection at U • [eᵢ] is |⟨a, U eᵢ⟩|².

        source
        theorem CSD.LF4.haar_integral_mul_right (h : ↥(Matrix.unitaryGroup (Fin 2) ℂ) → ℝ) (hh : Measurable h) (W : ↥(Matrix.unitaryGroup (Fin 2) ℂ)) :
        ∫ (U : ↥(Matrix.unitaryGroup (Fin 2) ℂ)), h U ∂Matrix.UnitaryGroup.unitaryHaarProb = ∫ (U : ↥(Matrix.unitaryGroup (Fin 2) ℂ)), h (U * W) ∂Matrix.UnitaryGroup.unitaryHaarProb

        Haar right-invariance in integral form.

        source
        theorem CSD.LF4.crossTerm (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₀ = 0

        The cross-term vanishes. T = ∫ rsign(2·blochProj n − 1)·|2·blochProj ψ − 1| dμ_FS = 0, for unit n, ψ. The antipode symmetry: Haar right-multiplication by the swap flips both Born coordinates (inner_unitary_flip), negating the integrand, so T = −T.