The complete algebraic structure of the Standard Model of particle physics is derived from a single axiom: a locally finite partial order. No additional mathematical structure is assumed. This trilogy comprises three companion papers: Paper I: "The Physics of Order" derives the Lorentzian metric, quantum linearity, spacetime dimension d=3+1, the gauge group SU (3) ×SU (2) ×U (1), all electric charges, three generations, the Weinberg angle, the gauge coupling, proton stability, the uniqueness of U (1), and the Higgs potential form — all as theorems of a finite partial order. Every algebraic step is formally verified in Lean 4 (25 core files, ~5, 000 lines, zero sorry, zero custom axioms). The continuum limit is constructed from the prime numbers via Weyl equidistribution. Nine further conclusions are derived, including mandatory dark matter, the seesaw neutrino scale, and the absence of a landscape of vacua. Paper II: "Fermion Mass Ratios from the K/P Projection" computes nine zero-parameter predictions: mᵤ/mₜ (1. 22×), mc/mₜ (1. 46×), m_μ/m_τ (0. 94×), mₑ/m_τ (0. 92×), mₜ/mb (0. 85×), the Cabibbo angle |Vᵤs| = 0. 224 via Fritzsch texture (0. 99×), |Vcb| = 0. 072 (1. 7×), the Higgs mass-to-VEV ratio mH/v = 0. 33–0. 42 (0. 65–0. 82×), and the electroweak scale v = 297 GeV via Coleman-Weinberg dimensional transmutation with μ² = 0 (1. 21×). Eight of nine are within a factor of 1. 5× of experiment, spanning seventeen orders of magnitude. Paper III: "Exclusions and Predictions" derives the impossibility of anti-gravity, excludes all extra-dimensional theories, excludes six grand unified theories (with representation-based incompatibility arguments), proves the absence of a string landscape, and predicts a dark matter candidate and the lightest neutrino mass m₁ ~ 0. 005 eV from the seesaw mechanism with MR = MP (proved unique in NeutrinoScale. lean). Lean 4 source: https: //github. com/tomdif/unifiedtheory Full project build: 2, 367+ jobs, zero errors, zero sorry, zero custom axioms. The #print axioms command on every capstone theorem returns only Lean's built-in foundations (propext, Classical. choice, Quot. sound).
Thomas DiFiore (Sun,) studied this question.