smSectorCount
plain-language theorem explainer
The theorem establishes that the Standard Model Lagrangian consists of exactly five sectors. Researchers reconstructing the SM from Recognition Science would cite this to confirm the decomposition into gauge kinetic, fermion kinetic, Yukawa, Higgs, and topological components. The proof is a one-line decision procedure that evaluates the cardinality of the finite type from its inductive enumeration.
Claim. The cardinality of the set of Standard Model Lagrangian sectors equals five.
background
Within the Recognition Science approach to the Standard Model, the Lagrangian is structured around five sectors. These correspond to the gauge kinetic terms for the SU(3)×SU(2)×U(1) group, fermion kinetic terms, Yukawa couplings, Higgs potential, and the QCD topological term. The module documentation explains that the four canonical terms plus the topological contribution total five, matching the configuration dimension for spatial dimension three, where the main terms satisfy four equals two to the power of two. This builds on the upstream inductive definition of the four canonical sectors by extending it with the topological term.
proof idea
The proof uses the decide tactic on the equality goal. It relies on the automatically derived Fintype and DecidableEq instances for the inductive enumeration of the five sectors to evaluate the cardinality as five.
why it matters
The result populates the sector count in the Lagrangian certification definition, which also incorporates the relation of four main terms to two squared and the total term count. It anchors the Standard Model structure in the Recognition Science framework by verifying the sector total aligns with the configuration dimension. This connects to the forcing chain where three spatial dimensions imply four primary terms augmented by one topological term.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.