Foundation Gauge From Cube Dimension Sum Triangular

The six faces of the cube

A cube has six faces, eight vertices, and twelve edges. These are classical facts of geometry, known since antiquity. The declaration dimension_sum in the Recognition Science library is a machine-checked theorem about a specific way of counting the cube's symmetries, and it lands on the number six: the sum of the three assigned dimensions 3 + 2 + 1 equals the cube's face count, which is 6.

The cube's symmetries are the rigid motions and reflections that map the cube onto itself. There are 48 of them in total. The framework's library, a machine-checked collection of formal theorems, splits these 48 symmetries into three layers. The first layer counts the ways to permute the three axes, which is 6. The second counts the even sign flips, which is 4. The third counts a parity quotient, which is 2. The theorem dimension_sum then verifies that the assigned dimensions 3, 2, and 1 sum to 6, matching the number of faces.

The number 6 is not a coincidence in this counting. The cube has 6 faces, and the symmetry group of the cube has order 48, which factors as 6 × 4 × 2. The framework assigns the labels SU(3), SU(2), and U(1) to these three factors. These are names from particle physics, where they describe the strong, weak, and electromagnetic forces. The assignment is a definitional choice, a model, not a derivation. The library does not construct the continuous Lie groups SU(3), SU(2), or U(1), nor does it build a gauge connection or a Yang-Mills action.

What the declaration dimension_sum actually proves is a finite arithmetic statement: the sum of the three assigned numbers equals the cube's face count. The theorem is checked by the machine, so the arithmetic is certain. But the leap from a cube's symmetry count to the gauge group of the Standard Model is not proved. It is a modeling choice, an identification. The parity quotient of order 2 is not the group U(1). The framework itself marks the derivation of the Standard Model gauge group as an open target, not a finished result.

In plain language, the declaration establishes a clean numerical coincidence: the dimensions 3, 2, and 1 add to 6, the number of faces of a cube. It does not establish that the cube's symmetries are the forces of nature. The arithmetic is solid; the interpretation is a hypothesis. A reader should take the theorem as a neat structural observation, and the gauge labels as a speculative model that the framework itself does not claim to have proven.

/-- The assigned integers satisfy `3 + 2 + 1 = 6`, the closed-form face count
at `D = 3`. No physical decomposition of faces is constructed. -/
theorem dimension_sum :
    color_layer.fund_rep_dim + weak_layer.fund_rep_dim + hypercharge_layer.fund_rep_dim
    = cube_face_count 3 := by
  native_decide

/-- **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

/-- 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 derivation of the Standard Model gauge group from cube symmetries is not a theorem.

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: