isoSpinMultipletCount
plain-language theorem explainer
The result states that the isospin multiplet type, defined by five constructors from singlet through quintet, has cardinality five. Researchers verifying the dimension of the isospin representation space in Recognition Science models would reference this computation. The proof proceeds by a single decision tactic that exhaustively checks the finite enumeration.
Claim. The cardinality of the set of isospin multiplets is $5$.
background
In the module on isospin symmetry derived from Recognition Science, isospin corresponds to the SU(2) subgroup of rank 2 at spatial dimension D=3. The inductive type IsoSpinMultiplet enumerates the five canonical multiplets: singlet (I=0), doublet (I=1/2), triplet (I=1), quartet (I=3/2), and quintet (I=2). This matches the configuration dimension equal to D=5 in the framework. The upstream definition provides the finite type structure with decidable equality and Fintype instance.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the equality Fintype.card IsoSpinMultiplet = 5, which succeeds because the type is a finite enumeration of five elements.
why it matters
This theorem supplies the five_multiplets field in the isospinCert definition, which certifies the SU(2) rank and generator count matching D-1 and D. It aligns with the framework's D=3 spatial dimensions, where the five multiplets reflect the configDim. No open questions are directly addressed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.