higgsPotential
plain-language theorem explainer
The declaration defines the Recognition Science Higgs potential as the J-cost evaluated at the normalized field ratio r. Particle physicists translating the Standard Model electroweak potential into RS units would cite it to identify the vacuum as the J-cost minimum. It is a direct one-line abbreviation that sets the potential equal to the J-cost function.
Claim. The Recognition Science Higgs potential is defined by $V(r) := J(r)$ where $J(r) = (r + r^{-1})/2 - 1$ for the field ratio $r = |H| / (v / √2)$.
background
The module recasts the Standard Model Higgs potential in Recognition Science terms. The J-cost is the function J(r) = (r + r^{-1})/2 - 1 drawn from the Recognition Composition Law; it vanishes at r = 1 and is symmetric under r ↦ r^{-1}. The upstream Standard Model definition is the quartic -μ²φ² + λφ⁴, while the Yang-Mills vacuum sets all gauge bonds to rung zero.
proof idea
This is a one-line definition that directly applies the J-cost function to the input ratio r.
why it matters
The definition supplies the potential used by the HiggsPotentialCert structure and the non-negativity, symmetry, and unique-minimum theorems in the same module. It realizes the recognition-vacuum interpretation of the Higgs mechanism, where the VEV is the J-cost minimum, consistent with T5 J-uniqueness. It feeds the SMLagrangianSector inductive type for the full Lagrangian skeleton.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.