three_integerizes
plain-language theorem explainer
For every Standard Model electric charge Q in {-1, 2/3, -1/3}, the product 3Q is an integer. Cited by anyone tracking the face-count integerization scale for the Z-map: k=3 works algebraically even though it later fails family separation. Proof is exhaustive case split on the three charges, each discharged by norm_num.
Claim. Let $\mathrm{sm\_charges}=\{-1,\,2/3,\,-1/3\}\subset\mathbb{Q}$. Then for every $Q$ in that set there exists $n\in\mathbb{Z}$ with $3Q=n$. Explicitly: $3\cdot(-1)=-3$, $3\cdot(2/3)=2$, $3\cdot(-1/3)=-1$.
background
Stage 1 of the Z-map derivation asks which positive integers $k$ make the ledger coupling $kQ$ integral for every Standard Model electric charge. The ledger (T8) demands integer $\delta$-units, so a recognition boundary of charge $Q$ must be integerized before it can enter the band polynomial.
The three charges are fixed as the list ${-1,,2/3,,-1/3}$. The predicate integerizes_all k asserts $\forall Q$ in that list, $\exists n\in\mathbb{Z}$ with $kQ=n$. The face count of the 3-cube is $F=2D=6$ at $D=3$; the module aims to prove that $6$ is the minimal positive even such $k$. Checking $k=3$ is a necessary intermediate step: it succeeds at pure integerization, so the later uniqueness argument must exclude it on other grounds (family separation and hierarchy strength).
proof idea
Unfold integerizes_all 3 and introduce an arbitrary charge $Q$ with membership in sm_charges. Simplify the membership hypothesis against the concrete three-element list, then rcases into the three equality cases $Q=-1$, $Q=2/3$, $Q=-1/3$. Each case is closed by exhibiting the integer witness ($-3$, $2$, $-1$ respectively) and discharging the rational equality with norm_num. No external lemmas beyond the local definitions are required.
why it matters
Feeds directly into integerization_results, which packages the full dichotomy: $k\in{1,2,4,5}$ fail integerization while $k\in{3,6}$ succeed. That package is the algebraic half of Stage 1 of the topological Z-map derivation: once both $3$ and $6$ are known to integerize, the module can argue that only the even scale $F=6$ (face count at $D=3$, landmark T8) is admissible, because $k=3$ collapses family separation ($Z_\mathrm{up}(a{=}1,b{=}1)=Z_\mathrm{down}(a{=}1,b{=}1)$ after the color offset is restored) and yields a weak hierarchy. Without this positive witness the later uniqueness claim for the face-count scale would have a gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.