Initial public release of the Lean 4 formalization of Busch's effects formulation of Gleason's theorem.
Main theorem:
Busch.gleason_busch_unconditional
The repository verifies with:
./scripts/verify.sh
The verification script checks a full build, axiom dependencies for the main theorem and key bridge theorems, absence of placeholders, and absence of project-level declaration escape hatches.