gaugeLieCompletionCert
plain-language theorem explainer
A single certificate packages the cube-to-gauge dictionary: three compact factors SU(3)×SU(2)×U(1), recognition-axis counts (3,2,1), Lie ranks (2,1,1), and carrier counts (8,3,1), plus the B₃ order factorization. Anyone citing the first clean bridge from the D=3 cube skeleton to the SM compact-factor skeleton will point here. The body is a pure structure assembly of already-proved numeric and factorization lemmas.
Claim. There exists a gauge-Lie-completion certificate asserting: exactly three compact gauge factors; recognition-axis counts $3$, $2$, $1$ for $\mathrm{SU}(3)$, $\mathrm{SU}(2)$, $\mathrm{U}(1)$ respectively, summing to the $3$-cube face count $6$; Lie ranks $2$, $1$, $1$ summing to $4$; carrier counts $8$, $3$, $1$ summing to $12$; and the signed-permutation order of $B_3$ factors as (axis permutations)$\times$(even sign flips)$\times$(parity quotient).
background
The module records the compact-completion rule that sends the forced $B_3$ layer counts (axis permutations $3$, even sign-flip completion $2$, parity quotient $1$) to the Standard Model compact factors $\mathrm{SU}(3)$, $\mathrm{SU}(2)$, $\mathrm{U}(1)$. It deliberately keeps two notions apart: recognition-axis count $(3,2,1)$ totaling $6$, versus Lie rank $(2,1,1)$ totaling $4$.
CompactGaugeFactor is the three-element type of those factors. recognitionAxisCount, lieRank, and carrierCount assign the numeric data per factor. Upstream, cube_order_factors_as_completion reuses the three-layer factorization already proved in GaugeFromCube: $|\mathrm{SignedPerm},3| = $ axis-perm count $\times$ even-sign-flip count $\times$ parity-quotient order. Carrier and rank totals are closed by decide.
This is the first bridge from the cube layer skeleton to the compact gauge-factor skeleton, not yet hypercharge assignments or fermion representations.
proof idea
Pure structure construction: each field of GaugeLieCompletionCert is filled by a named sibling theorem. Factor cardinality comes from compactGaugeFactor_count; axis counts and their sum from recognition_axis_counts and recognition_axis_total; Lie ranks and sum from lie_rank_values and lie_rank_total; carriers and sum from carrier_counts and carrier_total; the $B_3$ factorization from cube_order_factors_as_completion (itself a one-line appeal to three_layer_factorization). No new reasoning; the certificate is the packaging.
why it matters
Feeds the T8 gauge bridge: t8_to_gauge_standard_model_bridge_holds routes gauge and Standard Model surfaces through the canonical $D=3$ cube/spinor skeleton, and this certificate is the compact-factor half of that route. In the forcing chain, T8 forces three spatial dimensions; the cube work then forces the $B_3$ layer counts; this object records the dictionary that turns those counts into $\mathrm{SU}(3)\times\mathrm{SU}(2)\times\mathrm{U}(1)$ with the correct rank and carrier arithmetic.
It closes punchlist item P0-S2-01 as a clean, sorry-free bridge theorem. Open downstream work remains: full hypercharge embedding and fermion-representation derivation are explicitly out of scope here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.