higgs_mass_positive
plain-language theorem explainer
Any field excursion costs recognition: J(r) > 0 for r ≠ 1. Model builders constructing the Higgs sector in Recognition Science cite this to guarantee a positive mass term away from the vacuum. The proof is a direct one-line wrapper that invokes the core positivity lemma for the J-cost function.
Claim. For every positive real number $r ≠ 1$, the recognition cost satisfies $0 < J(r)$, where $J(r)$ is the J-cost function.
background
J-cost is the recognition cost function whose positivity away from r = 1 is established by rewriting Jcost r as a square over a positive denominator, as shown in the upstream lemma Jcost_pos_of_ne_one: J(x) > 0 for x ≠ 1 and x > 0. The local setting is the Higgs module, where the vacuum sits at the unique J-cost minimum r = 1 and the mass arises from the second derivative J''(1) = 1. This theorem supplies one of the three fields required by the higgsBosonCert structure.
proof idea
One-line wrapper that applies the lemma Jcost_pos_of_ne_one from the Cost module, passing the hypotheses 0 < r and r ≠ 1 directly to obtain 0 < Jcost r.
why it matters
This theorem supplies the mass_positive field inside higgsBosonCert, which bundles the three structural properties of the Higgs boson in the J-cost framework. It closes the positivity requirement for the potential away from the recognition vacuum and aligns with the J-uniqueness property in the forcing chain. The result touches the open question of matching the predicted m_H to the observed 125 GeV scale once the phi-ladder calibration is fixed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.