ordered_hierarchy
plain-language theorem explainer
Predicate on integer coefficients (a,b) of the even charge-to-band polynomial requiring the three SM family band labels to satisfy Z_lepton > Z_up > Z_down > 0. Anyone proving uniqueness of the unit coefficients (1,1) cites it as the family-separation and ordering constraint. It is a pure definitional conjunction of three strict inequalities on the evaluated Z-polynomial.
Claim. For integers $a,b$, the ordered-hierarchy property holds when the three family band values of the even polynomial $Z_{a,b}(\tilde Q)=a\tilde Q^2+b\tilde Q^4$ obey $Z_{a,b}(\tilde Q_\ell)>Z_{a,b}(\tilde Q_u)>Z_{a,b}(\tilde Q_d)>0$, i.e. lepton, up-quark, and down-quark bands are strictly ordered and positive.
background
This module derives the charge-to-band map $Z(\tilde Q)$ from recognition topology on the 3-cube, without anchor masses. Stage 1 fixes the integerization scale $\tilde Q=FQ$ with face count $F=6$ at $D=3$, the minimal positive even integer sending all SM charges ${-1,2/3,-1/3}$ into $\mathbb{Z}$. Stage 2 forces an even non-negative polynomial vanishing at zero; the minimal form is $Z=a\tilde Q^2+b\tilde Q^4$ with $a\ge 0$, $b>0$.
The three family evaluators are the polynomial at the lepton, up, and down integerized charges: $Z_\ell(a,b)=Z_{\mathrm{poly}}(a,b,\tilde Q_\ell)$ and likewise for up and down. Ordered hierarchy packages the physical demand that those three values be strictly separated and ordered by charge magnitude, with the lightest (down) still positive. Downstream selection rules then minimize the coefficient budget under this constraint.
proof idea
Definitional, not a proved theorem. The body is the three-way conjunction $Z_\ell(a,b)>Z_u(a,b)\land Z_u(a,b)>Z_d(a,b)\land Z_d(a,b)>0$, with each $Z$ the in-module polynomial evaluator at the corresponding $\tilde Q$. No tactics or lemmas; consumers unfold it and discharge the inequalities (typically by simp then omega, as in the canonical check for $(a,b)=(1,1)$).
why it matters
Stage-2 family separation is incomplete without an ordering-and-positivity filter; this predicate is that filter. It is the hypothesis hord in both in-module and Masses-side theorems complete_ordered_min_budget_forces_unit_coeffs, which state that a topology-compatible complete family that is ordered and meets the minimal budget $a+b=2$ is forced to $(a,b)=(1,1)$. The same predicate appears in complete_ordered_minimizer, complete_ordered_minimizer_forces_unit_coeffs, minimal_nonzero_coefficients, one_one_achieves_minimum, and quadratic_ordered.
Together with the face-count theorem $F=6$ (T8, $D=3$) and the color offset $2^{D-1}=4$, it closes the topology-only route to the canonical Z-map used for mass-ladder bands. The companion theorem canonical_ordered records that $(1,1)$ itself satisfies the predicate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.