SMLagrangianCert
plain-language theorem explainer
The SM Lagrangian skeleton certificate bundles the vacuum-zero condition, reciprocal symmetry, and non-negativity for per-sector J-cost together with the matching total-cost properties and the exact count of four sectors. Researchers connecting Recognition Science to the Standard Model would cite the structure when assembling the J-cost skeleton for gauge, fermion, Yukawa, and Higgs sectors ahead of the Wightman-OS bridge. It is introduced as a structure definition that packages these properties for direct use in downstream certificate assembly
Claim. A certificate for the Standard Model Lagrangian skeleton asserts that the J-cost on each sector deviation ratio vanishes at unity, satisfies $J(r)=J(r^{-1})$ and $0≤J(r)$ for all $r>0$, that the summed total cost vanishes when every sector ratio equals one and remains non-negative for positive assignments, and that exactly four sectors exist.
background
The module sets out the Standard Model Lagrangian skeleton on the Recognition Manifold. The full SM Lagrangian decomposes into four canonical sectors (gauge kinetic, fermion kinetic, Yukawa, Higgs potential) each equipped with a unified J-cost-on-deviation form; the total cost is their direct sum with no tree-level cross-sector mixing. The per-sector cost is defined by applying the J-cost function to the sector deviation ratio, while the total cost sums the four contributions.
proof idea
The declaration is a structure definition whose fields directly record the six listed properties. Each property is supplied downstream by dedicated lemmas (sectorCost_zero_at_vacuum, sectorCost_reciprocal_symm, sectorCost_nonneg, totalCost_zero_at_vacuum, totalCost_nonneg) that invoke the definition of sector cost as J-cost, the additivity of total cost, and the upstream non-negativity theorem for J-cost.
why it matters
The structure supplies the named interface for the SM Lagrangian skeleton, feeding the concrete smLagrangianCert construction and the StandardModelLagrangianStructure module. It realizes the four-sector decomposition required by the Recognition Science J-cost formalism and prepares the structural layer for the Wightman-OS bridge. The module notes that full closure of A1 remains a multi-month task.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.