quark_constraints_force_coeffs
plain-language theorem explainer
Integer coefficients of the even charge polynomial Z = c + a Q̃² + b Q̃⁴ are uniquely fixed to (a,b,c)=(1,1,4) by the up and down quark targets Z(4)=276 and Z(-2)=24, under a≥0 and b>0. Anyone closing the Z-map coefficient story cites this uniqueness step. The proof expands the two evaluations, subtracts to a linear Diophantine relation, and finishes with omega/linarith.
Claim. Let $Z(c,a,b;q)=c+a q^{2}+b q^{4}$ with $c,a,b\in\mathbb{Z}$. If $Z(c,a,b;4)=276$, $Z(c,a,b;-2)=24$, $a\ge 0$, and $b>0$, then $a=1$, $b=1$, and $c=4$.
background
The module studies a partial coefficient closure for the Z-map polynomial
$Z=c+a\tilde{Q}^{2}+b\tilde{Q}^{4}$. Here $\tilde{Q}$ is an integer charge proxy; the template is the even quartic Zpoly, so only even powers of charge enter.
Quark family targets supply two calibration points: up-type $Z_{u}=276$ at $\tilde{Q}=4$, and down-type $Z_{d}=24$ at $\tilde{Q}=-2$. Mild structural hypotheses keep the quadratic weight nonnegative ($a\ge 0$) and force a genuine quartic term ($b>0$).
The module states explicitly that this does not yet derive the polynomial from recognition topology; it only removes coefficient arbitrariness once the two quark anchors and the sign/presence constraints are granted.
proof idea
Unfold both evaluations of the polynomial template. The up constraint becomes $c+16a+256b=276$; the down constraint becomes $c+4a+16b=24$ (via simpa on the definition and ring rewrites).
Subtract with linarith to obtain the Diophantine relation $a+20b=21$. Under $a\ge 0$ and $b>0$ in $\mathbb{Z}$, omega forces $b=1$ and then $a=1$. Substitute back into the down equation with linarith to get $c=4$, and package the triple.
why it matters
In the Recognition Science mass/charge ladder story, the Z-map supplies the integer offset that sits on the $\varphi$-ladder mass formula. Fixing $(a,b,c)=(1,1,4)$ from quark data is the coefficient-forcing half of Pass 2: it turns an underdetermined even quartic into a rigid template before lepton offsets are specialized.
Sibling results in the same module then evaluate the forced polynomial on lepton and quark charges (lepton_value_with_forced_coeffs, quark_values_with_forced_coeffs). The module doc is candid that first-principles derivation from recognition topology remains open; this theorem only discharges coefficient freedom under the stated anchors.
No downstream consumers are wired yet in the graph, so the result presently stands as a local uniqueness lemma inside Verification rather than a link in the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.