{"id":"palomar/PALOMAR-2026-08-31-000014","url":"https://github.com/stalex444/Busch-theorem/tree/b6801977b666320c38b7027bc130a49583578902","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-31-000014-v1.json","repo":"https://github.com/stalex444/Busch-theorem","tags":["quant-ph","math-ph","msc:81P16","msc:81P15","msc:46N50","quantum-foundations","quantum-measurement","lean-formalization"],"score":0,"title":"stalex444/Busch-theorem","trust":"high","domain":"quant-ph","source":"palomar","authors":["Stephanie Alexander"],"reviews":0,"subject":"quant-ph","summary":"Kernel-checked proof of Busch's theorem in finite dimension: every generalized probability measure on the effects of a complex matrix algebra — nonnegative on effects, additive whenever a sum of effects is again an effect, normalized at the identity — is represented by a unique density matrix via the trace pairing. Existence and uniqueness are both compared (busch_representation). The result is the uniqueness of the Born rule in the POVM reading; it is valid in every finite dimension (beyond finiteness and decidable equality of the index type, the compared statement assumes only [Nonempty…","category":"research","comments":0,"disputed":false,"division":"physics","mentions":0,"verified":true,"discussed":0,"published":"2026-08-31","reactions":{},"formalized":true,"formalizes":[{"title":"Quantum states and generalized observables: a simple proof of Gleason's theorem","identifier":"Physical Review Letters 91, 120403 (2003)","relationship":"formalizes"}]}