SigmaLayer/MixedState: mixed-state representation and statistical mixtures

Category: 7-SigmaLayer (the projective-sector layer (Paper C)).

Ledger target T9, the mixed-state representation. The repository already carries the Born rule on density operators (LF2.BornWrapper.traceForm, Tr(ρ E)), the pure-state density (rankOneDensity ψ = |ψ⟩⟨ψ|), and the pure Born quadratic form (born_quadratic). The gap this module closes is the statistical mixture / ensemble structure: convex combinations of density operators and the affine dependence of the Born rule on the state, together with a purity predicate.

• mix p ρ₁ ρ₂ — the convex combination p ρ₁ + (1-p) ρ₂ is a genuine density operator (Hermitian, PSD, trace one): the classical mixture of two preparations.
• traceForm_mix — the Born rule is affine in the state: mixing preparations mixes the outcome probabilities, Tr((p ρ₁ + (1-p) ρ₂) E) = p Tr(ρ₁ E) + (1-p) Tr(ρ₂ E). This is the defining property of a statistical mixture and the reason density operators, not just state vectors, are the right state space.
• IsPure / rankOneDensity_isPure / isPure_iff_trace_sq_one — the purity predicate (ρ² = ρ), the fact that rank-one densities are pure, and the full purity characterisation IsPure ρ ↔ Tr(ρ²) = 1 (the converse isPure_of_trace_sq_one via the spectral theorem: ∑λᵢ = ∑λᵢ² = 1, λᵢ ≥ 0 forces λᵢ ∈ {0,1}).
• maximallyMixed / maximallyMixed_not_isPure — a genuinely mixed state: I/N is a density operator and, for N ≥ 2, is not pure, so the mixture structure is not vacuous.

This is the mixed-state layer Mathlib does not supply (no density-matrix type upstream); it is built on the repository's LF2.DensityOperator/Effect and traceForm.

theorem CSD.SigmaLayer.isSelfAdjoint_ofReal (r : ℝ) : IsSelfAdjoint ↑r

(r : ℂ) is self-adjoint for real r (its conjugate is itself).

theorem CSD.SigmaLayer.posSemidef_real_smul {N : ℕ} {A : Matrix (Fin N) (Fin N) ℂ} (hA : A.PosSemidef) {p : ℝ} (hp : 0 ≤ p) : (↑p • A).PosSemidef

A nonnegative real multiple of a positive semidefinite complex matrix is positive semidefinite.

The convex mixture of density operators

noncomputable def CSD.SigmaLayer.mix {N : ℕ} (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (ρ₁ ρ₂ : LF2.DensityOperator N) : LF2.DensityOperator N

The statistical mixture of two density operators. The convex combination p ρ₁ + (1-p) ρ₂ (with 0 ≤ p ≤ 1) is itself a density operator: the classical mixture of two quantum preparations.

Equations

• CSD.SigmaLayer.mix p hp0 hp1 ρ₁ ρ₂ = { M := ↑p • ρ₁.M + ↑(1 - p) • ρ₂.M, isHermitian := ⋯, nonneg := ⋯, trace_one := ⋯ }

@[simp]

theorem CSD.SigmaLayer.mix_M {N : ℕ} (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (ρ₁ ρ₂ : LF2.DensityOperator N) : (mix p hp0 hp1 ρ₁ ρ₂).M = ↑p • ρ₁.M + ↑(1 - p) • ρ₂.M

theorem CSD.SigmaLayer.traceForm_mix {N : ℕ} (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (ρ₁ ρ₂ : LF2.DensityOperator N) (E : LF2.Effect N) : LF2.traceForm (mix p hp0 hp1 ρ₁ ρ₂) E = p * LF2.traceForm ρ₁ E + (1 - p) * LF2.traceForm ρ₂ E

The Born rule is affine in the state. Mixing preparations mixes the outcome probabilities: Tr((p ρ₁ + (1-p) ρ₂) E) = p Tr(ρ₁ E) + (1-p) Tr(ρ₂ E). The defining property of a statistical mixture, and the reason density operators are the right state space.

Purity

def CSD.SigmaLayer.IsPure {N : ℕ} (ρ : LF2.DensityOperator N) : Prop

A density operator is pure iff it is a projector (ρ² = ρ, hence rank one given trace one); otherwise it is a genuine statistical mixture.

Equations

• CSD.SigmaLayer.IsPure ρ = (ρ.M * ρ.M = ρ.M)

theorem CSD.SigmaLayer.rankOneDensity_isPure {N : ℕ} (ψ : EuclideanSpace ℂ (Fin N)) (hψ : ‖ψ‖ = 1) : IsPure (LF2.rankOneDensity ψ hψ)

Rank-one densities are pure. The pure-state density |ψ⟩⟨ψ| (unit ψ) is a projector.

theorem CSD.SigmaLayer.IsPure.trace_sq_one {N : ℕ} {ρ : LF2.DensityOperator N} (h : IsPure ρ) : (ρ.M * ρ.M).trace = 1

Purity witness. A pure state has Tr(ρ²) = 1.

theorem CSD.SigmaLayer.isPure_of_trace_sq_one {N : ℕ} {ρ : LF2.DensityOperator N} (h : (ρ.M * ρ.M).trace = 1) : IsPure ρ

Purity from the trace witness (the converse). A density operator with Tr(ρ²) = 1 is pure. Via the spectral theorem: the eigenvalues λᵢ ≥ 0 satisfy ∑λᵢ = ∑λᵢ² = 1, forcing each λᵢ ∈ {0,1} (so λᵢ² = λᵢ), whence ρ² = ρ by diagonalisation.

theorem CSD.SigmaLayer.isPure_iff_trace_sq_one {N : ℕ} {ρ : LF2.DensityOperator N} : IsPure ρ ↔ (ρ.M * ρ.M).trace = 1

Purity characterisation. A density operator is pure iff Tr(ρ²) = 1.

A genuinely mixed state

noncomputable def CSD.SigmaLayer.maximallyMixed (N : ℕ) [NeZero N] : LF2.DensityOperator N

The maximally mixed state I/N. A density operator representing complete ignorance; the canonical genuinely-mixed preparation.

Equations

• CSD.SigmaLayer.maximallyMixed N = { M := ↑(↑N)⁻¹ • 1, isHermitian := ⋯, nonneg := ⋯, trace_one := ⋯ }

theorem CSD.SigmaLayer.maximallyMixed_not_isPure {N : ℕ} [NeZero N] (hN : 2 ≤ N) : ¬IsPure (maximallyMixed N)

The maximally mixed state is genuinely mixed. For N ≥ 2, I/N is not pure: the mixture structure is not vacuous, there exist states that are not rank-one projectors.

T9 capstone

theorem CSD.SigmaLayer.mixedState_capstone {N : ℕ} (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (ρ₁ ρ₂ : LF2.DensityOperator N) (E : LF2.Effect N) : LF2.traceForm (mix p hp0 hp1 ρ₁ ρ₂) E = p * LF2.traceForm ρ₁ E + (1 - p) * LF2.traceForm ρ₂ E

T9: the mixed-state representation. Density operators are the right state space: convex mixtures of density operators are density operators (mix), the Born rule is affine in the state (traceForm_mix -- mixing preparations mixes probabilities), pure states are the rank-one projectors (rankOneDensity_isPure), and there are genuinely mixed states (maximallyMixed_not_isPure). The pure Born rule (born_quadratic) is the extreme-point case.