HiggsFieldSector
plain-language theorem explainer
HiggsFieldSector enumerates the five sectors of the Higgs field arising from the recognition vacuum minimum: neutral, charged positive, charged negative, Goldstone positive, and Goldstone negative. Physicists reconstructing electroweak symmetry breaking from J-cost minimization cite this enumeration to set the configuration dimension at five. The definition proceeds by direct inductive construction that automatically derives decidable equality, representation, boolean equality, and finiteness instances.
Claim. The Higgs field sector is the finite set with five elements: neutral, positively charged, negatively charged, positive Goldstone, and negative Goldstone.
background
The module derives the Higgs vacuum expectation value from the J-cost minimum of the electroweak recognition vacuum. The potential is given by V(φ_H) = J(φ_H/v) = ½(φ_H/v + v/φ_H) - 1, which reaches its global minimum of zero at φ_H = v. Spontaneous symmetry breaking selects a nonzero vacuum expectation value through boundary conditions.
proof idea
The declaration is a direct inductive definition that introduces five constructors for the neutral, charged, and Goldstone sectors. It derives the type class instances for DecidableEq, Repr, BEq, and Fintype in a single step to enable cardinality and equality reasoning.
why it matters
This definition supplies the five sectors required by the HiggsFieldCert structure, which certifies that the configuration dimension equals five, the vacuum J-cost vanishes, and the off-vacuum positivity and inversion symmetry hold. It anchors the mapping from the recognition vacuum to the standard model Higgs doublet, consistent with the forcing chain that fixes spatial dimensions and the recognition composition law. The construction leaves open the dynamical selection of the specific vacuum scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.