GUTModel
plain-language theorem explainer
The inductive type enumerates the five canonical grand unified theory models as SU(5), SO(10), E6, flipped SU(5) and trinification. A physicist working on unification scales within Recognition Science cites this enumeration when counting candidates or matching generator numbers to the B3 half-order. The declaration is a direct inductive definition that derives decidable equality and finite cardinality automatically.
Claim. The finite inductive type of canonical GUT models consists of the five constructors SU(5), SO(10), $E_6$, flipped SU(5) and trinification.
background
In the Recognition Science treatment of grand unification the GUT scale is the energy at which the strong, weak and electromagnetic forces merge. The module equates the GUT group rank to the sum of Standard Model ranks (3+2+1=6) or to the rank of SU(5) set equal to configuration dimension D+2 with D fixed at 5. The five listed models are taken to realize this D=5 configuration, with the additional relation that SU(5) has rank D+1=4 and 24 generators equal to half the order of the B3 lattice.
proof idea
The declaration is a direct inductive definition introducing five constructors. The deriving clauses for DecidableEq, Repr, BEq and Fintype are discharged automatically by the Lean typeclass mechanism with no explicit proof terms required.
why it matters
The definition supplies the enumeration required by the GUTCert structure, which asserts cardinality 5, SU(5) generator count 24 and equality with the B3 half-order. It thereby anchors the claim that GUT group dimension aligns with the Recognition Science configuration dimension of 5, supporting the derivation of unification from the single functional equation. The step connects to the T8 landmark fixing spatial dimension while extending the same logic to the GUT scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.