b3Half_eq_24
plain-language theorem explainer
The half B3 order equals 24, confirming the generator count for SU(5) in grand unification models from Recognition Science. Researchers working on force unification at the GUT scale cite this to equate the 24 generators of SU(5) with half the order of the B3 structure. The proof evaluates the arithmetic definition of the half-order using a decision procedure.
Claim. $|B_3|/2 = 24$
background
The module develops grand unification from Recognition Science, where the GUT scale unifies the strong, weak, and electromagnetic forces. The SU(5) group is presented with rank D+1 and generator count 5^2-1=24, set equal to |B3|/2. The upstream definition fixes b3HalfOrder as the natural number 48/2, supplying the concrete value for this identification. This occurs in a setting with five canonical GUT models at configDim D=5 and zero sorries in the Lean development.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the equality after the definition of b3HalfOrder is unfolded, confirming that 48 divided by 2 yields 24.
why it matters
This theorem supplies the b3_half field inside the gutCert definition, which aggregates five-model counts, SU(5) generator equalities, and matching proofs to certify the GUT construction. It directly supports the module claim that SU(5) generators number 24 and match |B3|/2. The result sits within the Recognition Science treatment of GUT groups whose rank relations involve D+1 or D+2, connecting to the overall derivation of physics from a single functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.