higgs_symmetric
plain-language theorem explainer
The theorem establishes symmetry of the recognition-derived Higgs potential under inversion of the normalized field ratio about the vacuum. Physicists modeling electroweak symmetry breaking in the Recognition Science framework cite it to confirm reflection invariance of the J-cost minimum. The proof is a direct one-line term application of the Jcost_symm lemma.
Claim. Let $V(r)$ be the Higgs potential given by the J-cost on the normalized field ratio $r = |H|/(v/√2)$. Then $V(r) = V(r^{-1})$ for every $r > 0$.
background
In the Recognition Science setting the Standard Model Higgs potential is reinterpreted as the J-cost on the ratio $r$ of the Higgs field magnitude to its vacuum expectation value. The J-cost is the function $J(x) = ½(x + x^{-1}) - 1$, which vanishes at the fixed point $x = 1$ and supplies the recognition-vacuum interpretation of electroweak symmetry breaking. The module records three structural facts: vacuum zero cost, symmetry under inversion, and second derivative equal to one at the minimum. The upstream lemma Jcost_symm states that Jcost x = Jcost x^{-1} whenever x > 0 and is proved by algebraic expansion and field simplification.
proof idea
The declaration is a term-mode one-line wrapper. It supplies the hypothesis hr : 0 < r directly to the upstream lemma Jcost_symm, which returns the required equality after rewriting the definition of higgsPotential in terms of Jcost.
why it matters
The result supplies the symmetric field of the HiggsPotentialCert record, which is then used by higgsFieldCert to certify the five-sector Higgs structure. It realizes the second key structural fact listed in the module doc-comment and aligns with the J-uniqueness and self-similar fixed-point steps of the forcing chain. No open scaffolding remains for this property.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.