mass_parameter_pos
plain-language theorem explainer
Mass parameter positivity in the RS Higgs mechanism follows from the J-cost being strictly positive away from unity at the vacuum expectation value. Researchers modeling spontaneous symmetry breaking via recognition cost would cite this to establish that particles acquire nonzero mass. The proof is a direct application of the J-cost positivity lemma after unfolding the definition and confirming the vev exceeds one.
Claim. Let $m$ denote the mass parameter, defined as the J-cost of the vacuum expectation value vev. Then $m > 0$.
background
The Recognition Science treatment of the Higgs mechanism (SM-002) starts from the J-cost functional $J(x) = ½(x + x^{-1}) - 1$, which is minimized at the symmetric point $x=1$ with $J(1)=0$. Symmetry breaking occurs when the vacuum selects a value $x=vev>1$, and the mass parameter is identified with $J(vev)$. The upstream result Jcost_pos_of_ne_one states that $J(x)>0$ for $x>0$, $x≠1$, proved by rewriting $J(x)$ as a square over $x$ and applying positivity of squares and division.
proof idea
The proof unfolds the massParameter definition to expose the J-cost at vev. It obtains vev>1 from vev_gt_one and vev≠1 via linarith, then applies the lemma Jcost_pos_of_ne_one (from the Cost module) together with the positivity hypothesis vev_pos.
why it matters
This result feeds directly into mass_parameter_ne_zero, which shows the mass parameter cannot vanish and thereby excludes a zero Higgs scale. It realizes the core claim of the SM-002 derivation that the Higgs mechanism emerges from J-cost symmetry breaking, ensuring positive recognition costs for particle states. In the broader framework it connects to J-uniqueness and the phi fixed point that forces the eight-tick octave and three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.