Z_poly
plain-language theorem explainer
Z_poly defines the quartic polynomial Z(Q̃) = a Q̃² + b Q̃⁴ for computing charge indices from integerized charges in the lepton sector. Researchers working on lepton mass assignments or charge-conjugation properties in the Recognition framework cite this form. The definition is a direct algebraic encoding of the even ansatz with non-negative coefficients and no constant term.
Claim. The charge index polynomial is given by $Z(Q̃) = a Q̃^2 + b Q̃^4$ for natural numbers $a, b$ and integer charge index $Q̃$.
background
The Z-Map Derivation module computes the lepton charge index from an even polynomial ansatz on the integerized charge. Charge integerization uses k = F(3) = 6 faces of the cube Q₃, so the electron charge index is Q̃_e = 6 · (-1) = -6. The ansatz Z(Q̃) = a Q̃² + b Q̃⁴ enforces charge-conjugation invariance, neutral vanishing at Q̃=0, and non-negative coefficients.
proof idea
The declaration is a direct definition that expands to the expression (a : ℤ) * q ^ 2 + (b : ℤ) * q ^ 4. It requires no lemmas or tactics and serves as the base case for theorems establishing evenness and specific evaluations such as Z_poly_even and Z_lepton_eq.
why it matters
Z_poly supplies the polynomial form used to obtain Z_ℓ = 1332 in Z_lepton_eq and to confirm agreement with the hardcoded anchor value. It underpins the strictly increasing property in BaselineDerivation.Z_strictly_increasing and the minimal coefficient result in unit_coefficients_minimal. The construction aligns with the mass formula on the phi-ladder by furnishing the charge index Z for leptons.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.