sm_charges

This module derives the charge-to-band polynomial $Z(\tilde Q)$ from recognition boundaries on the 3-cube, without anchor constraints or empirical masses. Stage 1 asks for a face-count integerization scale: a recognition boundary of charge $Q$ couples to the $F$ faces of the cube, and the ledger demands integer entries (T8: $\delta$-units $\simeq \mathbb{Z}$). The face count $F = 2D$ is the candidate scale.

At $D = 3$ one has $F = 6$. The claim to prove is that $6$ is the least positive even integer $k$ such that $kQ \in \mathbb{Z}$ for every Standard Model charge. The three charges that enter that quantification are exactly the list defined here: electron charge $-1$, up-type $2/3$, down-type $-1/3$.

The predicate integerizes_all k is universal quantification over membership in this list: for every $Q$ in the list there exists $n \in \mathbb{Z}$ with $k \cdot Q = n$.

Definitional. The body is the concrete list literal $[-1,, 2/3,, -1/3]$ of type $\mathrm{List},\mathbb{Q}$. No tactics, no lemmas. Downstream proofs discharge membership by simp on this definition and then case-split the three constructors.

Stage 1 of the topological Z-map derivation rests on this fixed charge set. The parent results six_integerizes, three_integerizes, and the failure theorems one_fails, two_fails, four_fails, five_fails all quantify over membership in the list; together they establish that $F = 6$ (at $D = 3$) is the minimal positive even integerizer of SM charges, matching the face count of the 3-cube forced by T8.

Without a single shared list, the integerization theorems would not be comparable. Later stages (even polynomial form $Z = a\tilde Q^2 + b\tilde Q^4$, family separation forcing $a = b = 1$, and the color offset $2^{D-1} = 4$) inherit the same charge set through the integerized coordinate $\tilde Q = FQ$.