zmap_canonical_tuple_satisfies_first_principles
plain-language theorem explainer
The canonical Z-map parameters (face scale 6, quadratic and quartic coefficients 1 and 1, color offset 4) jointly satisfy the four first-principles conditions used to characterize the charge-to-band map. Anyone citing the topological derivation of Z(Q̃) from the 3-cube, or the converse half of the canonical-tuple characterization, needs this bundle. The proof is a four-way conjunction assembled from the minimality of 6 as even integerizer, the uniqueness of (a,b)=(1,1), and the edge-direction count identity.
Claim. The scale $k=6$ integerizes all Standard Model charges $Q\in\{-1,2/3,-1/3\}$; every positive even integerizer is at least $6$; the coefficients $(a,b)=(1,1)$ are a complete ordered minimizer of the even band polynomial; and the color offset equals the edge-direction count $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 fixes the integerization scale: a charged boundary couples to the $F=2D$ faces of the cube, and the ledger demands integer entries (T8: $\delta$-units $\simeq\mathbb{Z}$). At $D=3$, $F=6$ is the least positive even $k$ with $kQ\in\mathbb{Z}$ for all three SM charges.
Stage 2 constrains the band label: $Z$ must be even in $\tilde Q$, non-negative, and vanish 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 for the three SM families force $a=b=1$. Stage 3 adds the color offset $2^{D-1}=4$ (edge directions of the cube) for quarks.
The four conjuncts here are exactly those first-principles conditions, packaged as the converse that the canonical tuple $(6,1,1,4)$ meets them all.
proof idea
Term-mode refine builds the four-way conjunction. The first two conjuncts are the two projections of six_smallest_positive_even_integerizer (that 6 integerizes all SM charges, and that it is minimal among positive even integerizers). The third is one_one_is_complete_ordered_minimizer, which records that $(a,b)=(1,1)$ is the complete ordered minimizer of the even band polynomial. The fourth goal is discharged by simp with edge_direction_eq_four and the natural-to-integer cast, equating the color offset $4$ to the edge-direction count.
why it matters
This is the converse half of the topological forcing of the Z-map. Downstream, canonical_tuple_iff_first_principles combines it with the forward forcing theorem to obtain the biconditional: a tuple $(k,a,b,c)$ satisfies the first-principles characterization if and only if it equals $(6,1,1,4)$. The same statement is re-exported in Masses.ZMapForcing as the upstreamed converse used by the mass-ladder side.
In the Recognition framework this closes Stage 1–3 of the module: face-count integerization at $D=3$ (T8), unique even quartic coefficients from family separation, and color offset $2^{D-1}=4$. It underwrites the claim that $Z_{\mathrm{lepton}}=\tilde Q^2+\tilde Q^4$ and $Z_{\mathrm{quark}}=4+\tilde Q^2+\tilde Q^4$ are forced by cube topology rather than fit to data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.