gutCert
plain-language theorem explainer
gutCert constructs a concrete certificate for grand unification by populating the GUTCert record with five models, twenty-four SU(5) generators, and their match to the B3 half-order. A physicist examining unification scales in Recognition Science would cite this to confirm the numerical agreement between SU(5) and the RS-derived B3 structure. The definition is a direct record construction that assigns upstream decide-proved equalities to each field.
Claim. The grand unification certificate is the structure satisfying: the number of GUT models equals 5, the number of SU(5) generators equals 24, the B3 half-order equals 24, and the SU(5) generator count equals the B3 half-order.
background
The module treats grand unification as the scale where strong, weak, and electromagnetic forces meet, with GUT group rank given by rank(SU(3)) + rank(SU(2)) + rank(U(1)) = 6 or alternatively by SU(5) with rank D+2. Five canonical models (SU(5), SO(10), E6, flipped SU(5), trinification) correspond to configDim D = 5. SU(5) has rank 4 = D+1 and 5²-1 = 24 generators, which the module equates to |B₃|/2. The GUTCert structure is defined with four fields: five_models requires Fintype.card GUTModel = 5, su5_generators requires su5GeneratorCount = 24, b3_half requires b3HalfOrder = 24, and match_proof requires su5GeneratorCount = b3HalfOrder.
proof idea
The definition constructs the GUTCert record by direct field assignment: gutModelCount supplies the five_models field, su5Generators_eq_24 supplies su5_generators, b3Half_eq_24 supplies b3_half, and su5_matches_b3half supplies match_proof. Each upstream result is itself a decide tactic that discharges the equality.
why it matters
This supplies the concrete witness that closes the numerical verification between SU(5) generators and the B3 half-order inside the Recognition Science grand-unification claim. It directly supports the module statement that five models equal configDim D = 5 and that SU(5) generators equal |B₃|/2. No downstream uses are recorded, and the declaration touches no open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.