SMLagrangianCert
plain-language theorem explainer
This structure packages the sector cardinality and term-count relations for the Standard Model Lagrangian within the Recognition Science framework. Researchers embedding the SM into QRFT would reference it to verify the decomposition into five sectors with four principal terms equaling two squared. The definition assembles three equalities already proved by the module's count lemmas without additional reasoning.
Claim. The certificate asserts that the set of Standard Model Lagrangian sectors has cardinality five, that the count of main terms equals four which is two to the power of two, and that the total term count equals the main term count plus one.
background
The module decomposes the SM Lagrangian into gauge kinetic, fermion kinetic, Yukawa, Higgs potential, and theta terms. The inductive type SMLagrangianSector enumerates these five cases. Sibling definitions fix mainTermCount at four and totalTermCount at five, with the four matching two squared as required by spatial dimension three.
proof idea
As a structure definition it directly records the three field equalities. The cardinality field is supplied by the smSectorCount lemma on the Fintype instance. The main term equality invokes the mainTerms_2sq lemma, while the total equality uses the total_terms lemma.
why it matters
It is instantiated by the local smLagrangianCert definition and the corresponding definition in the QRFT skeleton module. The module documentation places it inside the A1 SM Depth analysis, where the term count five equals the configuration dimension and four equals two to the power of D minus one. This anchors the Lagrangian structure to the T8 step of the forcing chain that fixes three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.