SMLagrangianSector
plain-language theorem explainer
The inductive type enumerates the five sectors of the Standard Model Lagrangian in the Recognition Science derivation: gauge kinetic, fermion kinetic, Yukawa, Higgs potential, and theta term. Researchers reconstructing the SM from the Recognition Composition Law and J-cost would cite this enumeration when counting terms and assigning nonnegative costs. The declaration is a direct inductive construction that derives decidable equality, representation, and finite type structure with no additional proof steps.
Claim. The Standard Model Lagrangian decomposes into five sectors $S = G_K + F_K + Y + H + T$, where $G_K$ denotes gauge kinetic terms, $F_K$ fermion kinetic terms, $Y$ Yukawa couplings, $H$ the Higgs potential, and $T$ the topological theta term. The set $S$ carries decidable equality and has finite cardinality.
background
In the Recognition Science setting the Standard Model Lagrangian is decomposed into canonical sectors whose individual costs are evaluated with the J-cost function. The Higgs potential sector is realized as the J-cost on the field ratio, matching the upstream definition that sets the vacuum potential to zero. The module states that the four main terms (gauge, fermion, Yukawa, Higgs) satisfy the relation $4 = 2^2 = 2^{D-1}$ while the topological theta term brings the total to five sectors, identified with configuration dimension $D$.
proof idea
The declaration is a direct inductive definition that introduces the five constructors and derives the type classes DecidableEq, Repr, BEq, and Fintype in a single line. No tactics or lemmas are applied; the structure is introduced as a primitive enumeration.
why it matters
This enumeration is used by the downstream SMLagrangianCert structure to certify five_sectors cardinality, mainTermCount equal to $2^2$, and totalTermCount equal to five. It bridges the four-sector skeleton to the full five-sector Lagrangian, supporting totalCost nonnegativity and the claim that the SM term count matches the Recognition Science configuration dimension. The construction closes the structural gap between the HiggsPotentialFromRecognitionVacuum result and the full Lagrangian cost theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.