totalTermCount
plain-language theorem explainer
Recognition Science counts five sectors in the Standard Model Lagrangian as four canonical terms plus one topological term. Researchers deriving the SM from the forcing chain cite this count when certifying the overall structure. The declaration is a direct constant definition with no computation or lemmas applied.
Claim. The total number of Lagrangian sectors in the Standard Model is $5$.
background
The module derives the Standard Model Lagrangian structure from Recognition Science. It identifies four main terms (gauge kinetic for SU(3)×SU(2)×U(1), fermion kinetic for 15 Weyl fermions per generation across three generations, Yukawa couplings, and Higgs potential) that sum to 4 = 2^2, together with one topological θ-term for QCD, for a total of five sectors. This matches the expected count from configDim D via the relation 4 = 2^(D-1). The definition supplies the constant used by sibling declarations to certify the sector count.
proof idea
This declaration is a one-line definition that directly assigns the natural number 5.
why it matters
The definition supplies the total sector count required by the structure SMLagrangianCert, which records five_sectors : Fintype.card SMLagrangianSector = 5 together with the relations main4_2sq and total5. It is invoked by the theorem total_terms that proves totalTermCount = mainTermCount + 1. In the RS framework it completes the A1 SM Depth section by matching the expected count from the eight-tick octave and D = 3 spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.