integerizes_all
plain-language theorem explainer
A natural number k integerizes the Standard Model charges when kQ is an integer for every Q in {−1, 2/3, −1/3}. Mass and Z-map forcing arguments cite this predicate to state minimality of the face-count scale F = 6. The body is a one-line universal quantification over the fixed charge list.
Claim. For $k \in \mathbb{N}$, the predicate holds iff for every Standard Model electric charge $Q \in \{-1, 2/3, -1/3\}$ there exists $n \in \mathbb{Z}$ with $k \cdot Q = n$ (equality in $\mathbb{Q}$).
background
The module derives the charge-to-band map $Z(\tilde{Q})$ from recognition boundaries on the 3-cube, without mass anchors. Stage 1 requires that a boundary of charge $Q$ couple to the $F = 2D$ faces so that ledger entries stay integral (T8: $\delta$-units $\simeq \mathbb{Z}$). At $D = 3$ one has $F = 6$.
The three SM charges are fixed as the rational list $\mathrm{sm_charges} = {-1, 2/3, -1/3}$. Integerization means clearing denominators: $kQ \in \mathbb{Z}$ for each such $Q$. The predicate packages that check for an arbitrary candidate scale $k$.
Upstream, the charge list is a plain definition; the universal quantifier shape mirrors the TraceLogic all pattern (family-indexed stability), but here the family is just the finite charge list and the predicate is pure arithmetic.
proof idea
Definitional, not a proved theorem. The body is the Prop
$\forall Q \in \mathrm{sm_charges},; \exists n:\mathbb{Z},; (k:\mathbb{Q})\cdot Q = \uparrow n$.
No tactics or lemmas fire at the definition site; downstream failure/success theorems discharge membership in sm_charges by simp and solve the resulting rational equations by linarith.
why it matters
This is the Stage-1 gate for the topological Z-map. Downstream, six_smallest_positive_even_integerizer and smallest_positive_even_integerization_scale assert that $k=6$ is the least positive even integer satisfying the predicate, matching face count $F=2D$ at $D=3$ (forcing chain T8). Failure lemmas one_fails through five_fails rule out smaller candidates.
The same predicate appears in the bundled first-principles tuple and in Masses.ZMapForcing: any $(k,a,b,c)$ obeying smallest-even integerization, minimal ordered coefficients, and edge-direction color offset is forced to $(6,1,1,4)$. Thus the definition is the arithmetic interface between cube topology and the canonical band polynomial $Z = a\tilde{Q}^2 + b\tilde{Q}^4$ plus color offset $2^{D-1}=4$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.