integerization_results
plain-language theorem explainer
Among positive integers 1 through 6, only 3 and 6 send every Standard Model electric charge into the integers; 1, 2, 4, and 5 each leave at least one charge fractional. Anyone citing the face-count integerization stage of the Z-map derivation needs this exhaustive check. The proof is a six-component product of the already-proved per-scale lemmas.
Claim. Writing $\mathrm{int}(k)$ for the assertion that $kQ\in\mathbb{Z}$ for every Standard Model charge $Q\in\{-1,2/3,-1/3\}$, one has $\neg\mathrm{int}(1)\land\neg\mathrm{int}(2)\land\mathrm{int}(3)\land\neg\mathrm{int}(4)\land\neg\mathrm{int}(5)\land\mathrm{int}(6)$.
background
The module derives the charge-to-band polynomial $Z(\tilde Q)$ from recognition boundaries on the 3-cube, without anchor masses. Stage 1 fixes the integerization scale: a boundary of charge $Q$ couples to the $F=2D$ faces of the cube, and the ledger (T8) demands integer $\delta$-units, so $kQ$ must lie in $\mathbb{Z}$ for a canonical scale $k$.
The three SM values are $Q\in{-1,2/3,-1/3}$. The predicate behind the claim is that a positive integer $k$ integerizes all three at once. Face count at $D=3$ is $F=6$; the module also records that 3 integerizes but is odd, while 6 is the smallest positive even integerizer.
The six per-scale lemmas (failure for 1, 2, 4, 5; success for 3 and 6) are already proved in-module; this declaration only packages them.
proof idea
Pure term-mode packaging: the goal is a six-fold conjunction, and the proof is the ordered 6-tuple of the sibling lemmas that establish failure at 1 and 2, success at 3, failure at 4 and 5, and success at 6. No further arithmetic is performed here; each conjunct is discharged by name.
why it matters
This is the exhaustive Stage-1 census that the Z-map derivation certificate consumes. Downstream, derivation_complete builds a ZMapDerivation record whose integerization field is exactly this theorem (alongside face-count equals six, charge-conjugation invariance, neutral vanishing, and family separation).
In the framework it locks the face-count story to T8 ($D=3$ spatial dimensions, $\delta$-units $\simeq\mathbb{Z}$) and to the eight-tick cube geometry: $F=2D=6$ is forced as the minimal positive even integerization scale for SM charges. Together with the later uniqueness of $Z=a\tilde Q^2+b\tilde Q^4$ under family separation, it underwrites the lepton/quark band formulas without empirical mass anchors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.