mainTerms_2sq
plain-language theorem explainer
The declaration confirms that the main term count in the Standard Model Lagrangian equals four, matching two squared. Researchers deriving the Standard Model from Recognition Science would cite this to anchor the 2^(D-1) sector relation for three dimensions. The proof is a direct decision on the natural-number definition of the count.
Claim. The number of principal terms in the Standard Model Lagrangian equals $2^{2}$.
background
The module decomposes the Standard Model Lagrangian into four main sectors: gauge kinetic terms for the SU(3)×SU(2)×U(1) interactions, fermion kinetic terms across the Weyl fermions, Yukawa couplings that generate masses, and the Higgs potential responsible for spontaneous symmetry breaking. The upstream definition sets mainTermCount to the natural number 4 to encode exactly these sectors. This count sits inside the larger statement that four main terms plus one topological term yield five sectors total, matching the configuration dimension D.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the equality between the constant definition of mainTermCount and the numeral 2 squared.
why it matters
This supplies the main4_2sq field inside the smLagrangianCert definition that certifies the full Lagrangian structure. It directly instantiates the Recognition Science relation 4 = 2^(D-1) for D = 3, connecting to the eight-tick octave and the forcing chain that forces three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.