Machine-checked foundations of quantum theory and the Standard Model: Gleason's theorem and the gauge-sector uniqueness, kernel-checked in Lean 4

Machine-checked (Lean 4 / Mathlib) certificates for two foundational results. (1) Gleason's theorem (finite, dim>=3): every non-contextual additive probability on projectors is the Born rule Tr(rho P), proven via the Cooke-Keane-Moran descent-chain route (no continuity needed). (2) The Standard Model gauge-sector uniqueness: the anomaly-cancellation conditions force the hypercharges uniquely up to normalization and the u<->d swap, and the five anomaly coefficients vanish for (1/6, 2/3, -1/3, -1/2, -1). Zero sorry/axiom; #print axioms = propext, Classical.choice, Quot.sound only.