smLagrangianCert
plain-language theorem explainer
The smLagrangianCert definition constructs a certificate asserting that the Standard Model Lagrangian skeleton obeys vacuum-zero J-cost, reciprocal symmetry under scaling, and non-negativity across its four sectors, with the total cost inheriting the same properties. Researchers assembling the Recognition Science bridge to the Standard Model would cite this when instantiating the structural skeleton for the Wightman/OS transition. The construction is a direct record instantiation that substitutes the pre-proved sector theorems into the SMLagrag
Claim. Let SMLagrangianCert be the structure requiring that the sector cost function satisfies sectorCost(1) = 0, sectorCost(r) = sectorCost(r^{-1}) for r > 0, sectorCost(r) ≥ 0 for r > 0, the total cost vanishes when every sector argument equals 1, the total cost is non-negative whenever all sector arguments are positive, and exactly four sectors exist. The definition smLagrangianCert is the instance of this structure obtained by direct substitution of the corresponding sector theorems.
background
In Recognition Science the J-cost quantifies deviation from the recognition vacuum at unity, with the canonical identity event achieving the global minimum. The module decomposes the Standard Model Lagrangian into four canonical sectors (gauge kinetic, fermion kinetic, Yukawa, Higgs potential) and equips each with a J-cost-on-deviation form; the SMLagrangianCert structure packages the required structural properties for this skeleton. Upstream, cost_nonneg from ObserverForcing states that the cost of any recognition event is non-negative via Jcost_nonneg, while the sibling sectorCost theorems apply the same Jcost_nonneg and Jcost_symm identities to the sector cost function.
proof idea
The definition constructs the SMLagrangianCert record by direct field assignment: vacuum_zero receives sectorCost_zero_at_vacuum, reciprocal_symm receives sectorCost_reciprocal_symm, cost_nonneg receives sectorCost_nonneg, total_vacuum_zero receives totalCost_zero_at_vacuum, total_nonneg receives totalCost_nonneg, and sector_count receives sector_count. No further tactics or reductions are applied.
why it matters
This supplies the concrete certificate required by the downstream smLagrangianCert in StandardModelLagrangianStructure, which extends the skeleton with five-sector and main-term properties. It completes the structural opening that ties GaugeBosonLagrangian, Yukawa, and HiggsPotential work into one named object with the correct shape for the S1 Wightman/OS bridge; the module records that full A1 closure remains multi-month work while this layer carries zero sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.