mainTermCount
The declaration defines the number of principal terms in the Standard Model Lagrangian as four. Physicists reconstructing the SM from Recognition Science forcing chains cite this count to anchor the 2^(D-1) relation for D=3. It is introduced by direct numerical assignment, which then feeds reflexivity and decision-tactic proofs in the surrounding statements.
claimThe number of principal terms in the Standard Model Lagrangian is defined to be $4$.
background
The module decomposes the Standard Model Lagrangian into four sectors: gauge kinetic terms for SU(3)×SU(2)×U(1), fermion kinetic terms for the Weyl fermions, Yukawa couplings, and the Higgs potential. Module documentation states these four terms equal 2^2, with one additional topological θ-term bringing the total to five sectors matching configuration dimension D. This decomposition supplies the base count used by downstream equalities relating the term number to powers of two.
proof idea
The declaration is a direct definition that assigns the constant 4 to mainTermCount. No lemmas or tactics are invoked inside the definition itself; it functions as the base value for one-line reflexivity and decide proofs in the dependent statements.
why it matters in Recognition Science
This definition supplies the numerical anchor for the Standard Model Lagrangian certification. It is used directly by mainTerms_eq_4 (via rfl), mainTerms_2sq (2^2), mainTerms_2pow_Dm1 (2^(3-1)), total_terms (mainTermCount + 1), and the SMLagrangianCert structure. It realizes the T8 forcing step that sets D=3 spatial dimensions through the eight-tick octave, closing the link between the observed gauge structure and the Recognition Science dimensional count without extra hypotheses.
scope and limits
- Does not derive the explicit differential form of any individual Lagrangian term.
- Does not obtain the value 4 from the J-cost functional or Recognition Composition Law.
- Does not incorporate the topological θ-term into the principal count.
- Does not address coupling constants, renormalization, or quantum corrections.
Lean usage
theorem mainTerms_eq_4 : mainTermCount = 4 := rflformal statement (Lean)
32def mainTermCount : ℕ := 4