six_integerizes
plain-language theorem explainer
The integer 6 multiplies every Standard Model electric charge in {-1, 2/3, -1/3} into an integer. Anyone deriving the Z-map face-count scale from recognition topology on the 3-cube cites this fact. The proof is a three-case check: each charge is scaled by 6 and reduced by arithmetic to an explicit integer witness.
Claim. For every Standard Model electric charge $Q \in \{-1,\, 2/3,\, -1/3\}$, there exists an integer $n$ such that $6Q = n$.
background
This module derives the charge-to-band polynomial $Z(\tilde Q)$ from structural properties of recognition boundaries on the 3-cube, without anchor constraints or empirical masses. Stage 1 treats face-count integerization: a boundary of charge $Q$ couples to the $F$ faces of the cube, and the ledger requires integer entries (T8: $\delta$-units $\simeq \mathbb{Z}$), so the coupling must be integerized. At $D=3$ one has $F=2D=6$.
The three SM electric charges are the rationals $-1$, $2/3$, and $-1/3$. A natural number $k$ integerizes all of them when $kQ\in\mathbb{Z}$ for each such $Q$. That predicate is the local definition used by every integerization lemma in the module.
proof idea
Term-mode case split on membership in the SM charge list. After simplifying the membership hypothesis, three residual goals remain (one per charge). Each is closed by exhibiting an explicit integer witness: $6\cdot(-1)=-6$, $6\cdot(2/3)=4$, and $6\cdot(-1/3)=-2$, with the equalities discharged by norm_num.
why it matters
Supplies the positive half of the small-$k$ census: $k\in{1,2,4,5}$ fail while $k\in{3,6}$ succeed. It is the first conjunct of the claim that 6 is the smallest positive even integerization scale (3 also integerizes, but is odd). That minimality hypothesis is an input to the joint first-principles forcing theorem, which concludes that the canonical Z-map tuple is $(k,a,b,c)=(6,1,1,4)$ once even integerization, minimal complete ordered coefficients, and the edge-direction color offset are imposed. Framework landmark: T8 forces $D=3$, hence face count $F=2D=6$ as the Stage-1 scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.