su5Generators_eq_24
plain-language theorem explainer
The equality of the SU(5) generator count to 24 confirms the adjoint dimension for the SU(5) gauge group in grand unification models. Researchers constructing GUT embeddings of the Standard Model cite this when verifying that the generator number matches 24. The proof applies a decision procedure directly to the arithmetic definition of the count as five squared minus one.
Claim. The number of generators of the Lie algebra of SU(5) satisfies $5^2 - 1 = 24$.
background
The module examines grand unification within Recognition Science, where the GUT group rank equals the sum of Standard Model ranks (3+2+1=6) or alternatively D+2=5 for SU(5). Five canonical models are considered, with SU(5) having rank 4 and generator count given by five squared minus one, stated to equal 24 and to match half the order of B3. The upstream definition sets the generator count to this expression, which the theorem evaluates to the integer 24.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the definition of the generator count as 5 squared minus 1, verifying equality to 24.
why it matters
This theorem supplies the su5_generators field in the GUTCert structure, which aggregates the count of five models, the SU(5) generator number, the B3 half order, and their matching proof. It supports the framework claim that SU(5) generators total 24, aligning with the GUT scale unification where group dimensions relate to spatial and internal degrees of freedom in the Recognition Science approach.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.