complete_ordered_min_budget_forces_unit_coeffs
plain-language theorem explainer
If integer coefficients a,b of a topology-compatible complete polynomial family are at least 1, obey the ordered hierarchy, and meet the minimal complete budget a+b=2, then necessarily (a,b)=(1,1). Mass-layer and Z-map forcing arguments cite this as the topology-only selection rule that pins the canonical unit coefficients. The proof is a one-line re-export of the verified statement from the Z-map topological derivation module.
Claim. Let $a,b\in\mathbb{Z}$ with $a\ge 1$, $b\ge 1$. If $(a,b)$ satisfies the ordered hierarchy condition and the minimal complete coefficient budget $a+b=2$, then $a=1$ and $b=1$.
background
The Masses Z-Map Forcing Bridge module lifts partial O2/O3 closure into the canonical mass-layer namespace so that forcing facts are consumable from Masses.*. It packages integerization-scale closure and the canonical anchor charge map values, while remaining short of full first-principles closure.
Here the objects are integer coefficients $(a,b)$ of a topology-compatible complete polynomial family. The ordered hierarchy is the structural ordering constraint on that family; the complete coefficient budget is the sum $a+b$. Completeness with positivity forces $a+b\ge 2$, so the equality $a+b=2$ is the minimal admissible budget.
The substantive selection rule lives in the Z-map topological derivation layer: in the complete ordered family the minimal budget forces the canonical unit pair. This declaration is the mass-layer bridge to that fact.
proof idea
One-line wrapper. The proof applies the identically named theorem from the Z-map topological derivation module to the four hypotheses (positivity of $a$, positivity of $b$, ordered hierarchy, and minimal budget), and returns the forced equality $(a,b)=(1,1)$. No local algebraic work is done here.
why it matters
This is the topology-only selection-rule bridge for the O2' minimizer path in the mass layer. Downstream, the minimizer-form companion uses it: any complete ordered minimizer unpacks to positivity, ordered hierarchy, and optimality, obtains $a+b\ge 2$ from uniqueness of the minimal complete budget, and then invokes this theorem to force $(a,b)=(1,1)$.
In the Recognition mass story the unit coefficients fix the canonical Z-map tuple that feeds the phi-ladder mass formula (yardstick times $\varphi$ to a rung offset). The module is explicit that this is partial O2/O3 progress, not full first-principles closure; the bridge makes the present forcing step directly available to mass-layer consumers without re-deriving the topological selection rule.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.