isospinCert
plain-language theorem explainer
The isospinCert definition assembles an IsospinCert structure that certifies the numerical match between SU(2) isospin and Recognition Science at three spatial dimensions. A physicist embedding the Standard Model into RS would cite it to record that the rank equals D-1, the adjoint equals D, and exactly five multiplets appear. It is a direct record that substitutes three prior equalities into the structure fields.
Claim. Let IsospinCert be the structure whose fields require that the rank of SU(2) equals 2, the number of generators equals 3, and the cardinality of the set of isospin multiplets equals 5. The term isospinCert is the instance of IsospinCert obtained by substituting the equalities rank of SU(2) equals 2, number of generators equals 3, and cardinality of IsoSpinMultiplet equals 5.
background
In the module on isospin symmetry from RS, isospin is identified with the SU(2) subgroup of SU(3) that appears at D = 3. The structure IsospinCert collects the three matching conditions: rank of SU(2) equals D-1 = 2, number of generators equals D = 3, and exactly five canonical multiplets (I = 0 to 2). These conditions are supplied by the upstream theorems su2Rank_eq_Dm1, su2Generators_eq_D, and isoSpinMultipletCount, each proved by reflexivity or decision.
proof idea
The definition is a one-line wrapper that directly supplies the three fields of IsospinCert using the theorems su2Rank_eq_Dm1 for the rank, su2Generators_eq_D for the generators, and isoSpinMultipletCount for the multiplet cardinality.
why it matters
This definition records the numerical agreement between SU(2) representation theory and the Recognition Science forcing chain at D = 3, where rank equals D-1 and adjoint dimension equals D. It supplies the concrete certificate referenced in the module documentation for the A1 SM depth embedding. No downstream theorems currently depend on it, leaving open its use in larger derivations of particle multiplets.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.