Foundation Gauge From Cube Gauge Generation Unification

The cube's gauge labels

The symmetries of a three-dimensional cube are a classical object. Rotations and reflections that map the cube onto itself form a group of 48 elements. This group, known as the hyperoctahedral group, has a standard decomposition: 48 equals 6 times 4 times 2. The factor 6 counts the permutations of the three axes, the factor 4 counts the even sign flips, and the factor 2 counts the parity quotient. These are finite arithmetic facts, proved by direct computation.

In Recognition Science, the declaration gauge_generation_unification packages these three factors with labels borrowed from particle physics. The framework's library assigns the name "SU(3) color" to the factor 6, "SU(2) weak" to the factor 4, and "U(1) hypercharge" to the factor 2. It also records the tuple (3, 2, 1) as the dimensions of these layers. The proved result unique_gauge_factorization shows that any factorization of 48 into three natural numbers a, b, c, with a equal to 6, b a power of 2 with k+1=3, and c equal to 2, forces a=6, b=4, c=2. This is a uniqueness statement about the arithmetic of the cube's symmetry group.

The library is explicit about what this does not do. The declaration does not construct the Lie groups SU(3), SU(2), or U(1), does not build a representation of them, and does not define a gauge connection or a Yang-Mills action. The parity quotient of order 2 is not the group U(1). Matching the finite factors to Standard Model labels is an identification, a definitional choice, not a result that the Standard Model gauge group is forced. The registry item P-014 remains OPEN as a derivation of the Standard Model gauge group. The framework proves the arithmetic of the cube; it does not prove that the cube is the gauge group.

/-- **THEOREM**: |Aut(Q₃)| = |B₃| = 48.
    The automorphism group of the 3-cube has order 48. -/
theorem cube_aut_order : Fintype.card (SignedPerm 3) = 48 := by
  rw [signed_perm_card]
  norm_num

theorem axis_perm_count_D3 : axis_perm_count 3 = 6 := by native_decide

/-- For D = 3: the even sign-flip subgroup has order 4. -/
theorem even_sign_flip_count_D3 : even_sign_flip_count 3 = 4 := by
  native_decide

/-- **Layer 3**: The parity quotient ℤ/2ℤ.
    The quotient of the sign-flip group by the even subgroup.
    Order: 2. This finite group is not `U(1)`; the later hypercharge label is
    MODEL. -/
def parity_quotient_order : ℕ := 2

/-- The three MODEL-labeled records. The names and dimensions are definitions,
not consequences of the finite groups. -/
def color_layer : GaugeLayer :=
  { name := "SU(3) color"
    fund_rep_dim := 3
    discrete_order := 6 }

def weak_layer : GaugeLayer :=
  { name := "SU(2) weak"
    fund_rep_dim := 2
    discrete_order := 4 }

def hypercharge_layer : GaugeLayer :=
  { name := "U(1) hypercharge"
    fund_rep_dim := 1
    discrete_order := 2 }

What this page does not claim

The declaration does not construct the Lie groups SU(3), SU(2), or U(1). The parity quotient of order 2 is not the group U(1). The framework does not prove that the Standard Model gauge group is forced by the cube's symmetries.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/GaugeFromCube.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: