Documentation

CsdLean4.LF4.QubitReflection

LF4/QubitReflection: the reflection identity on ℂ² (context-fixed qubit, A7) #

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

The reflection identity (piece 1 of the qubit context-fixed proof, specs/record-layer-plan.md §2): for unit vectors n, ψ, φ in ℂ², with the reflection R_n φ = 2⟨n,φ⟩·n − φ (= 2|n⟩⟨n| − I),

‖⟨ψ,φ⟩‖² + ‖⟨ψ, R_n φ⟩‖² = 2·c·u + 2·(1−c)·(1−u), c = ‖⟨n,ψ⟩‖², u = ‖⟨n,φ⟩‖².

In Bloch terms this is s + s′ = 2cu + 2(1−c)(1−u), the C-term crux of §2. The proof uses the {n, n^⊥} orthonormal decomposition of ℂ² (completeness), so that ⟨ψ,φ⟩ = P + Q, ⟨ψ, R_n φ⟩ = P − Q, then the parallelogram law ‖P+Q‖² + ‖P−Q‖² = 2‖P‖² + 2‖Q‖², with ‖P‖² = cu and ‖Q‖² = (1−c)(1−u) (the latter using that the complement of n is 1-dimensional — Parseval, obtained from completeness at φ = ψ). Pure ℂ² linear algebra, no measure theory. Foundational-triple, no sorry.

References #

specs/record-layer-plan.md §2 (the qubit context-fixed crux, C-term); LF4/HatBox.lean (the hat-box + density normalisation, the single-axis ingredients).

source
theorem CSD.LF4.inner_two (x y : EuclideanSpace ℂ (Fin 2)) :
inner ℂ x y = (starRingEnd ((fun (x : Fin 2) => ℂ) 0)) (x.ofLp 0) * y.ofLp 0 + (starRingEnd ((fun (x : Fin 2) => ℂ) 1)) (x.ofLp 1) * y.ofLp 1

The inner product on ℂ² in coordinates: ⟨x,y⟩ = conj(x₀)y₀ + conj(x₁)y₁.

source
noncomputable def CSD.LF4.perp (n : EuclideanSpace ℂ (Fin 2)) :
EuclideanSpace ℂ (Fin 2)

The orthogonal complement unit vector n^⊥ = (−conj n₁, conj n₀) in ℂ².

Equations
Instances For
    source
    @[simp]
    theorem CSD.LF4.perp_zero (n : EuclideanSpace ℂ (Fin 2)) :
    (perp n).ofLp 0 = -(starRingEnd ((fun (x : Fin 2) => ℂ) 1)) (n.ofLp 1)
    source
    @[simp]
    theorem CSD.LF4.perp_one (n : EuclideanSpace ℂ (Fin 2)) :
    (perp n).ofLp 1 = (starRingEnd ((fun (x : Fin 2) => ℂ) 0)) (n.ofLp 0)
    source
    theorem CSD.LF4.normSq_eq_one_of_norm (n : EuclideanSpace ℂ (Fin 2)) (hn : ‖n‖ = 1) :
    (starRingEnd ((fun (x : Fin 2) => ℂ) 0)) (n.ofLp 0) * n.ofLp 0 + (starRingEnd ((fun (x : Fin 2) => ℂ) 1)) (n.ofLp 1) * n.ofLp 1 = 1

    The unit-norm hypothesis as the complex identity conj(n₀)n₀ + conj(n₁)n₁ = 1.

    source
    theorem CSD.LF4.completeness (n ψ φ : EuclideanSpace ℂ (Fin 2)) (hn : ‖n‖ = 1) :
    inner ℂ ψ φ = inner ℂ ψ n * inner ℂ n φ + inner ℂ ψ (perp n) * inner ℂ (perp n) φ

    Completeness of {n, n^⊥} in ℂ²: ⟨ψ,φ⟩ = ⟨ψ,n⟩⟨n,φ⟩ + ⟨ψ,n^⊥⟩⟨n^⊥,φ⟩ for unit n.

    source
    theorem CSD.LF4.norm_inner_comm (x y : EuclideanSpace ℂ (Fin 2)) :
    ‖inner ℂ x y‖ = ‖inner ℂ y x‖

    The inner-product norm is symmetric: ‖⟨x,y⟩‖ = ‖⟨y,x⟩‖.

    source
    theorem CSD.LF4.parseval_vec (n x : EuclideanSpace ℂ (Fin 2)) (hn : ‖n‖ = 1) (hx : ‖x‖ = 1) :
    ‖inner ℂ n x‖ ^ 2 + ‖inner ℂ (perp n) x‖ ^ 2 = 1

    Parseval for {n, n^⊥}: ‖⟨n,x⟩‖² + ‖⟨n^⊥,x⟩‖² = 1 for unit n, x (completeness at x=x).

    source
    theorem CSD.LF4.reflect_sq_add (n ψ φ : EuclideanSpace ℂ (Fin 2)) (hn : ‖n‖ = 1) (hψ : ‖ψ‖ = 1) (hφ : ‖φ‖ = 1) :
    ‖inner ℂ ψ φ‖ ^ 2 + ‖inner ℂ ψ ((2 * inner ℂ n φ) • n - φ)‖ ^ 2 = 2 * (‖inner ℂ n ψ‖ ^ 2 * ‖inner ℂ n φ‖ ^ 2) + 2 * ((1 - ‖inner ℂ n ψ‖ ^ 2) * (1 - ‖inner ℂ n φ‖ ^ 2))

    The reflection identity (piece 1 of the qubit context-fixed proof). For unit n, ψ, φ in ℂ², with the reflection R_n φ = 2⟨n,φ⟩·n − φ, ‖⟨ψ,φ⟩‖² + ‖⟨ψ,R_nφ⟩‖² = 2·c·u + 2·(1−c)·(1−u), c = ‖⟨n,ψ⟩‖², u = ‖⟨n,φ⟩‖². The C-term crux of record-layer-plan.md §2. Proof: completeness gives ⟨ψ,φ⟩ = P+Q, ⟨ψ,R_nφ⟩ = P−Q; parallelogram; ‖P‖²=cu, ‖Q‖²=(1−c)(1−u) (Parseval).