Foundation Gauge From Cube

Gauge ranks from the cube

Gauge structure from the cube is a finite model built from the symmetry of an ordinary three-dimensional cube. Its operations are the signed permutations: permute the cube's three axes, and flip each axis or leave it alone. The full set of signed permutations of a 3-cube has exactly 48 elements, forming what group theory calls the hyperoctahedral group B₃.

The count factors in a disciplined way. The framework establishes that 48 = 6 × 4 × 2, with 6 the permutations of the three axes, 4 the sign flips of even parity, and 2 the quotient that records parity itself. The decomposition 48 = 6 × 4 × 2 is the only one satisfying the stated conditions: no other triple of the same shape multiplies to 48. These are finite arithmetic facts, each one decided by direct computation.

Then come the names. The three factors are labeled with the Standard Model's gauge groups: SU(3) color for the 6, SU(2) weak for the 4, and U(1) hypercharge for the 2, with fundamental representation dimensions 3, 2, and 1. The labeling is a definitional choice, tagged as such: no Lie group, representation, or gauge connection is constructed, and the parity quotient of order 2 carries the name U(1) without being the group itself. What the library does establish is the arithmetic beneath the labels. The assigned dimensions sum to six, the number of faces of the cube.

The value of the model is a sharp question, not a conclusion. The arithmetic matches are exact and forced; the names are a choice; the gap between those two facts is the open problem. Closing it means deriving the continuous gauge groups from the framework's own principles, at which point the labels would become theorems. Until then this page keeps the two apart, and the derivation of the Standard Model gauge group remains an open target.

THEOREM cube_aut_order · IndisputableMonolith/Foundation/GaugeFromCube.lean

THEOREM sm_factorization · IndisputableMonolith/Foundation/GaugeFromCube.lean

THEOREM unique_gauge_factorization · IndisputableMonolith/Foundation/GaugeFromCube.lean

MODEL color_layer · weak_layer · hypercharge_layer · IndisputableMonolith/Foundation/GaugeFromCube.lean

THEOREM dimension_sum · IndisputableMonolith/Foundation/GaugeFromCube.lean

What this page does not claim

No Lie group, representation, gauge connection, or Yang-Mills action is constructed. The order-2 parity quotient is not shown to be the group U(1); it carries the label only. The derivation of the Standard Model gauge group is not claimed; it remains an open target.

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: