IndisputableMonolith.Foundation.GaugeLieCompletionFromCube
Module that packages the compact gauge-factor skeleton selected by the cube-layer completion rule: the three factors SU(3), SU(2), and U(1), with their recognition-axis counts, Lie ranks, and carrier counts. Anyone citing the cube-to-SM gauge bridge or the hypercharge layer uses these totals. The argument is definitional bookkeeping plus the identity that cube-order factors match the completion.
claimThe cube-layer completion selects three compact gauge factors $SU(3)$, $SU(2)$, and $U(1)$. Recognition-axis counts, Lie ranks, and carrier counts are recorded per factor and summed; the cube-order factorization is identified with this completion skeleton.
background
Upstream, GaugeFromCube (P-014) derives the structure $SU(3)\times SU(2)\times U(1)$ from the automorphism group of the 3-cube $Q_3$. That module supplies the geometric origin of the Standard Model gauge group from cube symmetry.
This module sits one layer above that derivation. It does not re-prove the group identification. It names the compact factors selected by the cube-layer completion rule and records the discrete invariants attached to each factor: recognition-axis count, Lie rank, and carrier count, together with their totals.
The local objects are an enumeration of compact gauge factors, per-factor and total tallies for axes, ranks, and carriers, and the statement that the cube-order factorization matches the completion skeleton. Downstream hypercharge work treats this skeleton as given.
proof idea
Definition module with supporting count lemmas, not a deep existence proof. Compact gauge factors are introduced as a finite enumeration of the three SM factors. Recognition-axis counts, Lie ranks, and carrier counts are assigned factorwise and summed. The main structural claim is the identity that cube-order factors match this completion (the named cube-order-factors-as-completion result). No heavy tactic chain: bookkeeping over the factor list plus the completion identification.
why it matters in Recognition Science
Feeds SMHyperchargeFromCube, which continues the punchlist item P0-S2-01 and explicitly treats this module as proving the compact gauge-factor skeleton $SU(3)\times SU(2)\times U(1)$ before attaching hypercharge. Also imported by UnifiedForcingChain, the T0–T8 inevitability chain from the cost foundation, so the cube-selected gauge skeleton is available where the forcing story closes.
In the Recognition framework this is the bookkeeping hinge between cube automorphisms and the SM gauge layer: geometry of $Q_3$ selects the factors; this module freezes the factor list and its discrete ranks so hypercharge and the unified chain can cite a single completion object rather than re-deriving the product group.
scope and limits
- Does not re-derive $SU(3)\times SU(2)\times U(1)$ from cube automorphisms; that lives in GaugeFromCube.
- Does not assign hypercharge quantum numbers or $U(1)_Y$ embeddings.
- Does not prove dynamical gauge coupling running or anomaly cancellation.
- Does not force spacetime dimension or the eight-tick octave; those are separate T-steps.
- Does not claim uniqueness of the completion rule beyond the recorded cube-order identity.
used by (2)
depends on (1)
declarations in this module (14)
-
inductive
CompactGaugeFactor -
theorem
compactGaugeFactor_count -
def
recognitionAxisCount -
def
lieRank -
def
carrierCount -
theorem
recognition_axis_counts -
theorem
recognition_axis_total -
theorem
lie_rank_values -
theorem
lie_rank_total -
theorem
carrier_counts -
theorem
carrier_total -
theorem
cube_order_factors_as_completion -
structure
GaugeLieCompletionCert -
def
gaugeLieCompletionCert