canonical_tuple_forced_from_anchor_outputs
plain-language theorem explainer
If the lepton and quark Z-polynomials of a topology-compatible family hit the three canonical anchor charge values, the integer coefficients are forced to (a,b,c)=(1,1,4). Mass-layer workers cite this to pin the unique Z-map tuple once anchors are fixed. The proof rewrites the sector equalities to the numeric anchors 1332, 276, 24, then applies the full-anchor coefficient-forcing lemma.
Claim. Let $a,b,c\in\mathbb{Z}$. Write the lepton family as $Z_{\ell}(a,b)=a\tilde{Q}^2+b\tilde{Q}^4$ and the offset quark families as $Z_{u}(c,a,b)=c+a\tilde{Q}^2+b\tilde{Q}^4$ and $Z_{d}(c,a,b)=c+a\tilde{Q}^2+b\tilde{Q}^4$. If $Z_{\ell}(a,b)$ equals the lepton anchor at charge $-1$, $Z_{u}(c,a,b)$ equals the up-quark anchor at charge $2/3$, and $Z_{d}(c,a,b)$ equals the down-quark anchor at charge $-1/3$, then $a=1$, $b=1$, and $c=4$.
background
The module Masses.ZMapForcing packages partial O2/O3 closure for the mass layer: the smallest positive even integerization scale that clears SM charges is $k=6$, and the canonical anchor charge map evaluates to three fixed family values $Z_{\ell}=1332$, $Z_{u}=276$, $Z_{d}=24$.
A topology-compatible complete family takes the polynomial shape $Z_{\mathrm{lepton}}=a\tilde{Q}^2+b\tilde{Q}^4$ and $Z_{\mathrm{quark}}=c+a\tilde{Q}^2+b\tilde{Q}^4$, with integer coefficients $(a,b,c)$. The charge-index map ChargeIndex.Z assigns each algebraic sector (lepton, up quark, down quark) and electric charge the corresponding anchor integer.
Upstream, anchor_charge_map_values records those three numeric anchors, and full_anchor_tuple_forces_coefficients_and_offset solves the resulting Diophantine system for $(a,b,c)$. This bridge is not yet full first-principles closure; it makes the current forcing progress consumable from the mass namespace.
proof idea
Tactic proof in three short blocks. First, unpack anchor_charge_map_values to obtain the three equalities $Z_{\ell}\mapsto 1332$, $Z_{u}\mapsto 276$, $Z_{d}\mapsto 24$. Second, rewrite each hypothesis along the corresponding anchor: the lepton match becomes $Z_{\mathrm{lepton}},a,b=1332$, and likewise for the offset up and down maps. Third, feed the three numeric equalities into full_anchor_tuple_forces_coefficients_and_offset, which returns $a=1\land b=1\land c=4$. No further case splits or arithmetic are local to this proof.
why it matters
This is the mass-layer bridge that converts anchor-matching hypotheses into the unique coefficient triple $(1,1,4)$ for the Z-map family. It sits beside the sibling first-principles statements (zmap_canonical_tuple_forced_from_first_principles, canonical_tuple_iff_first_principles) that aim to replace the anchor inputs by topology-only selection rules (ordered complete families with minimal coefficient budget forcing unit $(a,b)$).
In the broader RS mass formula, yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$ on the $\varphi$-ladder, a forced Z-map fixes the integer content of the gap term. The module explicitly notes this is not full first-principles closure yet: anchors are still an intermediate interface. No downstream consumers are wired yet (used_by empty), so the immediate role is to expose the forcing fact cleanly inside Masses.* for later mass-spectrum theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.