sectorCost_pos_off_vacuum
plain-language theorem explainer
The theorem establishes strict positivity of sector cost for every positive real deviation r not equal to one. Researchers constructing the Recognition Science embedding of the Standard Model Lagrangian would cite it to confirm that each sector contribution vanishes exclusively at the recognition vacuum. The proof is a direct one-line wrapper that invokes the known positivity lemma for the J-cost function.
Claim. For every real number $r > 0$ with $r ≠ 1$, the sector cost satisfies $0 <$ sector cost$(r)$.
background
The module defines the Standard Model Lagrangian as a sum of four canonical sectors (gauge kinetic, fermion kinetic, Yukawa, Higgs potential), each equipped with a J-cost-on-deviation form that is zero precisely at the recognition vacuum. J-cost is the derived cost function on positive ratios induced by a multiplicative recognizer; its core positivity property states that Jcost(x) > 0 whenever x > 0 and x ≠ 1. The upstream lemma Jcost_pos_of_ne_one supplies the algebraic reduction Jcost(x) = (x-1)^2 / (x * denominator) and concludes positivity by squaring and division rules. The local setting is the structural skeleton that prepares the Wightman/OS bridge without cross-sector mixing at tree level.
proof idea
The proof is a one-line wrapper that applies the lemma Jcost_pos_of_ne_one directly to the argument r, using the supplied hypotheses 0 < r and r ≠ 1.
why it matters
This declaration completes the per-sector positivity layer of the SM Lagrangian skeleton, ensuring the total cost is nonnegative and zero only at vacuum. It fills the structural opening described in the module doc for tying GaugeBosonLagrangian, Yukawa, and Higgs work into a single named object ready for the S1 bridge. The result rests on the J-cost positivity already proved in the Cost module and supports the Recognition Science claim that the full Lagrangian cost vanishes exclusively at the canonical vacuum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.