downQuarkEta
plain-language theorem explainer
Defines the down-quark sub-leading correction parameter η by feeding the mixed-scheme PDG gen-12 and gen-23 residuals into the closed-form eta-from-data formula at ladder steps 6 and 8. Numerically this is the reported −0.88 value. Anyone checking Item-8 quark residual closure or comparing sector η values would cite it. The body is a direct application of the eta-from-data constructor.
Claim. The down-quark correction parameter is $\eta_{d} := \eta_{\mathrm{data}}(r_{12}^{d}, r_{23}^{d}; 6, 8)$, where $r_{12}^{d}$ and $r_{23}^{d}$ are the mixed-scheme PDG generation residuals for the down sector and the closed form is $\eta = (g_{12}s_{12}+g_{23}s_{23})/(\ln(s_{12}/s_{23})\cdot(g_{12}s_{12}-g_{23}s_{23}))$. Its numerical value is approximately $-0.88$.
background
Item 8 of the Recognition Science verification program concerns the sub-leading mass correction that sits on top of the leading $\varphi$-ladder yardstick formula. The module builds a minimal precise framework so that the open quark residual item becomes a falsifiable, sector-uniform statement rather than an ad-hoc fit.
The key device is the closed-form $\eta$ extractor etaFromData: given a residual pair and two distinct ladder steps, it returns
$\eta = (g_{12}s_{12}+g_{23}s_{23})/(\ln(s_{12}/s_{23})\cdot(g_{12}s_{12}-g_{23}s_{23}))$.
Algebraic identities then recover $1\pm\eta L$ as normalized residual combinations, so a single $\eta$ absorbs the consistency violation forced by the rigid sign-split family.
Down quarks are treated in a mixed renormalization scheme (unlike leptons, whose pole masses give a clean negative-sector test). The inputs here are the down-sector gen-12 and gen-23 residuals together with steps 6 and 8 on the $\varphi$-ladder.
proof idea
Pure definition: one application of the closed-form constructor etaFromData to the down-quark residual pair and the fixed steps 6 and 8. No tactics, no uniqueness argument, no solvability proof. The numerical content (−0.88) is whatever that formula evaluates to on the mixed-scheme PDG residuals.
why it matters
Item 8 asks for a unified sub-leading correction across sectors. This constant pins the down-quark $\eta$ that any refined-family or sign-class closure for the down signature must match. Sibling objects (downQuarkSignature, predictedResiduals, refined_neg_sector_closure, lepton and up-quark analogues) use the same $\eta$-from-data pattern so that sector comparisons are apples-to-apples.
In the broader RS picture the leading masses sit on the $\varphi$-ladder (yardstick $\cdot\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$); $\eta$ is the residual knob that makes the two-generation ratios consistent once the rigid sign-split identity $g_{12}s_{12}+g_{23}s_{23}=0$ is violated by data. The module already proves $\exists!$ closure for generic negative sectors and for concrete leptons; the down-quark $\eta$ is the corresponding numerical target for the quark side of that program.
No downstream theorem currently depends on this def (used-by is empty), so it functions as a named constant for residual tables and future closure proofs rather than as a proved claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.