sectorCost_nonneg
plain-language theorem explainer
The theorem establishes non-negativity of the per-sector J-cost for any positive deviation ratio r. Researchers building the Standard Model Lagrangian skeleton in Recognition Science cite it when certifying total cost additivity. The proof is a one-line wrapper that invokes the general Jcost_nonneg lemma from the Cost module.
Claim. For any real number $r > 0$, the sector cost satisfies $0 ≤ sectorCost(r)$, where $sectorCost(r)$ is the J-cost applied to the canonical deviation ratio of a given Lagrangian sector.
background
The module decomposes the Standard Model Lagrangian into four canonical sectors (gauge kinetic, fermion kinetic, Yukawa, Higgs potential) and equips each with a unified J-cost on deviation from the recognition vacuum. The definition sectorCost r := Cost.Jcost r directly imports the J-cost function whose non-negativity for positive arguments is already established by AM-GM: J(x) = (x-1)^2/(2x) ≥ 0 when x > 0. Upstream lemmas in Cost, Gravity.CoherenceCollapse, and EnergyProcessingBridge all prove the same inequality by rewriting the expression and applying square non-negativity together with positivity of the denominator.
proof idea
The proof is a one-line wrapper that applies Cost.Jcost_nonneg directly to the hypothesis hr : 0 < r, using the fact that sectorCost is definitionally equal to Jcost.
why it matters
The result supplies the cost_nonneg field inside the smLagrangianCert certificate and is invoked sector-wise inside totalCost_nonneg. It confirms that the J-cost formulation chosen for the SM Lagrangian skeleton remains non-negative, consistent with the foundational non-negativity of J that underpins the entire Recognition framework and the phi-ladder mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.