LF2/EffectGleason: the Busch effect-Gleason theorem, PROVED (discharges the former axiom) #
Category: 3-Local (LF2 operational stratum — the effect-Gleason representation theorem).
Glossary: https://glossary.constraintsurfacedynamics.com/gleason-theorem/
Plain-language, CSD-role and formal statements of the Gleason and Busch theorems, with
this module as its Lean anchor. Kept symmetric by scripts/check-glossary.sh.
Earlier revisions of LF2/BornWrapper.lean imported the Busch effect-Gleason theorem as the
axiom busch_effect_gleason: every effect-additive, bounded, normalised probability assignment
OP.p on effects is OP.p E = Tr(ρ E) for a unique density operator ρ. This module
discharges that axiom — it is proved here as OperationalPackage.effect_gleason_representation
(2026-07-21), so the corpus imports zero axioms beyond the foundational triple
(CONVENTIONS.md §8.1, AXIOMS.md §2.2, specs/BACKLOG.md). The axiom was deleted from
BornWrapper.lean and its two named consumers (born_form_of_package,
pure_state_born_weights_of_certainty) relocated here (signatures unchanged), since they now
depend on the proof, which imports BornWrapper. Busch's proof (Busch 2003, "A Simple Proof of
Gleason's Theorem") is short in finite dimensions because additivity over the effect algebra
gives linearity directly, bypassing the frame-function analysis of projective Gleason.
Proof arc (bottom-up) #
- This module — the foundational layer (
pis a monotone, additive functional).Effect.smul—t • Eis an effect fort ∈ [0,1](the scalar action used throughout).OperationalPackage.p_zero—p 0 = 0(fromp 0 = p(0 ⊕ 0) = 2 p 0).OperationalPackage.p_mono—E.M ≤ F.M(Löwner) ⟹p E ≤ p F(additivity +nonneg).OperationalPackage.p_smul_add—p((a+b) • E) = p(a • E) + p(b • E)fora,b,a+b ∈ [0,1](scalar additivity oft ↦ p(t • E)on[0,1]).OperationalPackage.p_smul_mono—t ↦ p(t • E)is monotone on[0,1].
- This module — homogeneity
p(t • E) = t · p Efort ∈ [0,1](p_smul_homog,smulVal_homog): the monotone + additive (Cauchy) equationf(a+b) = f(a)+f(b)on[0,1]forcesf(t) = t f(1)— via integer scaling (smulVal_natMul), rational homogeneity (smulVal_rat), and the density squeeze (exists_rat_btwn+ monotonicity). - Reconstruction — spectral reduction, polarisation, and the ρ-build (delivered).
The spectral reduction is done:
p_finsetSum(finite additivity),Effect.eigenvalues_le_one(effect eigenvalues∈ [0,1]),Effect.sum_eigenEffect_M(E = ∑ᵢ λᵢ |eᵢ⟩⟨eᵢ|), andp_eq_eigen_sum(p(E) = ∑ᵢ λᵢ · p(|eᵢ⟩⟨eᵢ|)) reduce the whole representation problem to determiningpon rank-one projectors. The polarisation identities are done:outerProduct_parallelogram(|u+v⟩⟨u+v| + |u−v⟩⟨u−v| = 2|u⟩⟨u| + 2|v⟩⟨v|, cross terms cancel) andouterProduct_polarization_real— the algebraic core that letsp, being additive, inherit the parallelogram law. The sub-unit rank-one effectouterEffect v(|v⟩⟨v|for any‖v‖ ≤ 1, needed for the combinationsu ± v,u ± iv), the degree-2 homogeneityp_outerEffect_smul(p(|c·v⟩⟨c·v|) = c²·p(|v⟩⟨v|)), and the Cauchy–Schwarz sum boundone_sub_two_outerProduct_posSemidef(I − |a⟩⟨a| − |b⟩⟨b|PSD for‖a‖²+‖b‖²≤1, via CS not an eigenvalue bound), and thep-level parallelogram lawp_parallelogram(p(|u+v⟩⟨u+v|) + p(|u−v⟩⟨u−v|) = 2p(|u⟩⟨u|) + 2p(|v⟩⟨v|)for‖u‖²+‖v‖²≤½, from the matrix identity + additivity + the√2-doublingp_outerEffect_sqrt2) are done. The ρ-build (step 3b-final) is now done as well:qform(the degree-2 homogeneous extension ofv ↦ p(|v⟩⟨v|)off the unit ball) satisfies the unrestricted parallelogram law (qform_parallelogram), so it is quadratic-like (qform_isQuadraticLike) and the Jordan–von Neumann engine ofMathlib/Analysis/InnerProductSpace/Gleason/Polarization.lean(written here first, extracted 2026-09-21 for the projection form of Gleason's theorem) makes its polarisationGleason.polarbi-additive and — viaGleason.additive_bounded_linear, which replaces the classical continuity step by the bound0 ≤ q ≤ ‖·‖²—ℝ-bihomogeneous; the complex polarisationGleason.sesqis then sesquilinear withsesq q v v = q v, and its matrix on the standard basisqmatrixis Hermitian (qmatrix_isHermitian) withp_outerEffect_eq_trace : p(|v⟩⟨v|) = Tr(R · |v⟩⟨v|)and — through the spectral reduction —p_eq_trace : p E = Tr(R · E)for every effect. - Positivity / normalisation + uniqueness (step 4 — done).
p ≥ 0 ⟹ RPSD (qmatrix_posSemidef, throughGleason.posSemidef_of_sphere_nonneg);p I = 1 ⟹ Tr R = 1(qmatrix_trace_one); uniqueness because a Hermitian matrix is determined by its quadratic form on the unit sphere (Gleason.eq_of_sphere_quadForm_eq, a polarisation) viaqdensity_unique. This packagesR = qmatrixas theDensityOperatorqdensityand yieldseffect_gleason_representation(∃!), the statement the axiom asserted.
Honest scope #
Delivered here — the complete theorem. Steps 1–2 (monotone/additive layer + homogeneity
p(t•E) = t·p E), the spectral reduction (p(E) = ∑ᵢ λᵢ · p(|eᵢ⟩⟨eᵢ|)), the polarisation
identities (step 3b), the ρ-build (step 3b-final: p E = Tr(R · E), p_eq_trace), and
step 4 (PSD / unit-trace / uniqueness), assembled into
OperationalPackage.effect_gleason_representation. All foundational-triple (propext,
Classical.choice, Quot.sound), no sorry, no placeholder — verified by AxiomAudit. The
busch_effect_gleason axiom has been removed from BornWrapper.lean; this module is the
proof.
References: LF2/BornWrapper.lean (Effect, DensityOperator, OperationalPackage,
traceForm, rankOneDensity_unique_of_certainty, born_quadratic); Busch 2003
(quant-ph/9909073); Jordan–von Neumann 1935
(the parallelogram characterisation, polarised in Gleason/Polarization.lean); AXIOMS.md §2.2;
CONVENTIONS.md §8.1; specs/BACKLOG.md; specs/future-work.md.
A finite sum of effects whose total is ≤ I is an effect. Hermiticity and PSD of the
sum are automatic; le_one is the hypothesis (as in Effect.add).
Equations
- CSD.LF2.Effect.finsetSum s E h = { M := ∑ i ∈ s, (E i).M, isHermitian := ⋯, nonneg := ⋯, le_one := h }
Instances For
p 0 = 0. From additivity p 0 = p(0 ⊕ 0) = 2 · p 0.
Monotonicity. If E.M ≤ F.M in the Löwner order (F.M - E.M PSD), then p E ≤ p F.
Write F = E ⊕ (F − E), an effect sum, and use p(F−E) ≥ 0.
Scalar additivity of t ↦ p(t • E) on [0,1]. For a, b ≥ 0 with a + b ≤ 1,
p((a+b) • E) = p(a • E) + p(b • E) — the Cauchy relation whose monotone solution is
p(t • E) = t · p E (p_smul_homog).
t ↦ p(t • E) is monotone on [0,1]. Immediate from p_mono: s ≤ t gives
(t − s) • E.M PSD, so s • E.M ≤ t • E.M.
C — homogeneity p(t • E) = t · p E on [0,1] (Route B step 2) #
The monotone + additive (Cauchy) functional equation f(a+b) = f(a)+f(b) on [0,1] forces
f(t) = t·f(1). We package f(t) = p(t•E) as a total function smulVal (0 outside [0,1])
to avoid carrying the 0 ≤ t ≤ 1 proofs, prove homogeneity on the naturals-ratio m/n (from
additivity), and squeeze to all reals by density of the rationals + monotonicity.
p(t • E) as a total function of t (0 outside [0,1]), for the Cauchy/monotone analysis.
Instances For
Homogeneity (the Cauchy/monotone squeeze). p(t • E) = t · p(E) for all t ∈ [0,1].
The rational homogeneity + monotonicity pin smulVal E t between q·c values for rationals
q arbitrarily close to t (density), forcing smulVal E t = t·c with c = p(E).
Homogeneity, effect form. p(t • E) = t · p(E) for t ∈ [0,1].
D — finite additivity (Route B step 3, building block) #
Finite additivity. For a family of effects whose total is ≤ I, p(∑ᵢ Eᵢ) = ∑ᵢ p(Eᵢ).
Induction on the index set via the pairwise additivity; each partial sum stays ≤ I because
the omitted effects are PSD. The prerequisite for reducing p on an arbitrary effect to p on
the rank-one projectors of its spectral decomposition.
E — spectral reduction (Route B step 3): p(E) = ∑ᵢ λᵢ · p(|eᵢ⟩⟨eᵢ|) #
Effect eigenvalues are ≤ 1. For an effect E (so 1 - E.M is PSD), each eigenvalue of
E.M is ≤ 1: on the eigenvector eᵢ, ⟨eᵢ, (1-E.M) eᵢ⟩ = 1 - λᵢ ≥ 0.
The eigenvalue-scaled rank-one projectors of an effect are effects. λᵢ • |eᵢ⟩⟨eᵢ| with
λᵢ = eigenvalues i ∈ [0,1] and eᵢ = eigenvectorBasis i (unit norm).
Equations
- E.eigenEffect i = CSD.LF2.Effect.smul (⋯.eigenvalues i) ⋯ ⋯ (CSD.LF2.rankOneEffect (⋯.eigenvectorBasis i) ⋯)
Instances For
E is the finite sum of its eigen-effects. E.M = ∑ᵢ λᵢ |eᵢ⟩⟨eᵢ| (the Hermitian spectral
theorem, same computation as density_eq_eigen_ensemble).
Spectral reduction of p (Route B step 3). For every effect E,
p(E) = ∑ᵢ λᵢ · p(|eᵢ⟩⟨eᵢ|) — the eigenvalue-weighted sum of p on the rank-one projectors of
E's spectral decomposition. Reduces the entire representation problem to determining p on
rank-one projectors. Combines finite additivity + homogeneity with the spectral theorem.
F0 — the sub-unit rank-one effect |v⟩⟨v| for ‖v‖ ≤ 1 #
rankOneEffect is defined only for unit vectors. The polarisation reconstruction needs
|v⟩⟨v| as an effect for the (generally non-unit) combinations u ± v, u ± iv; this requires
‖v‖ ≤ 1.
outerProduct under complex scaling. |c•v⟩⟨c•v| = |c|² · |v⟩⟨v|.
The sub-unit rank-one effect |v⟩⟨v| for ‖v‖ ≤ 1. PSD is automatic; le_one holds
because 1 - |v⟩⟨v| = (1 - |v̂⟩⟨v̂|) + (1-‖v‖²)|v̂⟩⟨v̂|, both PSD.
Equations
- CSD.LF2.outerEffect v hv = { M := CSD.LF2.outerProduct v, isHermitian := ⋯, nonneg := ⋯, le_one := ⋯ }
Instances For
On a unit vector, outerEffect agrees with rankOneEffect.
F — the polarisation identities (Route B step 3b, building blocks) #
The reconstruction of ρ from the rank-one values φ ↦ p(|φ⟩⟨φ|) rests on polarisation: the
diagonal quadratic form must come from a sesquilinear form. Its algebraic core is that the
outer products satisfy the parallelogram law at the matrix level — the cross terms of
|u±v⟩⟨u±v| cancel — so p, being additive, inherits the parallelogram law.
Matrix parallelogram identity for outer products.
|u+v⟩⟨u+v| + |u−v⟩⟨u−v| = 2|u⟩⟨u| + 2|v⟩⟨v|: the off-diagonal cross terms
|u⟩⟨v| + |v⟩⟨u| appear with opposite signs in the two sums and cancel. Pure matrix algebra.
Rank-one polarisation (real part).
|u+v⟩⟨u+v| − |u−v⟩⟨u−v| = 2(|u⟩⟨v| + |v⟩⟨u|): the difference isolates the cross terms
(the "real part" of the sesquilinear form the reconstruction recovers).
F1 — the Cauchy–Schwarz sum-of-projectors bound (Route B step 3b) #
The additivity step of the p-level parallelogram needs |a⟩⟨a| + |b⟩⟨b| ≤ I when
‖a‖² + ‖b‖² ≤ 1. This is Cauchy–Schwarz, not an eigenvalue bound:
⟨x, (I − |a⟩⟨a| − |b⟩⟨b|) x⟩ = ‖x‖² − |⟨a,x⟩|² − |⟨b,x⟩|² ≥ ‖x‖²(1 − ‖a‖² − ‖b‖²) ≥ 0.
Cauchy–Schwarz sum bound. For ‖a‖² + ‖b‖² ≤ 1, I − |a⟩⟨a| − |b⟩⟨b| is PSD.
⟨x, (I − |a⟩⟨a| − |b⟩⟨b|) x⟩ = ‖x‖² − |⟨a,x⟩|² − |⟨b,x⟩|² ≥ ‖x‖²(1 − ‖a‖² − ‖b‖²) ≥ 0.
G — p-level homogeneity of the rank-one form (Route B step 3b) #
Homogeneity of the rank-one value. p(|c·v⟩⟨c·v|) = c² · p(|v⟩⟨v|) for real c ∈ [0,1]
and ‖v‖ ≤ 1: |c·v⟩⟨c·v| = c² • |v⟩⟨v| = Effect.smul c² |v⟩⟨v|, then apply p_smul_homog.
The degree-2 homogeneity of the quadratic form v ↦ p(|v⟩⟨v|).
p depends only on the vector, not the norm-bound proof. For equal vectors, the
outerEffect values (and hence their p) agree.
√2-doubling of the rank-one value. p(|√2·v⟩⟨√2·v|) = 2·p(|v⟩⟨v|). Inverts
p_outerEffect_smul at c = 1/√2: |v⟩⟨v| = ½·|√2·v⟩⟨√2·v|.
The p-level parallelogram law (Route B step 3b). For ‖u‖² + ‖v‖² ≤ ½,
p(|u+v⟩⟨u+v|) + p(|u−v⟩⟨u−v|) = 2·p(|u⟩⟨u|) + 2·p(|v⟩⟨v|). The matrix parallelogram identity
(outerProduct_parallelogram) makes the two effect-sums equal; additivity (with the CS sum
bound as the ≤ I hypothesis) + the √2-doubling homogeneity give the scalar 2s. This is the
property that forces the diagonal form v ↦ p(|v⟩⟨v|) to come from a sesquilinear form.
H — the global quadratic form q v = ‖v‖² · p(|v̂⟩⟨v̂|) (Route B step 3b-final) #
p (outerEffect v ·) lives only on the sub-unit ball, while the polarisation argument needs a
quadratic form defined on all vectors (the combinations u ± v, u ± i·v leave the ball). The
degree-2 homogeneous extension q supplies it: it agrees with p ∘ outerEffect where the
latter is defined (qform_eq_p), so the sub-unit p_parallelogram becomes the unrestricted
parallelogram law (qform_parallelogram).
|c·v⟩⟨c·v| = |v⟩⟨v| for a phase ‖c‖ = 1.
p on outerEffect depends only on the matrix |v⟩⟨v|.
The global quadratic form q v = ‖v‖² · p(|v̂⟩⟨v̂|), v̂ = ‖v‖⁻¹ • v.
p (outerEffect v ·) is defined only for ‖v‖ ≤ 1; the reconstruction needs a quadratic form
on all of EuclideanSpace ℂ (Fin N). The formula gives q 0 = 0 automatically (the ‖v‖²
factor), agrees with p ∘ outerEffect on the sub-unit ball (qform_eq_p), and is degree-2
homogeneous under arbitrary complex scaling (qform_smul).
Instances For
0 ≤ q v (from OP.nonneg).
q v ≤ ‖v‖² (from OP.le_one). With qform_nonneg this is the local bound feeding the
Cauchy-equation argument in Gleason.IsQuadraticLike.polar_smul_real.
q 0 = 0.
Degree-2 homogeneity of q under complex scaling: q(c • v) = ‖c‖² · q v. The modulus
of c scales the ‖v‖² prefactor; its phase is invisible to |v⟩⟨v|
(outerProduct_smul_of_norm_one).
q agrees with p ∘ outerEffect on the sub-unit ball: q v = p(|v⟩⟨v|) for ‖v‖ ≤ 1.
The bridge between the global quadratic form and the operational data (p_outerEffect_smul at
c = ‖v‖).
q is even: q(−v) = q v (the unit phase −1).
The unrestricted parallelogram law for q. q(u+v) + q(u−v) = 2 q u + 2 q v for all
u, v — the sub-unit p_parallelogram transported off the ball by scaling both vectors down by
t = (2(1+‖u‖+‖v‖))⁻¹ and dividing out t² (qform_smul). This is the hypothesis of the
Jordan–von Neumann argument below.
I–L — the Jordan–von Neumann reconstruction (Gleason/Polarization.lean) #
qform is quadratic-like in the sense of Gleason.IsQuadraticLike (qform_isQuadraticLike), so
the polarisation engine of Mathlib/Analysis/InnerProductSpace/Gleason/Polarization.lean — the
bi-additive difference Gleason.polar, the sesquilinear form Gleason.sesq and its matrix
Gleason.polarMatrix — applies verbatim: qmatrix := Gleason.polarMatrix qform is Hermitian with
q v = ⟨v, R v⟩. The engine was written here first (2026-07-21) and extracted unchanged on
2026-09-21 so that the projection form of Gleason's theorem shares it
(specs/gleason-feasibility.md).
qform is quadratic-like: degree-2 homogeneous, parallelogram, 0 ≤ q ≤ ‖·‖² — the
four hypotheses of the Jordan–von Neumann engine.
The reconstructed matrix R = polarMatrix qform (R j k = S(eⱼ, eₖ) on the standard
basis) — the candidate density operator of Busch's theorem (its positivity and unit trace are
step 4).
Equations
- OP.qmatrix = Gleason.polarMatrix OP.qform
Instances For
R is Hermitian (Gleason.IsQuadraticLike.polarMatrix_isHermitian).
q is the quadratic form of R: q v = ⟨v, R v⟩
(Gleason.IsQuadraticLike.eq_dotProduct).
q v = Re ⟨v, R v⟩, the form the sphere lemmas of Gleason/Descent.lean take.
Tr(R · |v⟩⟨v|) = ⟨v, R v⟩. The trace pairing against an outer product is the
quadratic form of R (Gleason.trace_mul_vecMulVec on the outerProduct).
The rank-one representation (Route B step 3b-final). p(|v⟩⟨v|) = Tr(R · |v⟩⟨v|) for
every sub-unit v: the operational probability of every rank-one effect is a trace against one
fixed Hermitian matrix. This is what the polarisation programme was for.
Full representation on all effects (Route B step 3b-final, capstone).
p E = Tr(R · E) for every effect E — the rank-one representation lifted through the
spectral reduction (p_eq_eigen_sum, Effect.sum_eigenEffect_M).
This is the content of Busch's theorem except the state conditions on R. What remains
(step 4) is R.PosSemidef (from OP.nonneg), R.trace = 1 (from OP.total_one), and
uniqueness (non-degeneracy of the trace pairing) — which together make R a DensityOperator
and replace the busch_effect_gleason axiom in LF2/BornWrapper.lean.
M — step 4: positivity, normalisation, uniqueness, and the discharged theorem #
(Route B step 4, capstone)
The three state conditions on the reconstructed R = OP.qmatrix: R.PosSemidef (from
OP.nonneg, through Gleason.posSemidef_of_sphere_nonneg), R.trace = 1 (from
OP.total_one), and uniqueness, from the fact that a Hermitian matrix is determined by its
quadratic form on the unit sphere (Gleason.eq_of_sphere_quadForm_eq, a polarisation). Together
they package R as a DensityOperator and prove effect_gleason_representation, the statement
the busch_effect_gleason axiom used to assert. The sphere lemmas live in
Mathlib/Analysis/InnerProductSpace/Gleason/Descent.lean, shared with the projection form of
Gleason's theorem.
Step 4a — the reconstructed matrix is positive semidefinite. R.PosSemidef from
qform_nonneg on the unit sphere and qform_eq_re_dotProduct, through
Gleason.posSemidef_of_sphere_nonneg.
Step 4b — the reconstructed matrix has unit trace. R.trace = 1 from OP.total_one
(p I = 1) and p_eq_trace at E = Effect.one (Tr(R · I) = Tr R).
The reconstructed density operator R = OP.qmatrix, packaged with its PSD + unit-trace
witnesses.
Instances For
p is the trace form of qdensity. From p_eq_trace (↑(p E) = Tr(R·E)) and
traceForm_ofReal (↑(traceForm ρ E) = Tr(R·E)), by injectivity of ℝ ↪ ℂ.
Step 4c — uniqueness. Any density operator whose trace form reproduces p on every
effect equals qdensity: on the rank-one effects |v⟩⟨v| of the unit sphere both ρ.M and R
have quadratic form q v, and a Hermitian matrix is determined by its quadratic form on the
sphere (Gleason.eq_of_sphere_quadForm_eq).
Busch effect-Gleason (finite dim), proved. For every operational package there is a
unique density operator ρ with p E = Tr(ρ · E) for every effect. This discharges the
busch_effect_gleason axiom: qdensity witnesses existence (p_eq_traceForm_qdensity) and
qdensity_unique gives uniqueness.
Born-form assignment (spec §5.4 wrapper). The unique density operator representing an
operational package — now a theorem (effect_gleason_representation), not an axiom. The
dimension hypothesis hN : 2 ≤ N is retained for signature compatibility with the spec and with
downstream callers, though the reconstruction in fact works for every N.
Strengthened composite endpoint. Given only a purity hypothesis — that the
operational package assigns probability one to the rank-1 effect through ψ, i.e. the
preparation is "certain" to produce ψ — the Born quadratic form |⟨ψ|φ⟩|² falls out for every
rank-1 outcome. Relocated from LF2/BornWrapper.lean (2026-07-21) because it now composes the
proven effect_gleason_representation (was busch_effect_gleason) with
rankOneDensity_unique_of_certainty and born_quadratic; hN is retained for the spec
signature.