Z_poly
plain-language theorem explainer
Z_poly supplies the explicit quartic form for the charge index as a q squared plus b q to the fourth, with a and b positive integers. Mass-ladder derivations in Recognition Science cite it when computing baseline Z values for leptons and quarks from the anchor map. The entry is a direct algebraic abbreviation with no proof obligations or hidden structure.
Claim. The charge-index polynomial is $Z(a,b,q) = a q^2 + b q^4$ for natural numbers $a,b$ and integer $q$.
background
The BaselineDerivation module upgrades boundary assumptions on rung integers to derived status by applying standard 3-cube combinatorics at D=3. Items include octave offset -8, lepton baseline 2, and Z-map monotonicity under a ≥ 1 and b ≥ 1. The Z-map polynomial is the explicit form that underlies the anchor relation for masses.
proof idea
This is a direct definition that unfolds to the polynomial expression a * q^2 + b * q^4. No lemmas are applied; it serves as the primitive for downstream monotonicity and equality proofs.
why it matters
The definition supplies the Z polynomial used in Z_strictly_increasing (B-26 derived) and in RSBridge.ZMapDerivation for unit_coefficients_minimal, Z_lepton_eq yielding 1332 at q = -6, and Z_lepton_matches_anchor_value. It closes the derivation of the lepton baseline from D=3 cube geometry, consistent with the mass formula on the phi-ladder and the even, neutral-vanishing properties required by charge-conjugation invariance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.