GUTCert
plain-language theorem explainer
GUTCert is a structure that packages four numerical facts certifying the alignment of five grand unified models with the Recognition Science dimension count and the equality of SU(5) generators to the B3 half-order. A physicist modeling unification scales would cite it to record that the model cardinality, generator formula, and lattice order all equal 24 or 5 as required by the RS forcing chain. The structure is assembled directly from the sibling definitions of GUTModel cardinality, the 5^2-1 computation, and the 48/2 reduction.
Claim. A structure whose fields assert that the set of grand unified models has cardinality 5, that the number of generators of SU(5) equals 24, that the half-order of the B3 lattice equals 24, and that these two quantities are identical.
background
The module derives grand unification from the Recognition Science forcing chain by identifying the GUT scale with the point where strong, weak, and electromagnetic forces meet. Five canonical models (SU(5), SO(10), E6, flipped SU(5), trinification) are enumerated by the inductive type GUTModel and are asserted to match configuration dimension D = 5. The same module records that the SU(5) generator count 5^2 - 1 equals the half-order of the B3 lattice.
proof idea
Structure definition that directly references the three upstream constants: the Fintype.card of GUTModel, the definition su5GeneratorCount := 5^2 - 1, and the definition b3HalfOrder := 48 / 2. The final field simply records the equality between the last two constants.
why it matters
GUTCert supplies the bundled certificate consumed by the downstream definition gutCert, which in turn supports the module claim that five models equal configDim D = 5 and that 24 generators equal |B3|/2. It closes the numerical verification step that links the T8 forcing result D = 3 to the rank-5 SU(5) unification alternative.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.