Finite-dimensional effects, density operators and pure-state Born weights

Category: 3-Local (LF2 matrix interfaces).

Effect packages 0 ≤ E ≤ I; DensityOperator packages a positive semidefinite, trace-one matrix. OperationalPackage specifies a nonnegative, normalized assignment on all effects, additive whenever their sum remains an effect. Its probability upper-bound field is redundant, derivable by additivity with the complementary effect.

This file proves the outer-product identities, pure-state Born quadratic form and rankOneDensity_unique_of_certainty. The Busch representation theorem is proved in LF2/EffectGleason.lean, which imports this module; it is not an axiom imported here.

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

A nonnegative, normalized assignment on all effects, additive whenever the sum remains an effect. The upper-bound field is derivable from the other fields using I - E. No unitary-invariance or continuity premise is assumed.

Why unitary covariance is not a field. Spec Def 5.1 lists a third clause, p(U† E U) = p_U(E). Read as invariance — p (Effect.conjugateBy U E) = p E for every U — it over-constrains to basis-invariant packages, which a pure-state package does not satisfy. Read covariantly it is a map between packages, which is the right encoding and is not needed by the representation theorem. The structure therefore omits the clause and exposes Effect.conjugateBy as the building block; LF4 is where unitary evolution enters non-trivially and one of the two readings has to be chosen.

• 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 package it into the structure types above.

The outer product is stated on an arbitrary finite index ι (not just Fin N): the Fin N structures above and the index-parametric DensityOperatorIx (LF2/ReducedDensity.lean, LF2/MixedEnsembleIx.lean) share one definition.

noncomputable def CSD.LF2.outerProduct {ι : Type u_1} (φ : EuclideanSpace ℂ ι) : Matrix ι ι ℂ

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

Equations

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

theorem CSD.LF2.outerProduct_posSemidef {ι : Type u_1} [Fintype ι] (φ : EuclideanSpace ℂ ι) : (outerProduct φ).PosSemidef

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

theorem CSD.LF2.outerProduct_isHermitian {ι : Type u_1} [Fintype ι] (φ : EuclideanSpace ℂ ι) : (outerProduct φ).IsHermitian

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

theorem CSD.LF2.outerProduct_trace {ι : Type u_1} [Fintype ι] (φ : EuclideanSpace ℂ ι) : (outerProduct φ).trace = inner ℂ φ φ

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

theorem CSD.LF2.outerProduct_trace_of_unit_norm {ι : Type u_1} [Fintype ι] (φ : EuclideanSpace ℂ ι) (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 {ι : Type u_1} [Fintype ι] (φ : EuclideanSpace ℂ ι) (hφ : ‖φ‖ = 1) : ((fun (i : ι) => φ.ofLp i) ⬝ᵥ fun (i : ι) => 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 {ι : Type u_1} [Fintype ι] (φ : EuclideanSpace ℂ ι) (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.outerProduct_mul_outerProduct_trace {ι : Type u_1} [Fintype ι] (ψ φ : EuclideanSpace ℂ ι) : (outerProduct ψ * outerProduct φ).trace = ↑(‖inner ℂ ψ φ‖ ^ 2)

The trace of a product of two outer products is the squared overlap: Tr(|ψ⟩⟨ψ| · |φ⟩⟨φ|) = |⟨ψ, φ⟩|². The matrix core of the Born quadratic form (born_quadratic, DensityOperatorIx.traceForm_rankOne_outerProduct).

theorem CSD.LF2.one_sub_outerProduct_mul_self_of_unit_norm {ι : Type u_1} [Fintype ι] [DecidableEq ι] (φ : EuclideanSpace ℂ ι) (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 {ι : Type u_1} [Fintype ι] [DecidableEq ι] (φ : EuclideanSpace ℂ ι) (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.

theorem CSD.LF2.IsHermitian.eq_eigen_outer {ι : Type u_1} [Fintype ι] [DecidableEq ι] {C : Matrix ι ι ℂ} (hC : C.IsHermitian) : C = ∑ i : ι, ↑(hC.eigenvalues i) • outerProduct (hC.eigenvectorBasis i)

Entrywise spectral decomposition of a Hermitian matrix as an eigenvalue-weighted sum of rank-one eigenvector projectors: C = ∑ᵢ λᵢ |eᵢ⟩⟨eᵢ|. The Hermitian spectral theorem in diagonalised form, expanded entrywise. SigmaLayer.density_eq_eigen_ensemble and DensityOperatorIx.eq_eigen_ensemble are its density-operator instances.

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 OperationalPackage.effect_gleason_representation for the pure-preparation case. It is derivable from a weaker purity hypothesis via rankOneDensity_unique_of_certainty + OperationalPackage.effect_gleason_representation; see pure_state_born_weights_of_certainty in LF2/EffectGleason.lean 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.