IsospinCert
plain-language theorem explainer
IsospinCert packages three numerical identities that tie the SU(2) isospin group to Recognition Science at D=3. A physicist modeling emergent gauge symmetries would cite it to record that the rank equals D-1, the generator count equals D, and exactly five isospin multiplets exist. The declaration is a bare structure definition that simply asserts the three field equations with no further computation.
Claim. An IsospinCert is a record whose fields assert that the rank of the Lie algebra su(2) equals D-1, the number of su(2) generators equals D, and the set of isospin multiplets (enumerated as singlet, doublet, triplet, quartet, quintet) has cardinality 5.
background
The module Isospin Symmetry from RS treats isospin as the rank-2 subgroup of SU(3) that emerges once spatial dimension is fixed at D=3. IsoSpinMultiplet is the inductive type whose five constructors label the canonical representations I=0 through I=2. The constants su2Rank and su2Generators are defined locally as 2 and 3 respectively; an upstream definition in WeakForceEmergence likewise sets the generator count to 3 and identifies them with the three massive weak bosons.
proof idea
The declaration is a structure definition whose three fields are filled by direct reference to the sibling constants su2Rank, su2Generators and the Fintype instance on IsoSpinMultiplet. No lemmas or tactics are invoked; the body is empty.
why it matters
IsospinCert supplies the data record consumed by the downstream definition isospinCert, which in turn certifies the numerical match between isospin and the RS forcing chain at D=3. It therefore closes the A1 SM Depth section of the module and directly instantiates the T8 landmark that spatial dimension equals three together with the eight-tick octave that produces the observed five multiplets.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.