mainTerms_2pow_Dm1
plain-language theorem explainer
The declaration establishes that the main term count in the Standard Model Lagrangian equals 2 raised to (D-1) with D equal to 3. Physicists deriving the SM from Recognition Science would cite this to confirm the four principal sectors match the dimensional structure. The proof proceeds by direct evaluation of the natural-number definition via a decision procedure.
Claim. The number of main terms in the Standard Model Lagrangian equals $2^{D-1}$ where $D=3$ is the number of spatial dimensions.
background
The module sets the Standard Model Lagrangian structure inside Recognition Science by identifying four main sectors (gauge kinetic, fermion kinetic, Yukawa, Higgs) plus one topological term, for a total of five sectors matching configDim D. The sibling definition mainTermCount : ℕ := 4 fixes the count of the principal terms. This equality is required to match the framework relation 4 = 2^(D-1) with D=3 drawn from the eight-tick octave forcing chain.
proof idea
The proof is a one-line wrapper that applies the decide tactic after the definition of mainTermCount is unfolded, confirming the numerical equality 4 = 2^(3-1).
why it matters
This result anchors the Standard Model term count to the Recognition Science dimensional forcing (T8: D=3) and supports the module's Lagrangian certification. It feeds the sibling equalities mainTerms_eq_4 and total_terms that close the count to the full five-sector structure. The equality is a direct check that the SM sector count is consistent with the phi-ladder and RCL-derived constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.