sector_count
plain-language theorem explainer
The theorem establishes that the Standard Model Lagrangian decomposes into exactly four sectors on the recognition manifold. Physicists formalizing unified J-cost formulations of the SM would cite this when verifying the structural skeleton for the Wightman/OS bridge. The proof is a one-line decision procedure that enumerates the four constructors of the inductive sector type.
Claim. The set of canonical sectors of the Standard Model Lagrangian has cardinality four: $|SMLagrangianSector| = 4$.
background
In the Recognition Science framework the Standard Model Lagrangian decomposes into four canonical sectors on the recognition manifold: gauge kinetic, fermion kinetic, Yukawa, and Higgs potential. Each sector receives a J-cost function that vanishes at the recognition vacuum, with mutual additivity at tree level and no cross-sector mixing. The module supplies the structural skeleton that links prior GaugeBosonLagrangian, Yukawa, and HiggsPotential work into one named object ready for the S1 bridge.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the Fintype instance automatically derived from the inductive definition of SMLagrangianSector, which lists exactly four constructors.
why it matters
This result supplies the sector count required by the SMLagrangianCert structure, which bundles vacuum-zero, reciprocal-symmetry, and non-negativity properties for the full skeleton. It fills the structural opening noted in the module documentation for A1 closure and matches the canonical four-sector decomposition used in the Recognition Science program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.