Machine-checked falsification of quantum foundations: Bell, Tsirelson, no-cloning, and Kochen-Specker in Lean 4

Machine-checked (Lean 4 / Mathlib) certificates for the main falsification results of quantum foundations. Bell's theorem: the CHSH correlation satisfies S <= 2 for local hidden variables, in both the deterministic +/-1 form and the general local-realism form |a|,|b| <= 1. The Tsirelson bound: QM saturates S = 2*sqrt(2), so locality is violated. No-cloning: v -> v tensor v is not linear. Kochen-Specker: no non-contextual 0/1 value assignment in dimension >= 3 (the no_dispersion_free corollary of Gleason). Zero sorry/axiom; #print axioms = propext, Classical.choice, Quot.sound only.