mainTerms_eq_4
plain-language theorem explainer
The declaration confirms that the principal term count in the Standard Model Lagrangian equals four. A physicist reconstructing the SM from Recognition Science would cite this to fix the decomposition into gauge, Yukawa, Higgs, and fermion sectors. The proof is a direct reflexivity on the definition of the term count.
Claim. The number of principal terms in the Standard Model Lagrangian equals four, matching the decomposition $L = L_1 + L_2 + L_3 + L_4$ where the four sectors are gauge kinetics, fermion kinetics, Yukawa couplings, and the Higgs potential.
background
The module treats the Standard Model Lagrangian as having four canonical sectors: gauge kinetic terms for the SU(3)×SU(2)×U(1) interactions, fermion kinetic terms for the 15 Weyl fermions per generation, Yukawa couplings that generate masses, and the Higgs potential responsible for spontaneous symmetry breaking. This yields the count 4, which equals 2^(D-1) for spatial dimension D=3. The upstream definition mainTermCount : ℕ := 4 encodes this count directly.
proof idea
The proof is a one-line wrapper that applies reflexivity to the definition of mainTermCount, equating it immediately to the numeral 4.
why it matters
This equality fixes the main-term count inside the Recognition Science derivation of the Standard Model Lagrangian. It supports the relation 4 = 2^(D-1) and precedes the addition of the topological term to reach five sectors that match configDim D. The result anchors the four-term structure before any further counting lemmas are applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.