GaugeLayer
plain-language theorem explainer
GaugeLayer is a record type that packages a name string, fundamental representation dimension, and discrete symmetry order for each gauge layer extracted from the hyperoctahedral group B3 of the 3-cube. Physicists deriving the Standard Model gauge group from geometric symmetries cite it when mapping the three layers of B3 to SU(3), SU(2), and U(1). The declaration is a plain structure definition with three fields that serves as the uniform container instantiated by the three concrete layer definitions downstream.
Claim. A gauge layer is a triple $(name, d, o)$ where $name$ is a string label, $d$ is the dimension of the fundamental representation, and $o$ is the order of the discrete symmetry group.
background
The module derives the Standard Model gauge group SU(3) × SU(2) × U(1) from the automorphism group B3 of the 3-cube Q3, whose vertices are {0,1}^3 and whose group is the hyperoctahedral group of order 48. B3 decomposes as (Z/2Z)^3 ⋊ S3 and admits a natural three-layer splitting: axis permutations (S3), even sign flips ((Z/2Z)^2), and parity (Z/2Z). GaugeLayer supplies the uniform data structure that records, for each layer, its name, the dimension of the representation on which it acts, and the order of the discrete group realizing that layer. Upstream results supply the arithmetic extracted from any logic realization and the primitive distinction theorem that reduces seven axioms to four structural conditions plus three definitional facts.
proof idea
This is a structure definition that introduces the record type GaugeLayer with exactly three fields: name of type String, fund_rep_dim of type Nat, and discrete_order of type Nat. No tactics or lemmas are applied; the declaration is a direct record constructor used as the type of the three concrete layer instances defined later in the same module.
why it matters
GaugeLayer supplies the common interface that lets the three downstream definitions color_layer, weak_layer, and hypercharge_layer assign the concrete values (3,6), (2,4), and (1,2) that match the fundamental dimensions and Weyl-group orders of SU(3), SU(2), and U(1). It completes the gauge-structure derivation begun in ParticleGenerations and QuarkColors by supplying the missing SU(2) and U(1) layers from the same B3 decomposition. In the Recognition framework this step closes the geometric forcing chain from the 3-cube to the observed gauge symmetries.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.