six_smallest_positive_even_integerizer
plain-language theorem explainer
Six is the smallest positive even natural that multiplies every Standard Model charge in {-1, 2/3, -1/3} into an integer. Anyone fixing the Z-map integerization scale from first principles cites this minimality. The proof pairs the direct check that six works with a short case split eliminating the only smaller positive even candidates, two and four.
Claim. $6$ integerizes all Standard Model charges $Q\in\{-1,2/3,-1/3\}$ (i.e., $6Q\in\mathbb{Z}$ for each), and every positive even natural $k$ that likewise integerizes all three charges satisfies $k\ge 6$.
background
This module derives the charge-to-band polynomial from recognition boundaries on the 3-cube, without anchors or empirical masses. Stage 1 fixes the integerization scale: a boundary of charge $Q$ couples to the $F$ faces of the cube, and the ledger demands integer entries (T8: $\delta$-units $\simeq\mathbb{Z}$). At $D=3$ one has $F=2D=6$, so $\tilde Q=FQ$ is the candidate scale.
A natural $k$ integerizes all SM charges when, for every $Q\in{-1,2/3,-1/3}$, there is $n\in\mathbb{Z}$ with $kQ=n$. Upstream lemmas record that $k=6$ succeeds on all three values, while $k=2$ fails on the $\pm 1/3$ charges and $k=4$ fails on $-1/3$. The odd scale $k=3$ also integerizes, but Stage 1 restricts to even $k$ (parity of the face count).
proof idea
Split the conjunction. The first half is the existing lemma that six integerizes every SM charge. For minimality, take positive even $k$ that integerizes all charges. Evenness gives $k\bmod 2=0$; omega then yields the trichotomy $k=2$ or $k=4$ or $k\ge 6$. The $k=2$ branch contradicts the lemma that two fails on the $1/3$ charges; the $k=4$ branch contradicts the lemma that four fails on $-1/3$. The remaining branch is $k\ge 6$.
why it matters
Stage 1 of the topological Z-map derivation: at $D=3$, face count $F=6$ is forced as the minimal positive even integerizer for SM charges, linking T8 (three spatial dimensions and integer ledger units) to the 3-cube. Downstream, the masses layer re-exports the same statement as the smallest positive even integerization scale. The joint first-principles theorems use the minimality hypothesis to force the canonical tuple $(k,a,b,c)=(6,1,1,4)$ and, conversely, to verify that the canonical tuple meets every first-principles condition. Without this pin, $\tilde Q=kQ$ would not be unique before the even-polynomial and color-offset stages.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.