quark_values_with_forced_coeffs
plain-language theorem explainer
With forced coefficients (c,a,b)=(4,1,1), the even quartic charge polynomial evaluates to the two quark family anchors: 276 at charge 4 and 24 at charge -2. Anyone checking that the uniquely forced Z-map coefficients still hit the up- and down-type targets cites this. The proof is a two-goal arithmetic check after unfolding the polynomial.
Claim. For the even quartic $Z(c,a,b;q)=c+a q^{2}+b q^{4}$, the forced coefficients give $Z(4,1,1;4)=276$ and $Z(4,1,1;-2)=24$.
background
The module studies a partial closure of the Z-map polynomial $Z=c+a\tilde{Q}^{2}+b\tilde{Q}^{4}$. Quark family targets fix the anchors: up-type $Z_{u}=276$ at $\tilde{Q}=4$, down-type $Z_{d}=24$ at $\tilde{Q}=-2$. Mild structural constraints ($a\ge 0$, $b>0$) force the unique triple $(a,b,c)=(1,1,4)$.
Zpoly is the integer template for that polynomial: $c+a q^{2}+b q^{4}$. The sibling result that forces the coefficients is the uniqueness theorem under those constraints; the present statement only rechecks that the forced triple recovers the two anchors exactly.
proof idea
Term-mode proof: split the conjunction with constructor, then on each goal run norm_num after unfolding Zpoly. That reduces $4+1\cdot 4^{2}+1\cdot 4^{4}$ and $4+1\cdot(-2)^{2}+1\cdot(-2)^{4}$ to $276$ and $24$ by pure integer arithmetic. No external lemmas beyond the definition.
why it matters
Closes the verification loop for Pass 2 of the Z-map: once quark constraints force $(a,b,c)=(1,1,4)$, those same coefficients must still reproduce the family anchors used as input. The module doc is explicit that this does not yet derive the polynomial from recognition topology; it only removes coefficient arbitrariness. No downstream dependents are recorded yet; the natural consumers are any later lepton or full-spectrum checks that assume the forced triple (the sibling lepton evaluation sits alongside it). In the broader RS ladder, Z enters mass and charge bookkeeping on the phi-ladder, so locking the polynomial coefficients is a prerequisite for non-arbitrary rung assignments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.