Z_poly_even
plain-language theorem explainer
The charge index polynomial Z_poly is even in its integerized charge argument, confirming invariance under sign flip. Researchers deriving lepton masses from the even polynomial ansatz would cite this to justify the form Z(Q̃) = a Q̃² + b Q̃⁴. The proof is a one-line algebraic reduction that unfolds the definition and applies ring normalization.
Claim. For natural numbers $a, b$ and integer $q$, the charge index polynomial satisfies $a q^2 + b q^4 = a (-q)^2 + b (-q)^4$.
background
The RSBridge.ZMapDerivation module derives the lepton charge index Z_ℓ = 1332 from an even polynomial ansatz Z(Q̃) = a·Q̃² + b·Q̃⁴. This ansatz encodes charge-conjugation invariance together with neutral vanishing (no constant term) and non-negative coefficients. The definition Z_poly (a b : ℕ) (q : ℤ) := (a : ℤ) * q ^ 2 + (b : ℤ) * q ^ 4 supplies the explicit polynomial used throughout the module.
proof idea
The term proof unfolds Z_poly to expose the monomials in q and invokes the ring tactic. Ring normalization directly confirms the two sides are identical because every power of q that appears is even.
why it matters
Evenness of Z_poly justifies the structural choice of even powers in the charge index polynomial for the lepton sector. It supports the coefficient-minimality step that yields Z_ℓ = 1332 and is presupposed by sibling results such as Z_lepton_eq and Z_lepton_decomposition. The property is independent of the specific values of a and b provided they remain natural numbers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.