complete_ordered_min_budget_forces_unit_coeffs
plain-language theorem explainer
In the complete ordered coefficient family for the Z-map polynomial, the minimal budget a+b=2 with a,b≥1 forces the canonical pair (a,b)=(1,1). Masses and verification layers cite this as the selection-rule form of Stage-2 uniqueness. The proof pairs the unique-minimal-complete lower bound with linear arithmetic and omega.
Claim. Let $a,b\in\mathbb{Z}$ with $a\ge 1$, $b\ge 1$, and suppose $(a,b)$ lies in the ordered complete hierarchy for the even charge polynomial. If the coefficient budget is minimal, $a+b=2$, then necessarily $a=1$ and $b=1$.
background
This module derives the charge-to-band map $Z(\tilde Q)$ from recognition boundaries on the 3-cube, without mass anchors. Stage 1 fixes the integerization scale $\tilde Q=FQ$ with face count $F=6$ at $D=3$ (the least positive even $k$ sending all SM charges ${-1,2/3,-1/3}$ into $\mathbb{Z}$). Stage 2 requires a gauge-invariant band label: even in $\tilde Q$, nonnegative, and vanishing at zero. The minimal even polynomial is $Z=a\tilde Q^2+b\tilde Q^4$ with $a\ge 0$, $b>0$.
The ordered hierarchy packages the complete-family constraints on integer coefficients $(a,b)$: positivity, ordering, and distinct $Z$ values across the three SM families (family separation). The coefficient budget is the sum $a+b$. An upstream lemma unique_minimal_complete already shows every complete ordered pair satisfies $a+b\ge 2$. This theorem is the matching selection rule at the floor budget.
proof idea
Apply unique_minimal_complete to the hypotheses $a\ge 1$, $b\ge 1$, and ordered hierarchy to obtain $a+b\ge 2$. The assumption $a+b=2$ gives the matching upper bound, so the sum equals 2. With both summands positive integers at least 1, omega forces $a=1$ and $b=1$. The conclusion is the pair of equalities.
why it matters
Stage 2 of the topological Z-map derivation claims that family separation forces the canonical coefficients $(a,b)=(1,1)$. This theorem is the budget form of that claim: once the complete ordered family is fixed and the budget is pinned at its proven minimum 2, only unit coefficients survive. Downstream, complete_ordered_minimizer_forces_unit_coeffs packages the same fact for the minimizer predicate, and Masses.ZMapForcing.complete_ordered_min_budget_forces_unit_coeffs re-exports it as the topology-only bridge into the mass ladder.
Together with Stage 1 ($F=6$ from $D=3$, landmark T8) and Stage 3 (color offset $2^{D-1}=4$), this locks $Z_{\mathrm{lepton}}=\tilde Q^2+\tilde Q^4$ and $Z_{\mathrm{quark}}=4+\tilde Q^2+\tilde Q^4$ used by the phi-ladder mass formula. No empirical mass fit enters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.