ssbMechanismCount
plain-language theorem explainer
The theorem states that the Recognition Science framework enumerates exactly five spontaneous symmetry breaking mechanisms. A physicist mapping RS ground states to electroweak or condensed-matter phenomena would cite this count when fixing configDim D = 5. The proof is a one-line wrapper that invokes the decide tactic on the Fintype instance derived from the inductive enumeration.
Claim. The finite set of spontaneous symmetry breaking mechanisms has cardinality five: $5$.
background
In the Symmetry Breaking from RS module, spontaneous symmetry breaking is the J = 0 attractor state that is not invariant under a transformation. SSBMechanism is the inductive type whose five constructors are electroweak, chiral, magnetic, superconductor and boseEinstein; this enumeration is declared to equal configDim D = 5. The module imports the vacuum definition from YangMillsMassGap, where vacuum is the gauge-bond configuration with every bond at rung 0 and therefore carries zero J-cost.
proof idea
The proof is a one-line wrapper that applies the decide tactic. Decide computes the cardinality directly from the Fintype instance that the inductive type SSBMechanism derives automatically from its five constructors.
why it matters
The result supplies the five_mechanisms field of the downstream ssbCert definition, which certifies the full symmetry-breaking structure. It realizes the module's A1 SM Depth claim that five canonical mechanisms correspond to configDim D = 5 and thereby anchors the J = 0 ground state inside the Recognition Science forcing chain. The declaration touches the open mapping from these mechanisms onto the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.