upQuarkEta
plain-language theorem explainer
Up-quark η from mixed-scheme PDG residuals, numerically about −2.72, inflated by the t/c pole versus MS-bar mismatch at m_c. Item-8 workers cite it as the sector η that feeds the refined sub-leading mass family for up-type quarks. The body is a one-line instantiation of the closed-form eta-from-data map on the charm/up and top/charm rung residuals with ladder steps 13 and 11.
Claim. Define the up-quark correction $\eta_{\mathrm{up}}\in\mathbb{R}$ by the closed-form residual map $\eta(g_{12},g_{23},s_{12},s_{23})=(g_{12}s_{12}+g_{23}s_{23})/(\ln(s_{12}/s_{23})\cdot(g_{12}s_{12}-g_{23}s_{23}))$ evaluated at the up-sector gen-1$\to$2 and gen-2$\to$3 rung residuals $g_{12}=R(m_c^{\mathrm{PDG}}/m_u^{\mathrm{PDG}},13)$, $g_{23}=R(m_t^{\mathrm{PDG}}/m_c^{\mathrm{PDG}},11)$ with steps $s_{12}=13$, $s_{23}=11$.
background
Item 8 is the open quark sub-leading mass correction in the Recognition mass ladder. The module builds the smallest precise framework that would close it: a refined two-generation residual family with a single log-asymmetry parameter η that absorbs the consistency violation of the pure sign-split family.
The closed-form map etaFromData is $\eta=(g_{12}s_{12}+g_{23}s_{23})/(\ln(s_{12}/s_{23})\cdot(g_{12}s_{12}-g_{23}s_{23}))$, well-defined when the steps differ and the weighted residuals are non-degenerate. Upstream identities show $1+\eta L=2 g_{12}s_{12}/D$ and $1-\eta L=-2 g_{23}s_{23}/D$, so each generation equation closes algebraically once η is taken from the data.
For the up sector the inputs are the rung residuals of the PDG charm/up and top/charm ratios at ladder steps 13 and 11. The doc notes the numerical value is inflated by the mixed-scheme t/c comparison (pole mass versus $\overline{\mathrm{MS}}$ at $m_c$).
proof idea
Pure definitional wrapper. The body applies etaFromData to upGen12Residual, upGen23Residual, and the fixed steps 13 and 11. No tactics, no lemmas beyond the residual defs themselves: $g_{12}$ is the rung residual of $m_c^{\mathrm{PDG}}/m_u^{\mathrm{PDG}}$ at step 13, and $g_{23}$ is the rung residual of $m_t^{\mathrm{PDG}}/m_c^{\mathrm{PDG}}$ at step 11.
why it matters
Supplies the concrete up-sector η that the Item-8 refined family needs before existence/uniqueness theorems (refinedFamily_neg_solvable, refined_neg_sector_closure, and the sign-class collapse) can be specialized to real PDG numbers. Together with the sibling lepton and down-quark η defs it makes the all-sector generalization numerically falsifiable against mixed-scheme mass tables.
In the broader RS picture this sits under the phi-ladder mass formula (yardstick times $\phi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$): η is the sub-leading correction that the bare rung count does not capture. The module summary flags the sign-split consistency obstruction that PDG data violate; this definition is the data-side half of the fix. No downstream uses are wired yet in the graph, so it is presently a named constant waiting on sector-closure applications.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.