unique_gauge_factorization
plain-language theorem explainer
The theorem shows that 48, the order of the hyperoctahedral group B3, admits only the factorization 6 × 4 × 2 when a equals 3!, b equals 2 to the power D-1 with D fixed at 3, and c equals 2. Gauge theorists reconstructing SU(3) × SU(2) × U(1) from cube automorphisms cite it to rule out alternative dimension assignments. The proof reduces to hypothesis substitution, an omega step that fixes the exponent, and a final norm_num check that the product holds.
Claim. Let $a,b,c$ be natural numbers such that $a b c = 48$, $a = 3!$, there exists $k$ with $b = 2^k$ and $k+1=3$, and $c=2$. Then necessarily $a=6$, $b=4$, and $c=2$.
background
Module P-014 derives the full Standard Model gauge group from the automorphism group B3 of the 3-cube Q3. B3 has order 48 and decomposes as (ℤ/2ℤ)^3 ⋊ S3, where the S3 factor (order 6) arises from axis permutations and supplies the SU(3) structure, the even-sign-flip subgroup (order 4) supplies the SU(2) × U(1) structure, and the remaining factor of 2 completes the product. The local setting quotes the three-layer decomposition of B3 and notes that prior modules supplied only the color factor of 3. Upstream results supply parity maps on ledger states and algebraic-tautology checks that keep the counting collision-free.
proof idea
Tactic proof begins by introducing a, b, c and the four hypotheses. It substitutes the given a = 3! and c = 2, obtains the witness k from the existential hypothesis on b, applies omega to conclude k = 2, substitutes to obtain b = 4, then invokes simp followed by norm_num to verify the product identity and discharge the goal.
why it matters
The result supplies the uniqueness half of the gauge-group derivation in P-014, confirming that cube geometry forces exactly the factorization 6 × 4 × 2. It closes the gap between the S3 and even-sign-flip layers already derived and the full order-48 group, consistent with the forced D = 3 in the T0–T8 chain. No downstream theorems are listed, so the declaration functions as a terminal check that alternative gauge representations are excluded by the cube order.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.