SMGroupCert
plain-language theorem explainer
SMGroupCert packages the certified counts and rank decomposition for the Standard Model gauge structure in the Recognition Science derivation. Physicists tracing the gauge group SU(3)×SU(2)×U(1) back to the phi-ladder would cite this structure to lock in five boson types, rank sum 6, eight gluons, and twelve carriers. The definition is a direct bundling of four equalities taken from sibling constants with no additional steps.
Claim. The structure asserts that the set of Standard Model gauge boson types has cardinality 5, the ranks of SU(3), SU(2) and U(1) sum to 6, the gluon count equals 8, and the total number of gauge carriers equals 12.
background
The module treats the Standard Model gauge group as SU(3)×SU(2)×U(1) and certifies its rank decomposition against Recognition Science. The inductive type SMGaugeBosonType enumerates the five species gluon, W+, W-, Z, photon. Upstream constants fix rankSU3 := 3, rankSU2 := 2, rankU1 := 1 and gluonCount := rankSU3² - 1 = 8; the module doc notes that five types match configDim D = 5 while the rank sum 3+2+1=6 recovers the spatial dimension from the forcing chain.
proof idea
The declaration is a structure definition whose four fields are populated by direct reference to sibling definitions: smGaugeBosonCount supplies the type cardinality, totalRank supplies the rank sum, gluon_count supplies the gluon number, and total_carriers_eq supplies the total carrier count.
why it matters
The structure is instantiated by the downstream definition smGroupCert, which supplies the concrete values. It completes the A1 SM Depth certification step, linking the observed rank decomposition to T8 (D = 3) and the Recognition Composition Law. The construction shows that the Standard Model group structure is fixed once the eight-tick octave and spatial dimension are in place.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.