Z_poly_even
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not derive or constrain the coefficients a and b.
- Does not compute the numerical value of Z for any specific charge.
- Does not address the geometric origin of the integerization factor k = 6.
- Does not connect the polynomial to the phi-ladder or mass formula.
formal statement (Lean)
58theorem Z_poly_even (a b : ℕ) (q : ℤ) :
59 Z_poly a b q = Z_poly a b (-q) := by
proof body
Term-mode proof.
60 unfold Z_poly; ring
61
62/-- Z vanishes at neutral: Z(0) = 0. -/