HiggsFieldCert
plain-language theorem explainer
HiggsFieldCert packages four recognition properties of the Higgs vacuum into a single structure: exactly five sectors from the inductive HiggsFieldSector type, zero J-cost at unit scale, strictly positive J-cost for all other positive scales, and invariance of J-cost under scale inversion. A physicist extracting the electroweak sector from the Recognition Science functional equation would cite this record when confirming that the Higgs potential minimum reproduces the observed five-component structure. The declaration is a plain structure that,
Claim. A certificate asserting that the Higgs field has five sectors, that the J-cost function satisfies $J(1)=0$, that $J(r)>0$ for all $r>0$ with $r≠1$, and that $J(r)=J(r^{-1})$ for all $r>0$.
background
The module identifies the Higgs potential with the J-cost $J(x)=(x+x^{-1})/2-1$ whose global minimum occurs at $x=1$ with value zero. HiggsFieldSector is the inductive type whose five constructors (neutral, chargedPlus, chargedMinus, goldstonePlus, goldstoneMinus) label the components of the Higgs doublet and Goldstone modes. The upstream vacuum definition supplies the zero-bond gauge configuration whose total J-cost vanishes.
proof idea
Structure definition that directly records four field assertions. No lemmas or tactics are invoked inside the declaration itself.
why it matters
The structure is instantiated downstream by higgsFieldCert to supply a concrete witness for the Higgs vacuum in the Recognition Science derivation of the Standard Model Lagrangian. It encodes the five-sector count required by the module's configuration dimension and the J-cost minimum that produces spontaneous symmetry breaking, thereby linking the electroweak sector to the J-uniqueness property of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.