Constraint-First Unification, machine-checked: the exact content of a theory of everything is constraints, labels, and parameters

Machine-checked (Lean 4 / Mathlib) forced/free split across all four sectors of physics. The Born rule is the unique non-contextual probability rule (Gleason); the SM hypercharges are forced by anomaly cancellation (N_gen free); the flux tadpole is the unique duality invariant (Mitchell/FFT); the Einstein equation is the unique divergence-free theory (Lovelock). The measurement problem and 'why these 19' are provably the free column. Falsifiable: a hidden symmetry fixing the 19, a second divergence-free gravity theory, or a non-contextual deterministic completion of QM would each kill it. Zero sorry/axiom.