smLagrangianCert
plain-language theorem explainer
The definition constructs a certificate asserting that the Standard Model Lagrangian decomposes into exactly five sectors with four main terms and one additional topological term. Researchers deriving the Standard Model from Recognition Science would cite it to fix the sector count before imposing cost functions or vacuum properties. The construction is a direct record assembly that populates each field from a pre-established counting theorem obtained by exhaustive decision on finite types.
Claim. The certificate asserts that the set of Standard Model Lagrangian sectors has cardinality 5, the count of main terms equals $2^2$, and the total term count equals the main term count plus 1.
background
The module decomposes the Standard Model Lagrangian into gauge kinetic, fermion kinetic, Yukawa, Higgs, and topological sectors, yielding five sectors total. Four of these are the primary dynamical terms whose count satisfies $2^{D-1}$ for spatial dimension $D=3$, while the fifth is the QCD topological term. The certificate structure encodes precisely these three numerical relations so that downstream cost analysis can be attached without re-proving the enumeration.
proof idea
The definition builds the certificate record by direct field assignment. The sector cardinality field receives the theorem that establishes five sectors by exhaustive checking of the finite type. The main-term field receives the theorem proving the count equals four. The total-term field receives the theorem proving the sum is main plus one. Each supporting result is obtained by the decide tactic on finite enumerations.
why it matters
This certificate is imported by the QRFT skeleton certificate, which then layers vacuum-zero and non-negativity properties onto the same structure. It supplies the counting step that aligns the Lagrangian with the eight-tick octave and the forcing-chain derivation of three spatial dimensions. The placement closes the structural enumeration before the Recognition Composition Law or phi-ladder mass formulas are applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.