sectorCost_reciprocal_symm
plain-language theorem explainer
The declaration proves that sector cost, the J-cost on a sector deviation ratio, is unchanged when the ratio is inverted. Researchers assembling the SM Lagrangian skeleton certificate cite it to confirm per-sector invariance. The proof is a direct one-line application of the general Jcost symmetry lemma.
Claim. For every positive real number $r > 0$, the sector cost satisfies $sectorCost(r) = sectorCost(r^{-1})$.
background
The module builds a structural skeleton for the Standard Model Lagrangian on the recognition manifold by decomposing it into four sectors (gauge kinetic, fermion kinetic, Yukawa, Higgs potential) and assigning each a J-cost on its canonical deviation ratio. sectorCost is defined as the direct application of the J-cost function to this ratio. The setting is the pre-A1 structural layer that prepares named sector structures for the Wightman/OS bridge.
proof idea
The proof is a one-line wrapper that applies the Jcost_symm lemma from the Cost module to the sectorCost definition.
why it matters
It supplies the reciprocal_symm field inside the smLagrangianCert definition, the certificate for the full SM Lagrangian skeleton. The symmetry is required for consistency with the Recognition Composition Law and the J-cost framework's built-in inversion invariance, supporting vacuum-zero conditions and the eventual S1 closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.