LF3 Projectors / LF2 interface: sector volume ↔ LF2 Born form

Category: 3-Local (LF3 → LF2 bridge: sector volume equals LF2 trace-form Born weight on rank-1 effects).

Paper §5.14 / §9.7. (Renamed from branch-weight terminology in Phase 11, 2026-05-18, to align with the volume-ratios reading.)

Bridges the abstract H_SA-level sector volume to LF2's concrete matrix-based Born form. The basis isomorphism H_SA ≃ₗᵢ[ℂ] EuclideanSpace ℂ (Fin N) and the matrix representation of mHat P s t under that iso enter as explicit hypotheses of the bridge theorem, matching Mathlib's idiom for cross-API bridge lemmas (supply the bridging iso at the call site rather than hiding it as a field of SystemApparatusSetup).

The trace-inner identity Tr(|φ⟩⟨φ| · M) = ⟨φ, Mφ⟩ is the core algebraic content; it generalises LF2's born_quadratic to arbitrary effects via Matrix.dotProduct_mulVec and dotProduct_comm (paper §5.14, spec §9.7).

@[reducible, inline]

abbrev CSD.LF3.BasisIso (H_SA : Type u_4) [NormedAddCommGroup H_SA] [InnerProductSpace ℂ H_SA] [FiniteDimensional ℂ H_SA] (N : ℕ) : Type u_4

Basis isomorphism from the abstract H_SA to a concrete finite-dim Euclidean space, used to translate operators on H_SA into matrices for the LF2 Born-form interface.

Equations

• CSD.LF3.BasisIso H_SA N = (H_SA ≃ₗᵢ[ℂ] EuclideanSpace ℂ (Fin N))

noncomputable def CSD.LF3.rankOneStateOfΨ {N : ℕ} (Ψ : EuclideanSpace ℂ (Fin N)) (hΨ : ‖Ψ‖ = 1) : LF2.DensityOperator N

Interpret a unit vector Ψ : EuclideanSpace ℂ (Fin N) as an LF2 DensityOperator N via its rank-1 outer product |Ψ⟩⟨Ψ|.

Equations

• CSD.LF3.rankOneStateOfΨ Ψ hΨ = CSD.LF2.rankOneDensity Ψ hΨ

noncomputable def CSD.LF3.effectOfM {N : ℕ} (M : Matrix (Fin N) (Fin N) ℂ) (h1 : M.IsHermitian) (h2 : M.PosSemidef) (h3 : (1 - M).PosSemidef) : LF2.Effect N

Interpret an N × N matrix M satisfying the effect axioms as an LF2 Effect N.

Equations

• CSD.LF3.effectOfM M h1 h2 h3 = { M := M, isHermitian := h1, nonneg := h2, le_one := h3 }

Trace-inner core identity (paper §5.14)

theorem CSD.LF3.trace_outerProduct_mul_eq_inner {N : ℕ} (φ : EuclideanSpace ℂ (Fin N)) (M : Matrix (Fin N) (Fin N) ℂ) : (LF2.outerProduct φ * M).trace = inner ℂ φ ((Matrix.toEuclideanLin M) φ)

Tr(|φ⟩⟨φ| · M) = ⟨φ, Mφ⟩. The generalised Born trace identity for an arbitrary effect matrix M and a vector φ. Composes vecMulVec_mul, trace_vecMulVec, the EuclideanSpace inner-product formula, and dotProduct_mulVec plus dotProduct_comm.

Bridge theorem (paper §5.14 / spec §9.7)

theorem CSD.LF3.sectorVolume_eq_LF2_Born {K_A : Type u_1} {K_B : Type u_2} {H_SA : Type u_3} [NormedAddCommGroup K_A] [InnerProductSpace ℂ K_A] [FiniteDimensional ℂ K_A] [NormedAddCommGroup K_B] [InnerProductSpace ℂ K_B] [FiniteDimensional ℂ K_B] [NormedAddCommGroup H_SA] [InnerProductSpace ℂ H_SA] [FiniteDimensional ℂ H_SA] {S : SystemApparatusSetup K_A K_B H_SA} {N : ℕ} (P : ProjectorAlgebra S) (s t : Sign) (basisIso : BasisIso H_SA N) (Ψ : H_SA) (hΨ : ‖Ψ‖ = 1) (M : Matrix (Fin N) (Fin N) ℂ) (hM_eq : ∀ (x : H_SA), basisIso ((mHat P s t) x) = (Matrix.toEuclideanLin M) (basisIso x)) (hM1 : M.IsHermitian) (hM2 : M.PosSemidef) (hM3 : (1 - M).PosSemidef) : sectorVolume P Ψ s t = LF2.traceForm (rankOneStateOfΨ (basisIso Ψ) ⋯) (effectOfM M hM1 hM2 hM3)

LF3 ↔ LF2 bridge. Given a basis isomorphism basisIso and a matrix M representing mHat P s t under that iso (i.e. M is the matrix of the pointer-sector projector in the chosen basis, plus standard effect properties), the operator-form sector volume equals the LF2 Born-form trace pairing of the rank-1 density |basisIso Ψ⟩⟨basisIso Ψ| with the effect M.