Foundation Gauge From Cube Three Layer Factorization

The cube's arithmetic

The symmetries of a three-dimensional cube form a finite group: every rotation, reflection, and combination of the two that leaves the cube looking the same. There are exactly 48 such symmetries. This count is a classical fact, and the framework's machine-checked library of formal theorems proves it directly: the automorphism group of the cube has order 48.

The framework then decomposes this group into three layers. First, the 6 ways to permute the three axes (swap x and y, rotate the axes, and so on). Second, the 4 ways to flip the signs of coordinates while preserving the permutation even. Third, the 2-way parity quotient that distinguishes even from odd sign flips. The theorem three_layer_decomposition states the arithmetic consequence: 48 = 6 × 4 × 2. A companion theorem, unique_gauge_factorization, proves that under the stated conditions this is the only way to factor 48 into such a product.

In Recognition Science, this finite arithmetic is a ledger, a discrete record of events, and the framework models the three factors with the Standard Model's gauge groups. The 6 is labeled SU(3) color, the 4 is labeled SU(2) weak, and the 2 is labeled U(1) hypercharge. The framework's library proves that the assigned dimensions satisfy 3 + 2 + 1 = 6, matching the number of faces of the cube. This is a definitional choice, a MODEL, not a derivation.

The declaration does not construct any Lie group, representation, gauge connection, or field theory. The parity quotient of order 2 is not U(1) as a continuous group. Matching the finite factors to Standard Model labels is an identification, not a theorem that the Standard Model gauge group is forced. The registry item P-014 remains OPEN as a derivation of the Standard Model gauge group.

What the declaration establishes is a precise, machine-checked correspondence between the cube's symmetry arithmetic and the rank structure of the Standard Model's gauge groups. It shows that the numbers 6, 4, and 2, and their sum 6, appear naturally in the cube's geometry. Whether this correspondence is physically meaningful is a separate question the framework does not settle here.

/-- **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 factorization in terms of the Standard Model structure. -/
theorem sm_factorization :
    (48 : ℕ) = 6 * 4 * 2 := by norm_num

/-- **THEOREM (Unique Factorization under fixed hypotheses)**:
    The ONLY way to decompose 48 = |B₃| as an ordered product a × b × c
    where `a = 3!`, `b = 2^k` with `k+1=3`, and `c=2` is `6 × 4 × 2`.
    The hypotheses already prescribe the factor shapes; no gauge group follows. -/
theorem unique_gauge_factorization :
    ∀ a b c : ℕ,
      a * b * c = 48 →
      a = Nat.factorial 3 →
      (∃ k, b = 2 ^ k ∧ k + 1 = 3) →
      c = 2 →
      a = 6 ∧ b = 4 ∧ c = 2 := by
  intro a b c habc ha hb hc
  subst ha; subst hc
  obtain ⟨k, hbk, hk3⟩ := hb
  have hk : k = 2 := by omega
  subst hk
  simp at hbk
  subst hbk
  norm_num at habc ⊢

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

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

What this page does not claim

The declaration does not construct any Lie group, representation, gauge connection, or field theory. The parity quotient of order 2 is not U(1) as a continuous group. Matching the finite factors to Standard Model labels is an identification, not a theorem that the Standard Model gauge group is forced.

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: