complete_ordered_minimizer
plain-language theorem explainer
An integer coefficient pair (a,b) is a complete ordered minimizer when both are at least one, the band labels obey the lepton-up-down hierarchy, and no other such pair has a smaller sum a+b. Z-map and mass-forcing arguments cite this as the selection rule that pins the quartic charge polynomial. The definition packages positivity, ordered hierarchy, and global minimality of the coefficient sum into one predicate.
Claim. An integer pair $(a,b)$ is a complete ordered minimizer if $a \ge 1$, $b \ge 1$, the associated band labels satisfy $Z_{\mathrm{lepton}}(a,b) > Z_{\mathrm{up}}(a,b) > Z_{\mathrm{down}}(a,b) > 0$, and every other pair $(a',b')$ of integers $\ge 1$ that also obeys that ordered hierarchy has $a+b \le a'+b'$.
background
This module derives the charge-to-band polynomial $Z(\tilde{Q})$ from recognition boundaries on the 3-cube, without anchor masses. Stage 2 requires a gauge-invariant even polynomial $Z = a\tilde{Q}^2 + b\tilde{Q}^4$ with $a \ge 0$, $b > 0$, vanishing at neutral charge. Family separation then forces the coefficients.
The upstream predicate ordered hierarchy states that $Z_{\mathrm{lepton}} > Z_{\mathrm{up}} > Z_{\mathrm{down}} > 0$: the three SM families are well-separated and ordered by charge magnitude. That is the physical complete-family constraint.
The present definition strengthens that constraint to a minimizer form: among all positive integer pairs that realize the hierarchy, select those with minimal $a+b$. This is the complete-family selection rule used later to force unit coefficients.
proof idea
Definitional packaging, not a proved theorem. The body is the conjunction of four clauses: $a \ge 1$, $b \ge 1$, the ordered-hierarchy predicate on $(a,b)$, and a universal minimality quantifier over all other positive integer pairs that satisfy ordered hierarchy, requiring $a+b \le a'+b'$. No tactics or lemmas are applied; the Prop is the selection rule itself.
why it matters
Stage 2 of the topological Z-map derivation needs a clean selection rule that forces $a=1$, $b=1$ for the quartic $Z = a\tilde{Q}^2 + b\tilde{Q}^4$. This predicate is that rule in minimizer form.
Downstream, complete_ordered_minimizer_forces_unit_coeffs shows every such minimizer is exactly $(1,1)$. The bundled first-principles tuple then combines it with smallest-even integerization ($k=6$ at $D=3$) and edge-direction color offset ($c=4=2^{D-1}$) to force the canonical $(k,a,b,c)=(6,1,1,4)$. Masses.ZMapForcing re-exports the same bridge for O2' mass-ladder work.
In the forcing chain this sits under T8 ($D=3$) face-count integerization and feeds the unique SM band polynomial used on the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.