smGroupCert
plain-language theorem explainer
smGroupCert assembles a record certifying that the Standard Model gauge bosons consist of five types with ranks summing to six and eight gluons among twelve carriers. Researchers deriving the gauge group from Recognition Science forcing chains would reference this to verify the (3,2,1) decomposition matches SU(3)×SU(2)×U(1). The definition populates the SMGroupCert structure directly from sibling theorems on boson counts and rank sums.
Claim. The certificate asserts that the number of SM gauge boson types is 5, the ranks of SU(3), SU(2), and U(1) sum to 6, the gluon count equals 8, and the total number of carriers equals 12.
background
SMGroupCert is a structure requiring four equalities: the cardinality of SM gauge boson types is five, the sum of ranks for SU(3), SU(2), and U(1) is six, the gluon count is eight, and the total number of carriers is twelve. The module derives the Standard Model gauge group SU(3)×SU(2)×U(1) from Recognition Science via the GaugeGroupCube, with SU(3) rank equal to spatial dimension D=3, SU(2) rank D-1=2, and U(1) rank 1. Upstream results include the theorem proving 8 = 3² - 1 for the SU(3) gluon count and the theorem proving the rank sum equals 6.
proof idea
The definition constructs an instance of the SMGroupCert structure by assigning each field to the corresponding sibling result: the five_types field to the theorem establishing five boson types, the rank_decomp field to the theorem on the rank sum, the gluon_8 field to the theorem on eight gluons, and the total_12 field to the theorem on twelve carriers. All assignments rely on prior decide tactics establishing the numerical equalities.
why it matters
This definition certifies the group-rank match for the Standard Model within the Recognition Science framework, linking to the eight-tick octave and D=3 spatial dimensions through the rank decomposition. It fills the A1 SM Depth proposition by confirming five gauge boson types and the (3,2,1) ranks. No open questions are directly addressed, as it closes the certification with zero sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.