lepton_value_with_forced_coeffs
plain-language theorem explainer
With forced coefficients a = 1, b = 1 and lepton offset c = 0, the quartic-even Z-map at charge Q̃ = −6 equals 1332 exactly. Anyone anchoring lepton family values against the Z-polynomial template would cite this. The proof is a one-line numerical normalization after unfolding the polynomial definition.
Claim. With coefficients $c = 0$, $a = 1$, $b = 1$, the quartic-even charge polynomial $Z(\tilde{Q}) = c + a\tilde{Q}^{2} + b\tilde{Q}^{4}$ satisfies $Z(-6) = 1332$.
background
The module studies partial derivational closure of the Z-map polynomial $Z = c + a\tilde{Q}^{2} + b\tilde{Q}^{4}$. Quark family targets fix $Z_u = 276$ at $\tilde{Q} = 4$ and $Z_d = 24$ at $\tilde{Q} = -2$. Under the mild structural constraints $0 \le a$ and $0 < b$, the coefficients are uniquely forced to $(a,b,c) = (1,1,4)$.
The in-module template Zpoly is the integer quartic-even form $c + a q^{2} + b q^{4}$. For leptons the same forced $(a,b)$ are retained, but the constant offset is taken as $c = 0$ rather than the quark value $c = 4$. The evaluation point $\tilde{Q} = -6$ is the lepton charge slot used by the pass.
This does not yet derive the polynomial from recognition topology; it only removes coefficient arbitrariness once the structural assumptions and family targets are granted.
proof idea
One-line tactic proof. Unfold the definition of the quartic-even template and apply norm_num to evaluate
$0 + 1\cdot(-6)^{2} + 1\cdot(-6)^{4} = 36 + 1296 = 1332$
over the integers. No external lemmas are required beyond the definition itself.
why it matters
The sibling result that quark constraints force $(a,b,c) = (1,1,4)$ leaves the lepton sector with the same $(a,b)$ but offset $c = 0$. This theorem pins the resulting lepton anchor at 1332, so the Z-map is no longer free once the forced coefficients are installed.
In the broader Recognition framework the Z-map sits in the verification layer that checks mass and charge ladder consistency against the phi-ladder mass formula and the eight-tick octave structure. Closing coefficient freedom here is a step toward matching family anchors without hand-tuned polynomials. The module itself notes that full derivation from recognition topology remains open; this result only discharges the numerical lepton evaluation under the forced coefficients.
No downstream theorems currently depend on it (used_by is empty), so it functions as a verified checkpoint rather than an intermediate lemma in a longer chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.