SSBMechanism
plain-language theorem explainer
SSBMechanism enumerates the five canonical spontaneous symmetry breaking mechanisms in Recognition Science as electroweak, chiral, magnetic, superconductor, and Bose-Einstein. Researchers modeling J=0 vacuum selection and configDim D=5 cite this enumeration to anchor symmetry breaking. The declaration is a bare inductive type with five constructors that automatically derives DecidableEq, Repr, BEq, and Fintype.
Claim. Let $M$ be the set of spontaneous symmetry breaking mechanisms. Then $M$ consists of the five elements electroweak, chiral, magnetic, superconductor, and Bose-Einstein, equipped with decidable equality and finite cardinality.
background
The Symmetry Breaking from RS module defines spontaneous symmetry breaking as the case where the J=0 attractor (ground state) fails to be invariant under a transformation. It fixes exactly five canonical mechanisms, yielding configuration dimension D=5. The Higgs mechanism appears as the electroweak case, in which the vacuum selects a direction in field space and reduces SU(2)×U(1) to U(1)_EM.
proof idea
This is an inductive definition introducing five constructors. It derives the standard instances DecidableEq, Repr, BEq, and Fintype with no lemmas or tactics required.
why it matters
SSBMechanism supplies the finite set required by the downstream SSBCert structure, which asserts Fintype.card SSBMechanism = 5 together with Jcost 1 = 0 and positive excitation costs for r ≠ 1. It realizes the D=5 landmark stated in the module doc and closes the enumeration needed for certification of J=0 symmetry breaking in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.