Z_poly_zero
plain-language theorem explainer
Z_poly vanishes at zero charge for any natural coefficients a and b. Researchers deriving lepton charge indices from even polynomial ansatzes cite this to enforce neutral vanishing. The proof is a one-line algebraic reduction after unfolding the definition.
Claim. For natural numbers $a,b$, the charge index polynomial $Z(Q̃)=a Q̃^2 + b Q̃^4$ satisfies $Z(0)=0$.
background
The Z-map derivation module constructs the lepton charge index via an even polynomial ansatz $Z(Q̃)=a Q̃^2 + b Q̃^4$ that enforces charge-conjugation invariance, neutral vanishing, and non-negative coefficients. The sibling definition Z_poly implements this ansatz directly as $(a:ℤ)⋅q^2 + (b:ℤ)⋅q^4$. Upstream results supply the same polynomial in BaselineDerivation for charge-indexed masses and the present tick definition from TimeEmergence.
proof idea
The proof is a one-line wrapper that unfolds Z_poly and applies the ring tactic to obtain the algebraic identity at argument zero.
why it matters
This theorem confirms the neutral vanishing property demanded by the even polynomial ansatz in the Z-map derivation of Z_ℓ=1332. It supports the coefficient minimality section of the module and aligns with the Recognition Science requirement that charge indices vanish at neutral points. The result sits inside the integerization step that precedes the phi-ladder mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.