IndisputableMonolith.Verification.ZMapConstraintPass2
Module supplying an even quartic charge-polynomial template for Z-map residuals, plus algebraic lemmas that force its coefficients from quark constraints and evaluate the resulting lepton and quark values. Verification authors cite it when checking discrete charge assignments against the Recognition ladder. Argument is definitional setup followed by equational coefficient forcing.
claimAn even quartic charge polynomial $Z(q)=a_4 q^4+a_2 q^2+a_0$ is introduced as a template for Z-map residuals. Quark-side constraints force the free coefficients $(a_4,a_2,a_0)$; under those forced coefficients the module records the resulting lepton and quark residual values.
background
In Recognition Science verification, species sit on the $\varphi$-ladder with integer rungs and a charge-sensitive gap term. The mass formula is yardstick $\cdot\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$, so any residual charge map $Z$ must be algebraically constrained before ladder values are certified.
This module works in the Verification domain and imports only Mathlib. It treats $Z$ as an even quartic polynomial in a charge coordinate $q$ (only even powers, degree at most four). Sibling objects name the polynomial template, the quark constraints that pin its coefficients, and the lepton/quark evaluations obtained once those coefficients are fixed.
The setting is purely algebraic: no continuum limit, no analytic estimates, and no appeal to the T0--T8 forcing chain beyond the ambient RS units.
proof idea
Definition-first module, not a single deep theorem. The even-quartic template is declared, then quark constraints are applied as algebraic equations that force the free coefficients. With coefficients substituted, short evaluation lemmas compute the lepton and quark residual values. Structure is equational forcing and substitution rather than tactic-heavy proof.
why it matters in Recognition Science
Occupies the second pass of the Z-map constraint pipeline inside Verification. It turns an under-determined even-quartic charge template into a coefficient-fixed object that downstream ladder checks can consume when certifying quark and lepton residuals against the $\varphi$-ladder mass formula. Supports consistency of discrete charge assignments with the eight-tick octave bookkeeping, without itself reopening T5--T8. Parent consumers are the broader Z-map and species-value certificates that sit above this pass.
scope and limits
- Does not derive the RS mass formula or the phi-ladder itself.
- Does not prove that degree four is the only admissible polynomial degree.
- Does not address continuum, QFT, or experimental matching.
- Does not discharge any step of the T0--T8 forcing chain.
- Does not claim uniqueness of the forced coefficients outside the stated quark constraints.