canonical_ordered
plain-language theorem explainer
The coefficient pair (a,b)=(1,1) for the even charge-to-band polynomial yields a strictly ordered family hierarchy Z_lepton > Z_up > Z_down > 0. Anyone arguing uniqueness of the canonical Z-map cites this base fact. The proof unfolds the polynomial at the three SM reduced charges and discharges the integer inequalities by linear arithmetic.
Claim. For the even charge-to-band polynomial $Z(\tilde{Q})=a\tilde{Q}^2+b\tilde{Q}^4$ (quarks shifted by the color offset $2^{D-1}=4$), the choice $a=1$, $b=1$ satisfies $Z_{\mathrm{lepton}}>Z_{\mathrm{up}}>Z_{\mathrm{down}}>0$.
background
This module derives the charge-to-band map $Z$ from recognition topology on the 3-cube, without anchor constraints or empirical masses. Stage 1 fixes the face-count integerization scale $F=6$ (at $D=3$) so that $FQ\in\mathbb{Z}$ for all SM charges $Q\in{-1,2/3,-1/3}$. Stage 2 forces an even non-negative polynomial vanishing at zero: $Z=a\tilde{Q}^2+b\tilde{Q}^4$. Stage 3 adds the quark color offset $2^{D-1}=4$.
The ordered-hierarchy predicate demands strict family separation ordered by charge magnitude: $Z_{\mathrm{lepton}}(a,b)>Z_{\mathrm{up}}(a,b)>Z_{\mathrm{down}}(a,b)>0$. Reduced charges are $\tilde{Q}{\mathrm{lepton}}=-6$, $\tilde{Q}{\mathrm{up}}=4$, $\tilde{Q}{\mathrm{down}}=-2$. The underlying polynomial is $Z{\mathrm{poly}}(a,b,q)=aq^2+bq^4$; quark sectors receive the color offset.
proof idea
Short term proof: unfold the ordered-hierarchy predicate together with the three sector $Z$ definitions, the polynomial $Z_{\mathrm{poly}}$, and the three $\tilde{Q}$ constants via simp only. The resulting concrete inequalities (numerically $1332>276>24>0$) are discharged by omega. No external lemmas beyond those definitional unfolds.
why it matters
Base arithmetic fact that unit coefficients already realize a physically ordered family hierarchy. Downstream, one_one_is_complete_ordered_minimizer packages it into the complete-ordered-minimizer predicate ("Canonical $(1,1)$ is a complete ordered minimizer"), and complete_ordered_minimizer_forces_unit_coeffs uses that packaging to force $(a,b)=(1,1)$ among all such minimizers ("Any complete ordered minimizer is forced to $(a,b)=(1,1)$").
Closes Stage 2 of the topological Z-map derivation: family separation plus ordering pins the coefficients. The color offset $4=2^{D-1}$ is the edge count along one spatial direction of the 3-cube, tying the construction to T8 ($D=3$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.