Foundation Gauge Lie Completion From Cube Carrier Total

The carrier count

The Standard Model of particle physics describes three of the four known forces through a mathematical structure called a gauge theory. Each force in this theory is carried by specific particles: eight gluons carry the strong force, three W and Z bosons carry the weak force, and one photon carries the electromagnetic force. Together, these twelve particles are the gauge bosons, the messengers of the fundamental interactions. In the Recognition Science framework, a machine-checked library of formal theorems proves that this count of twelve emerges from a cube's geometry rather than being inserted by hand.

The framework's starting point is a ledger, a discrete record of recognition events, where each event carries a cost. From the structure of this ledger, the framework derives a three-dimensional space with a specific symmetry group. This group, called the signed permutation group on three elements, has a known factorization into three layers: the six ways to permute the three axes, the two ways to flip signs consistently, and the one parity quotient. The machine-checked theorem carrier_total establishes that these three layers correspond exactly to the three gauge factors of the Standard Model: the count 3 maps to SU(3) for color, 2 maps to SU(2) for weak isospin, and 1 maps to U(1) for hypercharge.

Each gauge factor carries a specific number of gauge bosons, determined by its mathematical dimension. For SU(3), the count is 3 squared minus 1, which equals 8. For SU(2), it is 2 squared minus 1, which equals 3. For U(1), the count is simply 1. The theorem carrier_total proves that these three numbers sum to 12, matching the known count of gauge bosons in the Standard Model. This is not a numerical coincidence within the framework; it is a proved consequence of the cube's symmetry structure.

The framework is careful to distinguish what this theorem establishes from what it does not. The carrier count of 12 is a proved result about the symmetry group of a cube. However, this is not yet a derivation of the full hypercharge assignments or the fermion representation content of the Standard Model. The theorem connects the cube's symmetry layers to the gauge factor skeleton, but it does not derive the specific charges or particle content that fill out the complete theory. The framework explicitly labels this as the first clean bridge theorem, not the full derivation.

What this means for a reader is that the framework provides a structural explanation for why the Standard Model has twelve gauge bosons, grounded in the geometry of three-dimensional space. The count is not assumed; it is forced by the cube's symmetry. This is a concrete step in a larger program, but it is a step with clear boundaries. The framework does not claim to have derived the entire Standard Model from its principles, only this particular count of force carriers.

/-- Total gauge carriers before electroweak mixing: `8 + 3 + 1 = 12`. -/
theorem carrier_total :
    carrierCount .su3 + carrierCount .su2 + carrierCount .u1 = 12 := by
  decide

/-- The cube completion has recognition-axis counts `(3,2,1)`. -/
theorem recognition_axis_counts :
    recognitionAxisCount .su3 = 3 ∧
    recognitionAxisCount .su2 = 2 ∧
    recognitionAxisCount .u1 = 1 := by
  decide

/-- Carrier counts are `8`, `3`, and `1`. -/
theorem carrier_counts :
    carrierCount .su3 = 8 ∧ carrierCount .su2 = 3 ∧ carrierCount .u1 = 1 := by
  decide

/-- Total Lie rank of `SU(3) x SU(2) x U(1)` is `4`. -/
theorem lie_rank_total :
    lieRank .su3 + lieRank .su2 + lieRank .u1 = 4 := by
  decide

What this page does not claim

This theorem does not derive the full hypercharge or fermion-representation content of the Standard Model. The carrier count of 12 does not by itself fix the values of the electroweak mixing angle or other free parameters. The cube symmetry group is not claimed to be the complete gauge group of the Standard Model before electroweak symmetry breaking.

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/GaugeLieCompletionFromCube.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: