zmap_canonical_tuple_forced_from_first_principles
plain-language theorem explainer
Any positive even integerization scale that is minimal among those clearing all SM charges, paired with complete-ordered-minimal polynomial coefficients and a color offset equal to the cube edge-direction count, is forced to the tuple (6, 1, 1, 4). Mass and Z-map authors cite this as the joint first-principles uniqueness of the charge-to-band map. The proof sandwiches k between two inequalities, then applies the unit-coefficient and edge-count lemmas.
Claim. Let $k \in \mathbb{N}$ be positive and even, and suppose $k$ integerizes all three Standard Model charges $\{-1, 2/3, -1/3\}$. If $k$ is minimal among all such positive even integerizers, if the even polynomial coefficients $(a,b)$ are a complete ordered minimizer (family-separating with $a \ge 0$, $b > 0$), and if the color offset $c$ equals the number of edge directions of the 3-cube, then $k = 6$, $a = 1$, $b = 1$, and $c = 4$.
background
This module derives the charge-to-band polynomial $Z(\tilde{Q})$ from recognition boundaries on the 3-cube, without anchors or empirical masses. Stage 1: a charged boundary couples to the $F = 2D$ faces; the ledger demands integer entries (T8: $\delta$-units $\simeq \mathbb{Z}$), so the coupling must integerize. At $D = 3$, $F = 6$ is the smallest positive even $k$ with $kQ \in \mathbb{Z}$ for all $Q \in {-1, 2/3, -1/3}$.
Stage 2: gauge constraints force $Z$ even in $\tilde{Q}$, non-negative, and vanishing at zero, so the minimal form is $Z = a\tilde{Q}^2 + b\tilde{Q}^4$ with $a \ge 0$, $b > 0$. Distinct $Z$ values on the three SM families force $a = b = 1$. Stage 3: quarks gain $2^{D-1}$ extra channels along cube edge directions, giving color offset $c = 4$.
The predicate integerizes_all packages the three charge-clearing conditions; complete_ordered_minimizer packages the family-separation minimality on $(a,b)$; edge_direction_count is the combinatorial edge tally used for $c$.
proof idea
Tactic proof in three blocks. First force $k = 6$: apply the minimality hypothesis at $k' = 6$ (using positivity, evenness of 6, and the sibling six_integerizes) to get $k \le 6$; apply the sibling six_smallest_positive_even_integerizer to get $6 \le k$; conclude by omega.
Second, invoke complete_ordered_minimizer_forces_unit_coeffs on the ordered-minimizer hypothesis to obtain $a = 1$ and $b = 1$.
Third, rewrite the color-offset hypothesis through the lemma edge_direction_eq_four (edge-direction count equals 4) to get $c = 4$. Package the four equalities as the conclusion.
why it matters
Closes the joint forward direction of the three-stage topological derivation of the Z-map: face-count integerization, gauge-minimal even polynomial, and edge-direction color offset together pin the unique tuple $(6,1,1,4)$. Downstream, canonical_tuple_iff_first_principles uses this as the forward half of the biconditional characterizing the canonical tuple; Masses.ZMapForcing re-exports the same statement for the mass ladder.
In the Recognition chain this sits on T8 ($D = 3$), which fixes face count $F = 2D = 6$ and edge-direction count $2^{D-1} = 4$. The resulting $Z$ feeds the phi-ladder mass formula (yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$), so uniqueness of $(k,a,b,c)$ is uniqueness of the band labels that separate lepton and quark sectors. No scaffolding remains on this arrow; the converse direction is the sibling theorem immediately below.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.