mainTerms_2sq
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the explicit differential operators or field content of any Lagrangian term.
- Does not include the topological theta term in the main-term count.
- Does not establish the equality from the Recognition Composition Law or phi-ladder constructions.
Lean usage
example : mainTermCount = 2 ^ 2 := mainTerms_2sqformal statement (Lean)
36theorem mainTerms_2sq : mainTermCount = 2 ^ 2 := by decide