totalTermCount
plain-language theorem explainer
The definition assigns the natural number five to the total count of terms in the Standard Model Lagrangian. Researchers deriving the Standard Model from Recognition Science would reference this count to confirm the sector decomposition. The value follows from adding one topological term to four main terms that satisfy a power-of-two relation.
Claim. The total number of terms in the Standard Model Lagrangian is defined to be $5$.
background
The module derives the Standard Model Lagrangian structure from Recognition Science. It decomposes the Lagrangian into four main sectors (gauge kinetic, fermion kinetic, Yukawa couplings, Higgs potential) that equal $2^2$, plus one topological theta term for QCD, for a total of five. This matches the configuration dimension in the framework, with the four-term count proved by decide as $2^(D-1)$ where D denotes spatial dimensions.
proof idea
The declaration is a direct definition that sets totalTermCount to the natural number five with no lemmas or tactics applied.
why it matters
This definition supports the SMLagrangianCert structure, which requires five sectors, mainTermCount equal to four, and totalTermCount equal to mainTermCount plus one. It completes the explicit counting step stated in the module documentation for the Standard Model Lagrangian from RS, connecting to the framework's emphasis on power-of-two relations and dimensional consistency from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.