Proposition 7 — equal mixtures have equal spans

Proved

UnphysicalHilbert.prop7_equal_mixtures_same_span

by Lucas · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

density-operatorquantum-mechanics

Let $H$ be a complex inner product space and let $(\psi_i)_{i\in I}$ , $(\phi_j)_{j\in J}$ be finite families of unit vectors. Suppose there are weights $a_i>0$ , $b_j>0$ with $\sum_i a_i=1$ , $\sum_j b_j=1$ and

\sum_{i\in I} a_i\,|\psi_i\rangle\langle\psi_i|=\sum_{j\in J} b_j\,|\phi_j\rangle\langle\phi_j| .

Then

\operatorname{span}\{\psi_i : i\in I\}=\operatorname{span}\{\phi_j : j\in J\}.

Two decompositions of the same mixed state into pure states involve pure states from the same subspace; this is one direction of the paper's identification of superposition with non-unique decomposition of mixtures (Proposition 9).

Formalization Note Finite sets are encoded as finite indexed families; $H$ need not be complete.

Preamble

import Definitions.Def_UnphysicalHilbert_StateSpace

Formal statement

namespace UnphysicalHilbert

/-- Proposition 7: two finite families of pure states giving the same strictly convex
mixture span the same subspace. -/
theorem prop7_equal_mixtures_same_span
    {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
    {ι κ : Type*} [Fintype ι] [Fintype κ]
    (ψ : ι → H) (ϕ : κ → H) (hψ : IsNormalizedFamily ψ) (hϕ : IsNormalizedFamily ϕ)
    (a : ι → ℝ) (b : κ → ℝ) (ha : IsStrictConvexWeights a) (hb : IsStrictConvexWeights b)
    (hab : mixture a ψ = mixture b ϕ) :
    Submodule.span ℂ (Set.range ψ) = Submodule.span ℂ (Set.range ϕ) := by
  sorry

end UnphysicalHilbert

Source

G. Carcassi, C. A. Aidala, F. Calderón, *The unphysicality of Hilbert spaces*, arXiv:2308.06669v3 [quant-ph], 22 Dec 2024, https://arxiv.org/abs/2308.06669, Appendix A, p. 8, Proposition 7

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph