IsoSpinMultiplet
plain-language theorem explainer
IsoSpinMultiplet enumerates the five standard isospin representations used in the Recognition Science treatment of SU(2) symmetry. Physicists mapping the strong interaction to D=3 spatial dimensions would cite this when confirming that the multiplet count equals the configuration dimension. The declaration is an inductive type with five constructors that automatically derives decidable equality and finite-type structure.
Claim. The isospin multiplets are the five representations with quantum numbers $I=0$ (singlet), $I=1/2$ (doublet), $I=1$ (triplet), $I=3/2$ (quartet), and $I=2$ (quintet).
background
In Recognition Science the isospin symmetry is identified with the rank-2 SU(2) subgroup of SU(3). The module records that this rank equals D-1 and the number of generators equals D when D=3, while the five multiplets match the configuration dimension of the model. The inductive definition therefore supplies the concrete finite set whose cardinality is later certified to be exactly 5.
proof idea
The declaration is an inductive definition introducing the five constructors singlet, doublet, triplet, quartet and quintet. The deriving clause immediately generates the required instances of DecidableEq, Repr, BEq and Fintype; no further tactics are needed.
why it matters
The type is consumed by the IsospinCert structure, which records the equalities su2Rank = 3-1, su2Generators = 3 and Fintype.card IsoSpinMultiplet = 5. It thereby supplies the enumeration required to connect the Recognition Science forcing chain (T8: D=3) to the observed isospin multiplets of the strong interaction. The definition closes the finite-set requirement for the A1 SM Depth analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.