six_better_separation_than_three
plain-language theorem explainer
With the unique even quartic Z(Q̃)=Q̃²+Q̃⁴, the face-count scale k=6 yields strictly larger band labels than k=3 on every Standard Model charge family (lepton, up-type, down-type). Anyone comparing candidate integerization scales for the Z-map cites this. The proof is a one-line unfold of the polynomial followed by integer arithmetic via omega.
Claim. For the even quartic $Z(\tilde{Q})=\tilde{Q}^2+\tilde{Q}^4$, one has $Z(-6)>Z(-3)$, $Z(4)>Z(2)$, and $Z(-2)>Z(-1)$. Equivalently, the face-count integerization $k=6$ produces strictly larger $Z$-values than $k=3$ on each of the three SM charge families.
background
This module derives the charge-to-band map $Z(\tilde{Q})$ from recognition boundaries on the 3-cube, without mass anchors. Stage 1 fixes the integerization scale: a boundary of charge $Q$ couples to the $F=2D$ faces of the cube, and the ledger demands integer entries, so $\tilde{Q}=kQ$ must lie in $\mathbb{Z}$ for all SM charges $Q\in{-1,2/3,-1/3}$. At $D=3$ one has $F=6$, and $k=6$ is the minimal positive even integerizer.
Stage 2 forces the polynomial shape. Gauge invariance requires $Z$ even in $\tilde{Q}$, non-negative, and vanishing at zero; the minimal such form is $Z=a\tilde{Q}^2+b\tilde{Q}^4$. Family separation then pins $a=b=1$. The local definition is $Z_{\mathrm{poly}}(a,b,Q)=aQ^2+bQ^4$, so the unique map is $Z_{\mathrm{poly}}(1,1,-)$.
The three comparisons here evaluate that map at the $k=6$ versus $k=3$ integerized charges: lepton $\tilde{Q}\in{-6,-3}$, up-type ${4,2}$, down-type ${-2,-1}$.
proof idea
Term-mode proof in two steps. First simp only [Z_poly] unfolds each side to the explicit integer $aQ^2+bQ^4$ with $a=b=1$. Then omega discharges the three strict inequalities on concrete integers by linear arithmetic. No external lemmas are required beyond the definition of the polynomial.
why it matters
Stage 1 of the topological Z-map derivation already shows that $k=6$ is the smallest positive even integerizer of all SM charges, while $k=3$ integerizes them but is odd. This theorem strengthens the preference for six: once the unique even quartic is fixed by Stage 2, the $k=6$ images sit strictly above the $k=3$ images on every family, so the face-count scale also maximizes family separation among the two natural candidates.
That separation feeds the later color-offset stage ($Z_{\mathrm{quark}}=2^{D-1}+\tilde{Q}^2+\tilde{Q}^4$ with $2^{D-1}=4$ at $D=3$) and the mass-ladder placement that uses these band labels. Framework landmarks in play are T8 ($D=3$ spatial dimensions, forcing $F=2D=6$) and the ledger integrality constraint that makes integerization mandatory. No downstream theorems currently depend on this declaration; it is a local comparison inside the verification module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.