sectorCost_zero_at_vacuum
plain-language theorem explainer
The theorem establishes that the per-sector J-cost vanishes exactly when the deviation ratio equals unity, anchoring the zero-energy ground state for each Standard Model sector on the recognition manifold. A physicist constructing the RS-native Lagrangian skeleton would cite this to confirm the vacuum condition before adding gauge, Yukawa or Higgs terms. The proof is a one-line wrapper that directly invokes the unit lemma for the underlying J-cost function.
Claim. $J(1)=0$, where the sector cost is the J-cost function $J(r)=((r-1)^2)/(2r)$ evaluated on the canonical deviation ratio of any SM sector.
background
The module builds 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 on its deviation ratio. The J-cost itself is defined by J(r) = (r-1)^2 / (2r), which is the squared-ratio form equivalent to (r + 1/r)/2 - 1 and vanishes at the recognition vacuum r=1. This declaration supplies the first vacuum property required by the skeleton before mutual additivity and non-negativity are proved for the full set of sectors.
proof idea
The proof is a one-line wrapper that applies the Jcost_unit0 lemma from the Cost module (and its duplicate in JcostCore). That lemma itself follows by direct simplification of the J-cost definition, so the equality sectorCost 1 = 0 reduces immediately to Jcost 1 = 0.
why it matters
The result supplies the vacuum_zero field inside the SMLagrangianCert structure and is invoked to prove totalCost_zero_at_vacuum. It therefore forms the opening structural step that ties the existing GaugeBosonLagrangian, Yukawa and Higgs work into a single named skeleton ready for the Wightman/OS bridge. Within the Recognition framework it confirms the J-cost zero condition at unity that is presupposed by the unified forcing chain and the eight-tick octave construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.