sectorCost
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not derive the explicit algebraic form of J from the forcing chain.
- Does not include cross-sector mixing terms at this structural layer.
- Does not compute numerical values or runtimes for specific sectors.
- Does not address loop corrections or renormalization.
Lean usage
sectorCost (r .gaugeKinetic) + sectorCost (r .fermionKinetic)formal statement (Lean)
44def sectorCost (r : ℝ) : ℝ := Cost.Jcost r
proof body
Definition body.
45