unique_minimal_complete
plain-language theorem explainer
Among complete charge-to-band polynomials $Z=a\tilde{Q}^2+b\tilde{Q}^4$ with integer coefficients $a,b\ge 1$ that obey the ordered SM family hierarchy, the coefficient budget satisfies $a+b\ge 2$. Downstream uniqueness lemmas cite this as the lower bound that $(1,1)$ saturates. The proof is one-line linear arithmetic on the two positivity hypotheses; the hierarchy premise is unused.
Claim. For all integers $a,b\ge 1$, if the even polynomial $Z=a\tilde{Q}^2+b\tilde{Q}^4$ yields the ordered hierarchy $Z_{\mathrm{lepton}}>Z_{\mathrm{up}}>Z_{\mathrm{down}}>0$, then $a+b\ge 2$.
background
This module derives the charge-to-band map $Z(\tilde{Q})$ from recognition topology on the 3-cube, without mass anchors. Stage 2 requires $Z$ to be even in $\tilde{Q}$, non-negative, and zero at neutrality, so the minimal form is the complete even polynomial $Z=a\tilde{Q}^2+b\tilde{Q}^4$ with $a\ge 0$, $b>0$. Completeness here means both quadratic and quartic terms are present: $a\ge 1$ and $b\ge 1$.
The upstream predicate ordered_hierarchy a b encodes the physical separation demand $Z_{\mathrm{lepton}}>Z_{\mathrm{up}}>Z_{\mathrm{down}}>0$: the three SM families must be well-separated and ordered by charge magnitude. The doc-comment notes that incomplete budgets such as $(1,0)$ or $(0,1)$ can achieve $a+b=1$, but fail to match the spectrum's gap structure; among complete polynomials the minimal budget is $2$, achieved at $(1,1)$.
proof idea
Term-mode proof: introduce $a,b$ and the three hypotheses, discard the hierarchy premise, and discharge $a+b\ge 2$ by omega from the integer inequalities $a\ge 1$ and $b\ge 1$. No reference to the $Z$ evaluations is needed.
why it matters
Stage 2 of the Z-map derivation aims to force the canonical coefficients $(a,b)=(1,1)$ uniquely from family separation. This lemma supplies the sharp lower bound on the coefficient budget among complete ordered polynomials.
Three parents consume it: one_one_is_complete_ordered_minimizer uses the bound to show $(1,1)$ is minimal; complete_ordered_min_budget_forces_unit_coeffs combines $a+b=2$ with $a,b\ge 1$ to force unit coefficients; complete_ordered_minimizer_forces_unit_coeffs packages both into a single uniqueness statement. Together they close the selection rule that the physical spectrum's gap structure picks $Z=\tilde{Q}^2+\tilde{Q}^4$ (plus the Stage-3 color offset $2^{D-1}=4$ for quarks), consistent with T8 forcing $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.