gauge_generation_unification
plain-language theorem explainer
The theorem equates the face-pair count of the three-cube to the fundamental dimension of the color gauge layer, confirms the color count matches that dimension, and decomposes the total face count into the sum of color, weak, and hypercharge layer dimensions. Particle physicists deriving gauge groups from discrete geometry would cite this unification. The proof is a direct term-mode verification that splits the conjunction and discharges the goals by reflexivity and native arithmetic evaluation.
Claim. Let $Q_3$ denote the three-dimensional cube. Then the number of face pairs of $Q_3$ equals the dimension of the fundamental representation of the color gauge layer, the number of colors equals that dimension, and the total number of faces of $Q_3$ equals the sum of the fundamental representation dimensions of the color, weak, and hypercharge gauge layers.
background
The GaugeFromCube module extracts three gauge layers from the automorphism group $B_3 = (ℤ/2ℤ)^3 ⋊ S_3$ of the three-cube $Q_3$. The color_layer is the gauge layer with fundamental representation dimension 3 arising from axis permutations $S_3$. The weak_layer and hypercharge_layer arise from the even-sign-flip subgroup and parity quotient, with dimensions 2 and 1. The sibling definition cube_face_count D returns 2D, hence six faces when D=3. Upstream, ParticleGenerations supplies the face-pair count for three generations while QuarkColors supplies the color count; both are shown equal to the color layer dimension.
proof idea
The term proof begins with constructor to split the three-way conjunction. The first two conjuncts are discharged by rfl, confirming that face_pairs 3 and N_colors 3 both equal color_layer.fund_rep_dim. The remaining arithmetic equality between cube_face_count 3 and the sum of the three layer dimensions is settled by native_decide.
why it matters
This result completes the P-014 certificate by showing that the cube geometry already used for three generations and three colors also forces the gauge dimensions 3+2+1 whose sum recovers the six faces of $Q_3$. It unifies the Standard Model gauge group SU(3)×SU(2)×U(1) with no free parameters, directly after the DimensionForcing and ParticleGenerations steps in the foundation chain. The construction aligns with the Recognition Science forcing of D=3 spatial dimensions from the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.