sectorCost
plain-language theorem explainer
sectorCost supplies the per-sector J-cost on the canonical deviation ratio r for each Standard Model Lagrangian component. Workers assembling the Recognition Science SM skeleton cite it when decomposing gauge, fermion, Yukawa, and Higgs contributions into additive costs. The definition is a one-line wrapper around the Jcost operation imported from the core Cost module.
Claim. For a sector deviation ratio $r > 0$, the per-sector cost is $C(r) := J(r)$, where $J$ denotes the J-cost function on the recognition manifold.
background
The module constructs a structural skeleton for the Standard Model Lagrangian on the Recognition manifold by naming four canonical sectors (gauge kinetic, fermion kinetic, Yukawa, Higgs potential) and assigning each a J-cost form. J-cost is the deviation cost drawn from the upstream Cost abbrev, defined as Quantity CostUnit in the RSNative core. The module doc states that this skeleton exposes the J-cost-zero condition at the recognition vacuum and prepares mutual additivity with no cross-sector mixing at tree level.
proof idea
one-line wrapper that applies the Jcost function from the Cost module.
why it matters
This definition supplies the uniform cost primitive used by the four downstream theorems (sectorCost_zero_at_vacuum, sectorCost_reciprocal_symm, sectorCost_nonneg, sectorCost_pos_off_vacuum) and by the SMLagrangianCert structure and totalCost definition. It directly implements the module's stated goal of tying GaugeBosonLagrangian, Yukawa, and Higgs work into one named skeleton for the eventual Wightman/OS bridge. It instantiates the Recognition framework's J-cost on deviation at the Lagrangian layer, consistent with the RCL and the phi-ladder cost scaling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.