LF2 Born-Weight Wrapper

Category: 3-Local (LF2 matrix-based Effect/DensityOperator, Born quadratic form, and busch_effect_gleason axiom).

Spec §5. Packages the finite-dimensional probability assignment using concrete matrix-based Effect/DensityOperator structures, an imported busch_effect_gleason axiom, and a proved Born quadratic form for rank-1 outcomes on pure preparations. The rank-1 uniqueness theorem rankOneDensity_unique_of_certainty was carried as an axiom in earlier revisions and was discharged on 2026-05-18 (no spectral theorem needed; PSD inner-product route).

This file is built incrementally; see the companion plan at specs/LF2-plan.md §2.4.

structure CSD.LF2.Effect (N : ℕ) : Type

Effect on an N-dimensional complex Hilbert space. A Hermitian matrix with 0 ≤ E and E ≤ I (both expressed via PosSemidef).

• M : Matrix (Fin N) (Fin N) ℂ

  Underlying matrix.

• isHermitian : self.M.IsHermitian

  E is Hermitian.

• nonneg : self.M.PosSemidef

  0 ≤ E.

• le_one : (1 - self.M).PosSemidef

  E ≤ I, i.e. I - E is PSD.

structure CSD.LF2.DensityOperator (N : ℕ) : Type

Density operator on an N-dimensional complex Hilbert space. A Hermitian PSD matrix with trace 1.

• M : Matrix (Fin N) (Fin N) ℂ

  Underlying matrix.

• isHermitian : self.M.IsHermitian

  ρ is Hermitian.

• nonneg : self.M.PosSemidef

  0 ≤ ρ.

• trace_one : self.M.trace = 1

  Tr(ρ) = 1.

noncomputable def CSD.LF2.traceForm {N : ℕ} (ρ : DensityOperator N) (E : Effect N) : ℝ

Trace-form pairing. Tr(ρ · E) as a real number. The trace of a product of Hermitian matrices is real (self-adjoint), so taking the real part is not an approximation — it is an extraction.

Equations

• CSD.LF2.traceForm ρ E = RCLike.re (ρ.M * E.M).trace

noncomputable def CSD.LF2.Effect.one {N : ℕ} : Effect N

The identity effect I. Represents the trivial always-true measurement outcome.

Equations

• CSD.LF2.Effect.one = { M := 1, isHermitian := ⋯, nonneg := ⋯, le_one := ⋯ }

noncomputable def CSD.LF2.Effect.zero {N : ℕ} : Effect N

The zero effect. Represents the trivial always-false measurement outcome.

Equations

• CSD.LF2.Effect.zero = { M := 0, isHermitian := ⋯, nonneg := ⋯, le_one := ⋯ }

noncomputable def CSD.LF2.Effect.add {N : ℕ} (E F : Effect N) (hLe : (1 - (E.M + F.M)).PosSemidef) : Effect N

Conditional sum of effects. If E, F are effects and E + F ≤ I, their sum is again an effect. Hermitian-ness and PSD of the sum are automatic (Hermitian matrices are closed under addition, PSD matrices form a convex cone); only le_one is a genuine precondition — hence its role as an explicit hypothesis.

Equations

• E.add F hLe = { M := E.M + F.M, isHermitian := ⋯, nonneg := ⋯, le_one := hLe }

noncomputable def CSD.LF2.Effect.conjugateBy {N : ℕ} (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (E : Effect N) : Effect N

Unitary conjugation of an effect. U† E U is again an effect for any unitary U: Hermitian-ness, PSD, and E ≤ I are all preserved by conjugation with a unitary matrix. This is the structural ingredient behind spec Definition 5.1 clause 3 (unitary covariance).

Equations

• CSD.LF2.Effect.conjugateBy U E = { M := (↑U).conjTranspose * E.M * ↑U, isHermitian := ⋯, nonneg := ⋯, le_one := ⋯ }

structure CSD.LF2.OperationalPackage (N : ℕ) : Type

Operational consistency package (spec Definition 5.1). An assignment of probabilities to effects satisfying: non-negativity, boundedness by 1, total-one on the identity, and finite additivity when the sum remains below I.

On the omission of clause 3 (unitary covariance). Spec Def 5.1 lists a third clause: p(U† E U) = p_U(E) for every unitary U, "with the usual covariance interpretation for simultaneous transformation of preparation and effect structure." Two natural Lean encodings exist:

• Invariance reading — p (Effect.conjugateBy U E) = p E for all U. This over-constrains to basis-invariant packages (essentially the maximally mixed state); a pure-state package from |ψ⟩⟨ψ| does not satisfy it, since Tr(|ψ⟩⟨ψ| U† E U) = Tr(|Uψ⟩⟨Uψ| E), not Tr(|ψ⟩⟨ψ| E).
• Covariant reading — a functor OperationalPackage.conjugateBy U sending one package to another with (conjugateBy U OP).p E = OP.p (Effect.conjugateBy U E), preserving the nonneg / le_one / total / add fields. This is the mathematically correct encoding, but it's type-heavy and not needed by busch_effect_gleason as currently stated.

Rather than commit to the wrong reading, LF2 omits clause 3 from the structure and exposes Effect.conjugateBy below as the structural building block. LF4 (where unitary evolution enters non-trivially) is the right place to pick one of the two encodings; see specs/LF4-todo.md.

• p : Effect N → ℝ

  Probability assignment.

• nonneg (E : Effect N) : 0 ≤ self.p E

  0 ≤ p(E).

• le_one (E : Effect N) : self.p E ≤ 1

  p(E) ≤ 1.

• total_one : self.p Effect.one = 1

  p(I) = 1.

• additivity (E F : Effect N) (hLe : (1 - (E.M + F.M)).PosSemidef) : self.p (E.add F hLe) = self.p E + self.p F

  Finite additivity: if E + F ≤ I then p(E + F) = p(E) + p(F).

Rank-1 outer products

The construction |φ⟩⟨φ| as an N×N complex matrix, together with its basic algebraic properties (Hermitian, PSD, trace). This is the raw matrix layer; rankOneEffect / rankOneDensity (next phase) package it into the structure types above.

noncomputable def CSD.LF2.outerProduct {N : ℕ} (φ : EuclideanSpace ℂ (Fin N)) : Matrix (Fin N) (Fin N) ℂ

Rank-1 outer product. |φ⟩⟨φ| with entries M i j = φ i * star (φ j).

Equations

• CSD.LF2.outerProduct φ = Matrix.vecMulVec (fun (i : Fin N) => φ.ofLp i) fun (i : Fin N) => star (φ.ofLp i)

theorem CSD.LF2.outerProduct_posSemidef {N : ℕ} (φ : EuclideanSpace ℂ (Fin N)) : (outerProduct φ).PosSemidef

The outer product is positive semi-definite. Immediate from the general fact PosSemidef (vecMulVec a (star a)).

theorem CSD.LF2.outerProduct_isHermitian {N : ℕ} (φ : EuclideanSpace ℂ (Fin N)) : (outerProduct φ).IsHermitian

The outer product is Hermitian (a consequence of being PSD).

theorem CSD.LF2.outerProduct_trace {N : ℕ} (φ : EuclideanSpace ℂ (Fin N)) : (outerProduct φ).trace = inner ℂ φ φ

Trace of the outer product equals the Hilbert-space inner product inner ℂ φ φ.

theorem CSD.LF2.outerProduct_trace_of_unit_norm {N : ℕ} (φ : EuclideanSpace ℂ (Fin N)) (hφ : ‖φ‖ = 1) : (outerProduct φ).trace = 1

For a unit vector, the trace of the outer product is 1.

theorem CSD.LF2.dotProduct_self_star_of_unit_norm {N : ℕ} (φ : EuclideanSpace ℂ (Fin N)) (hφ : ‖φ‖ = 1) : ((fun (i : Fin N) => φ.ofLp i) ⬝ᵥ fun (i : Fin N) => star (φ.ofLp i)) = 1

Unfolding: the dot-product φ ⬝ᵥ star φ is the trace of the outer product. For a unit vector this equals 1.

theorem CSD.LF2.outerProduct_mul_self_of_unit_norm {N : ℕ} (φ : EuclideanSpace ℂ (Fin N)) (hφ : ‖φ‖ = 1) : outerProduct φ * outerProduct φ = outerProduct φ

Rank-1 projector is idempotent for a unit vector: P * P = P. This is the defining algebraic property of an orthogonal projection.

theorem CSD.LF2.one_sub_outerProduct_mul_self_of_unit_norm {N : ℕ} (φ : EuclideanSpace ℂ (Fin N)) (hφ : ‖φ‖ = 1) : (1 - outerProduct φ) * (1 - outerProduct φ) = 1 - outerProduct φ

1 - P is idempotent when P is. Ring calculation: (1-P)(1-P) = 1 - 2P + P² and P² = P gives 1 - P.

theorem CSD.LF2.one_sub_outerProduct_posSemidef {N : ℕ} (φ : EuclideanSpace ℂ (Fin N)) (hφ : ‖φ‖ = 1) : (1 - outerProduct φ).PosSemidef

Rank-1 complement is PSD. (I - |φ⟩⟨φ|).PosSemidef for unit φ. Proof: the matrix is Hermitian and idempotent, hence equal to its own product with its conjugate transpose, hence PSD.

noncomputable def CSD.LF2.rankOneEffect {N : ℕ} (φ : EuclideanSpace ℂ (Fin N)) (hφ : ‖φ‖ = 1) : Effect N

Rank-1 projector as an Effect. |φ⟩⟨φ| for a unit vector φ.

Equations

• CSD.LF2.rankOneEffect φ hφ = { M := CSD.LF2.outerProduct φ, isHermitian := ⋯, nonneg := ⋯, le_one := ⋯ }

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

Rank-1 pure-state density operator. |ψ⟩⟨ψ| for a unit vector ψ.

Equations

• CSD.LF2.rankOneDensity ψ hψ = { M := CSD.LF2.outerProduct ψ, isHermitian := ⋯, nonneg := ⋯, trace_one := ⋯ }

theorem CSD.LF2.born_quadratic {N : ℕ} (ψ φ : EuclideanSpace ℂ (Fin N)) (hψ : ‖ψ‖ = 1) (hφ : ‖φ‖ = 1) : traceForm (rankOneDensity ψ hψ) (rankOneEffect φ hφ) = ‖inner ℂ ψ φ‖ ^ 2

Spec §5.4 — the Born quadratic form. For a pure preparation |ψ⟩ and a rank-1 projector outcome |φ⟩⟨φ| (both with unit norm), the trace-form probability equals |⟨ψ|φ⟩|².

theorem CSD.LF2.pure_state_born_weights {N : ℕ} (OP : OperationalPackage N) (ψ : EuclideanSpace ℂ (Fin N)) (hψ : ‖ψ‖ = 1) (hρ : ∀ (E : Effect N), OP.p E = traceForm (rankOneDensity ψ hψ) E) (φ : EuclideanSpace ℂ (Fin N)) (hφ : ‖φ‖ = 1) : OP.p (rankOneEffect φ hφ) = ‖inner ℂ ψ φ‖ ^ 2

Composite endpoint (Busch-mediated form). For an operational package whose Busch-extracted density operator is rankOneDensity ψ (i.e., the preparation is the pure state |ψ⟩), the probability of a rank-1 outcome |φ⟩⟨φ| is |⟨ψ|φ⟩|².

The hypothesis hρ — that OP.p already agrees with the trace form of rankOneDensity ψ on every effect — is the downstream consumption of busch_effect_gleason for the pure-preparation case. It is derivable from a weaker purity hypothesis via rankOneDensity_unique_of_certainty + busch_effect_gleason; see pure_state_born_weights_of_certainty below for the strengthened form.

theorem CSD.LF2.rankOneDensity_unique_of_certainty {N : ℕ} (ψ : EuclideanSpace ℂ (Fin N)) (hψ : ‖ψ‖ = 1) (ρ : DensityOperator N) (h_certain : traceForm ρ (rankOneEffect ψ hψ) = 1) : ρ = rankOneDensity ψ hψ

Uniqueness of pure-state density from certainty.

A density operator ρ whose trace form pairs with |ψ⟩⟨ψ| to give 1 is necessarily |ψ⟩⟨ψ| itself. Equivalently, the only density operator that assigns probability one to the rank-1 projector through ψ is rankOneDensity ψ.

Carried as an axiom in earlier revisions; discharged on 2026-05-18 (see specs/LF4-todo.md §4 and AXIOMS.md §2.3). The proof bypasses the spectral theorem: the (I − P) ρ (I − P) sandwich is PSD with trace zero, hence zero; the PSD inner-product identity Matrix.PosSemidef.dotProduct_mulVec_zero_iff gives ρ · (I − P) = 0 without needing a square root; and the rank-1 sandwich identity P · M · P = Tr(M · P) • P collapses ρ to P.