The standard route to the Born rule was carried here as a borrowed assumption for months. It is now proved, and the corpus imports no axioms at all.
effect_gleason_representationThere is a celebrated argument that any consistent way of assigning probabilities to quantum questions must be the standard one. It is powerful and it is hard, so formalisation projects usually assume it and move on. Assuming it is not free: it means the probability rule was put in rather than derived. Here the effect-valued version was assumed at first, then proved outright, so nothing of the sort is borrowed any more.
Two things turn on this. First, honesty of the axiom ledger: with this discharged the corpus depends on no imported result and no postulate beyond the foundations of its proof assistant. Second, independence: the programme's own Born derivation goes through volume ratios and does not use this theorem, so the two routes are genuinely separate confirmations rather than one argument wearing two hats. A published abstract once described this as an external input; that was true when written and false by the time it was read, which is the reason this glossary is guarded.
Every operational package on a finite-dimensional space admits an effect-Gleason representation: the probability assignment on effects is given by a density operator through the trace pairing. This is the Busch effect-valued form, which unlike the original projection-valued Gleason theorem holds in dimension two as well. Proved in-corpus 2026-07-21, foundational-triple only.
CsdLean4/LF2/EffectGleason.leanSource links are pinned to a commit, so they do not drift. The anchors above are checked mechanically against the Lean tree on every build. The mathematics is not, and cannot be: that is a human responsibility and it rests with the author.