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); the Jordan–von Neumann argument makes its polarisationqpolarbi-additive (qpolar_add_left) and — viaadditive_bounded_linear, which replaces the classical continuity step by the bound0 ≤ q ≤ ‖·‖²—ℝ-bihomogeneous (qpolar_smul_real); the complex polarisationqsesqis then sesquilinear (qsesq_add_right,qsesq_smul_right,qsesq_conj_symm) withqsesq_self : S(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);p I = 1 ⟹ Tr R = 1(qmatrix_trace_one); uniqueness because a complex matrix is determined by its quadratic form (matrix_eq_zero_of_quadForm_zero, 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 §J–§K); 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 (the deferred homogeneity step).
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
rank-one projectors 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 rank-one projectors.
|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 qpolar_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 — Cauchy's functional equation with a local bound (Route B step 3b-final) #
The Jordan–von Neumann polarisation gives additivity of f u v = q(u+v) − q(u−v) in each slot,
hence ℚ-homogeneity. Upgrading to ℝ-homogeneity is where the classical proof invokes
continuity — unavailable here, since p is an arbitrary probability assignment. Boundedness is
the substitute: 0 ≤ q ≤ ‖·‖² bounds f on the unit ball, and a bounded additive function on
ℝ is linear.
Cauchy's functional equation with a local bound. An additive g : ℝ → ℝ that is bounded
on [-1,1] is linear: g t = t · g 1.
No continuity is assumed (and none is available: p is an arbitrary probability assignment).
The proof is the classical squeeze on h y = g y − y · g 1: h is additive, kills every
integer (h m = m · h 1 = 0), and is bounded on [-1,1]; for any x and any n ≥ 1,
n · h x = h (n x − ⌊n x⌋) lands in that bounded window, so |h x| ≤ (M + |g 1|)/n → 0.
Used by OperationalPackage.qpolar_smul_real, where the local bound comes from qform_nonneg
and qform_le_normSq.
J — the polarisation difference f u v = q(u+v) − q(u−v) (Route B step 3b-final) #
The polarisation difference f u v = q(u+v) − q(u−v) — four times the real part of the
sesquilinear form being reconstructed. Symmetric (qpolar_symm), additive (qpolar_add_left)
and ℝ-homogeneous (qpolar_smul_real) in each slot.
Instances For
f is symmetric: q(v−u) = q(−(u−v)) = q(u−v).
f 0 v = q v − q(−v) = 0 (evenness of q).
f u (−v) = − f u v (the two q-terms swap).
The halving identity (Jordan–von Neumann core). f u v + f w v = 2 · f ((u+w)/2) v:
apply the parallelogram law at (a ± v, b) with a = (u+w)/2, b = (u−w)/2 (so a + b = u
and a − b = w) and subtract the two instances — the q b terms cancel.
Additivity of the polarisation difference in the first slot. f (u+w) v = f u v + f w v:
the halving identity at (u, w) and at (u+w, 0) (where f 0 v = 0) share a right-hand
side.
Real homogeneity of the polarisation difference in the first slot. f (t • u) v = t · f u v for every real t. Additivity alone gives only ℚ-homogeneity; the upgrade to ℝ
is additive_bounded_linear, whose local bound is 0 ≤ q ≤ ‖·‖² (qform_nonneg,
qform_le_normSq) — no continuity of p is needed or available.
K — the polarised sesquilinear form S (Route B step 3b-final) #
With f bi-additive and ℝ-bihomogeneous, the complex polarisation
S(u,v) = ¼ f(u,v) − (i/4) f(u, i·v) is sesquilinear: linear in v (the i-homogeneity
S(u, i·v) = i·S(u,v) is pure algebra of the formula), conjugate-linear in u by conjugate
symmetry, and S(v,v) = q v.
The polarised sesquilinear form.
S(u,v) = ¼ f(u,v) − (i/4) f(u, i·v), the complex polarisation of q. It is additive
(qsesq_add_right) and ℂ-homogeneous (qsesq_smul_right) in v, conjugate-symmetric
(qsesq_conj_symm), and restricts to q on the diagonal (qsesq_self) — exactly the
sesquilinear form whose matrix is the density operator Busch's theorem asserts.
Instances For
S(u, 0) = 0.
Additivity of f in the second slot (by symmetry from qpolar_add_left).
Real homogeneity of f in the second slot (by symmetry from qpolar_smul_real).
Additivity of S in the second slot.
Real homogeneity of S in the second slot.
S(u, i·v) = i · S(u,v) — pure algebra of the polarisation formula (i·(i·v) = −v),
no additivity needed.
Complex homogeneity in the second slot: S(u, c•v) = c · S(u,v). Split
c = Re c + i · Im c and combine qsesq_smul_real_right with qsesq_smul_I_right.
Conjugate symmetry: S(v,u) = conj (S(u,v)). The real part is symmetric
(qpolar_symm); the imaginary part flips because q(v ± i·u) = q(u ∓ i·v) (multiply by the
unit phase ∓i and use qform_smul). With qsesq_smul_right this makes S conjugate-linear
in its first slot.
S restricts to q on the diagonal: S(v,v) = q v. The diagonal value is
f v v = 4 q v (degree-2 homogeneity at 2), and the imaginary term vanishes because
q(v − i·v) = q(v + i·v) (unit phase −i). Both steps are the same witness,
OperationalPackage.qform_smul (q(c • v) = ‖c‖² q v): at c = 2 it gives the diagonal value,
and at c = −i it gives ‖−i‖² = 1, collapsing the imaginary term.
L — the reconstructed matrix R and the representation theorem (Route B step 3b-final) #
R j k := S(eⱼ, eₖ) on the standard basis. Sesquilinearity turns the basis expansion of v
into q v = ⟨v, R v⟩ = Tr(R · |v⟩⟨v|), i.e. p(|v⟩⟨v|) = Tr(R · |v⟩⟨v|); the spectral
reduction lifts this to p E = Tr(R · E) for every effect.
Standard-basis expansion in EuclideanSpace: v = ∑ᵢ vᵢ • eᵢ.
Tr(R · |v⟩⟨v|) = ⟨v, R v⟩. The trace pairing against a rank-one projector is the
quadratic form of R — the identity turning the sesquilinear reconstruction into the
Born-style trace formula.
S is linear over finite sums in the second slot.
S is conjugate-linear over finite sums in the first slot (via qsesq_conj_symm).
The reconstructed matrix 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 = Matrix.of fun (j k : Fin N) => OP.qsesq (EuclideanSpace.single j 1) (EuclideanSpace.single k 1)
Instances For
R is Hermitian, directly from qsesq_conj_symm.
S is the sesquilinear form of R: S(u,v) = ⟨u, R v⟩. Expand both slots in the
standard basis (qsesq_sum_left, qsesq_sum_right).
q is the quadratic form of R: q v = ⟨v, R v⟩.
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), R.trace = 1 (from OP.total_one), and — the only genuinely new argument —
uniqueness, from the fact that a complex matrix is determined by its quadratic form
(matrix_eq_zero_of_quadForm_zero, a polarisation). Together they package R as a
DensityOperator and prove effect_gleason_representation, the statement the
busch_effect_gleason axiom used to assert.
A complex matrix is determined by its quadratic form. If star x ⬝ᵥ (D *ᵥ x) = 0 for
every x, then D = 0. Over ℂ the diagonal of a sesquilinear form recovers the whole form by
polarisation, so a vanishing quadratic form forces every entry to vanish.
The trace of a product of two Hermitian matrices is real. Tr(A·B)^conj = Tr(B·A) = Tr(A·B).
Step 4a — the reconstructed matrix is positive semidefinite. R.PosSemidef from
qform_nonneg and qform_eq_dotProduct (⟨x, R x⟩ = q x ≥ 0), with R Hermitian.
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. Their difference D is Hermitian with Tr(D · E) = 0 for every
effect; taking E = |v⟩⟨v| (sub-unit) gives ⟨v, D v⟩ = 0 on the whole unit ball, and scaling
- polarisation (
matrix_eq_zero_of_quadForm_zero) forcesD = 0.
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.