J_at_one
plain-language theorem explainer
The theorem establishes that the J-cost functional evaluates to zero at the multiplicative identity. Physicists deriving spontaneous symmetry breaking in the Higgs mechanism from recognition cost would cite this as the vacuum normalization condition. The proof is a term-mode reduction that unfolds the underlying cost definition and simplifies the resulting expression to zero.
Claim. Let $J(x) = ½(x + x^{-1}) - 1$ for $x > 0$ be the J-cost functional. Then $J(1) = 0$.
background
The module derives the Higgs mechanism from J-cost symmetry breaking. The J-cost functional is introduced as $J(x) = ½(x + 1/x) - 1$, with a minimum at the identity. Upstream results from CostAlgebra and BaselineDerivation supply the same normalization statement, phrased as the multiplicative identity having zero cost. The local setting is SM-002, where the vacuum selects a point that breaks the $x ↔ 1/x$ symmetry and generates masses proportional to J-cost.
proof idea
The proof is a one-line wrapper that unfolds Jcost and applies simp to reduce the expression directly to zero.
why it matters
This normalization feeds the canonicalCostAlgebra definition (via normalized := J_at_one) and the cost_algebra_certificate, which lists J(1) = 0 as one of five required properties alongside RCL and reciprocal symmetry. It anchors the zero-cost vacuum in the Higgs module, consistent with the J-uniqueness step in the forcing chain and the minimum of the Mexican-hat potential. The result closes a basic normalization requirement before symmetry breaking selects the golden-ratio fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.