su5GeneratorCount
plain-language theorem explainer
The definition sets the generator count of SU(5) to 24 via the standard Lie algebra dimension formula. Grand unification researchers cite it when matching this count to the half-order of the B3 structure inside Recognition Science. The value is obtained by direct arithmetic evaluation of 5 squared minus 1.
Claim. The number of generators of the special unitary group SU(5) is defined as $5^2 - 1$.
background
The Grand Unification from RS module treats the GUT scale as the unification point of strong, weak, and electromagnetic forces. It lists five canonical GUT models (SU(5), SO(10), E6, flipped SU(5), trinification) that correspond to configuration dimension 5. The module adopts the alternative SU(5) description whose rank equals D+1, with D the spatial dimension fixed at 3 by the forcing chain T8.
proof idea
This is a direct definition with an empty proof body. It evaluates the arithmetic expression 5 squared minus 1 to obtain the integer 24.
why it matters
The definition supplies the generator count 24 that appears inside the GUTCert structure and the two decide theorems su5Generators_eq_24 and su5_matches_b3half. It fills the explicit step that equates SU(5) generators to |B3|/2, linking the GUT construction to the eight-tick octave and D=3 from the forcing chain. The module records that the equality holds with zero sorry and zero axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.