mass_parameter_ne_zero
plain-language theorem explainer
The declaration establishes that the mass parameter arising from J-cost symmetry breaking in the Higgs mechanism is strictly positive. Researchers deriving Standard Model masses from recognition cost would cite it to rule out a vanishing vacuum scale. The proof is a one-line wrapper that invokes the inequality lemma on the already-proved positivity statement.
Claim. The mass parameter $m$ generated by the J-cost functional at the vacuum expectation value satisfies $m > 0$, hence $m ≠ 0$.
background
In the Recognition Science account of the Higgs mechanism the J-cost is the functional $J(x) = ½(x + 1/x) - 1$, symmetric under $x ↔ 1/x$ and minimized at $x = 1$. Spontaneous symmetry breaking selects the golden-ratio fixed point, producing a nonzero vacuum expectation value whose associated mass parameter is denoted massParameter. The local setting is the SM-002 derivation that obtains the Mexican-hat potential directly from J-cost convexity and the eight-tick dynamics of phi-forcing.
proof idea
The proof is a one-line wrapper that applies the standard lemma ne_of_gt to the upstream positivity result mass_parameter_pos.
why it matters
The result completes the positivity step inside the SM-002 derivation of spontaneous symmetry breaking from J-cost structure. It guarantees that the recognition scale remains positive, consistent with the phi-ladder mass formula and the T5–T8 forcing chain. No downstream uses are recorded in the current graph, but the declaration directly supports subsequent Yukawa and gauge-boson mass calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.