sectorCost_nonneg
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove strict positivity for r away from the vacuum.
- Does not address cross-sector mixing or interaction terms.
- Does not extend the inequality to non-positive r.
- Does not derive the explicit algebraic form of J-cost.
Lean usage
have h1 := sectorCost_nonneg (h .gaugeKinetic)formal statement (Lean)
51theorem sectorCost_nonneg {r : ℝ} (hr : 0 < r) : 0 ≤ sectorCost r :=
proof body
One-line wrapper that applies Cost.Jcost_nonneg.
52 Cost.Jcost_nonneg hr
53