gutModelCount
plain-language theorem explainer
The theorem establishes that the finite type of grand unification models contains exactly five elements. A physicist matching RS unification to standard GUT groups would cite this count when fixing the configuration dimension at five. The proof is a one-line decision procedure that exhausts the enumerated inductive type.
Claim. The set of canonical grand unification models has cardinality five: $ |GUTModel| = 5 $, where the models are SU(5), SO(10), E6, flipped SU(5), and trinification.
background
The module treats grand unification as the scale where strong, weak, and electromagnetic forces meet, with GUT group rank equal to 6 in the RS decomposition or 5 for SU(5). The inductive type GUTModel lists the five canonical models that realize configuration dimension D = 5, and the module notes that SU(5) generators equal 24, half the order of the B3 group. The upstream definition supplies the finite list with DecidableEq, Repr, BEq, and Fintype instances.
proof idea
The proof is a one-line wrapper that applies the decide tactic to compute Fintype.card on the inductive type GUTModel.
why it matters
This cardinality populates the five_models field inside the gutCert certificate, which also records the SU(5) generator count and the matching proof to B3 half-order. It directly supports the module claim that five models equal configDim D = 5 and links to the RS GUT scale where rank sums to 6 or SU(5) rank equals D+1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.