Zpoly
plain-language theorem explainer
Even quartic charge polynomial Z(c,a,b;q)=c+a q²+b q⁴ is the Z-map template for the second constraint pass. Anyone proving uniqueness of quark-sector coefficients (a,b,c)=(1,1,4) from the up/down anchors cites this form. It is a one-line integer arithmetic definition with no proof content.
Claim. For integers $c,a,b,q$, define the even quartic charge polynomial $Z(c,a,b;q) := c + a\,q^{2} + b\,q^{4}$.
background
The module closes part of the Z-map story. Recognition Science packages a charge-dependent integer map in the even quartic form $Z = c + a\tilde{Q}^{2} + b\tilde{Q}^{4}$. The tilde charge $\tilde{Q}$ is an integer proxy for the usual electric charge scaled to the recognition lattice.
Pass 2 takes two quark-family anchors as data: up-type $Z_{u}=276$ at $\tilde{Q}=4$, and down-type $Z_{d}=24$ at $\tilde{Q}=-2$. Mild structural side conditions are $a\ge 0$ (nonnegative quadratic weight) and $b>0$ (quartic term present). Under those, the three free coefficients are forced uniquely.
This definition is only the polynomial template. It does not yet derive the even-quartic shape from recognition topology; it fixes the algebraic object on which the coefficient constraints act.
proof idea
Pure definition: evaluate the integer expression $c + a\cdot q^{2} + b\cdot q^{4}$. No lemmas, no tactics, no hypotheses.
why it matters
Every uniqueness and evaluation theorem in the pass is stated in terms of this template. Downstream, quark_constraints_force_coeffs shows that the two quark anchors plus $a\ge 0$ and $b>0$ force $(a,b,c)=(1,1,4)$. The companion evaluations quark_values_with_forced_coeffs and lepton_value_with_forced_coeffs then plug those forced coefficients back in (with lepton offset $c=0$) and recover the numerical anchors by norm_num.
In the broader framework this removes coefficient arbitrariness from the Z-map before a first-principles derivation from recognition topology is available. It sits in the verification layer that checks consistency of mass/charge bookkeeping against the phi-ladder and eight-tick structure, rather than in the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.