SSBCert
plain-language theorem explainer
SSBCert is a structure that certifies spontaneous symmetry breaking in Recognition Science by requiring exactly five mechanisms, zero J-cost at the ground state r=1, and strictly positive J-cost for all other positive r. Researchers modeling SSB in RS would cite it to confirm the count matches the five canonical cases. The declaration is a bare structure definition with no proof body or lemmas.
Claim. An SSBCert consists of three fields: the cardinality of the set of SSB mechanisms equals 5, Jcost(1) = 0, and Jcost(r) > 0 for every real r > 0 with r ≠ 1.
background
The module SymmetryBreakingFromRS treats spontaneous symmetry breaking as the J=0 attractor state failing to remain invariant under a transformation. SSBMechanism is the inductive type with exactly the five constructors electroweak, chiral, magnetic, superconductor, and boseEinstein. Jcost is the cost function imported from the Cost module; the structure simply records that this function vanishes at r=1 and is positive elsewhere. The local setting is the A1 SM Depth claim that five mechanisms correspond to configDim D=5.
proof idea
Structure definition with three fields. No tactics, lemmas, or reductions are used; the declaration directly encodes the required properties via the inductive type SSBMechanism and the Jcost predicate.
why it matters
SSBCert supplies the type instantiated by the downstream definition ssbCert, which assembles the concrete witnesses five_mechanisms, ground_state, and excitation_cost. It records the module's central claim that five SSB mechanisms exist with J=0 as ground state, aligning with the Recognition Science treatment of symmetry breaking as part of the forcing chain. No open questions or scaffolding remain in this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.