sectorCost
plain-language theorem explainer
sectorCost assigns to each Standard Model sector its J-cost evaluated at the sector's canonical deviation ratio r. Researchers assembling the SM Lagrangian skeleton in Recognition Science cite this when building totalCost or verifying vacuum properties in SMLagrangianCert. The definition is realized as a direct one-line alias to the Jcost operation from the RSNative core.
Claim. For a real number $r$ representing a sector's canonical deviation ratio, the per-sector cost is given by $J(r)$, where $J$ is the J-cost function satisfying $J(1)=0$, $J(r)=J(r^{-1})$, and $J(r)≥0$ for $r>0$.
background
The module decomposes the Standard Model Lagrangian into four canonical sectors (gauge kinetic, fermion kinetic, Yukawa, Higgs potential) on the recognition manifold. Each sector receives a cost of the form J-cost on its deviation ratio from the vacuum value 1, with no cross-sector mixing at tree level. The upstream Cost is the Quantity CostUnit abbrev in RSNative.Core that supplies the Jcost function and its algebraic properties.
proof idea
This definition is a one-line wrapper that directly applies the Jcost function from the Cost quantity in the RSNative core.
why it matters
sectorCost supplies the per-sector primitive used to define totalCost (sum of four sector costs) and the SMLagrangianCert structure that encodes vacuum zero, reciprocal symmetry, and nonnegativity. It opens the structural skeleton that links GaugeBosonLagrangian, Yukawa, and Higgs work toward the Wightman/OS bridge. In the framework it instantiates the J-cost-on-deviation form for the four sectors, consistent with the recognition composition law and the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.