downAnchorCPosFromGen12
plain-language theorem explainer
Defines the positive down-sector amplitude inferred from the gen-1–2 anchor residual after freezing the lepton η. Equality with the gen-2–3 twin is the one-parameter consistency check under lepton anchoring. Anyone auditing Item 8 lepton-anchored closure cites it. The body is a direct arithmetic formula from residual, rung steps, α_s, and lepton η.
Claim. The positive down-sector coefficient inferred from the generation-1–2 anchor residual is $$c_{+}^{\mathrm{down}}(12)=\frac{R_{12}^{\mathrm{down}}\,(6+8)}{\alpha_s\cdot 8\,(1+\eta_{\ell}\log(6/8))},$$ where $R_{12}^{\mathrm{down}}$ is the rung residual of the strange-to-down mass ratio at the anchor against step $6$, $\alpha_s=2/17$, and $\eta_{\ell}$ is the lepton-sector $\eta$ from pole-mass residuals.
background
Item 8 concerns the open quark sub-leading mass correction. This module builds the smallest precise target that would close it and make the all-sector generalization falsifiable. Residuals are rung-unit defects: $\log_\varphi$ of an observed mass ratio minus the integer ladder step. The refined family introduces amplitudes $c$ (signed) and a shared $\eta$ that absorbs the sign-split consistency violation forced by PDG data.
The strong coupling is the RS value $\alpha_s=2/17$ (wallpaper-group fraction), within $0.3\sigma$ of PDG $\alpha_s(M_Z)$. Lepton $\eta\approx +0.065$ is taken as the cleanest data point (no RG ambiguity). The down gen-1–2 residual is the rung residual of the strange-to-down anchor mass ratio against step $6$. Freezing lepton $\eta$ and transporting anchor residuals yields two candidate positive down amplitudes, one from each generation step.
proof idea
Definition, not a proof. Substitutes the three upstream quantities into the refined-family inversion for the positive coefficient on a gen-1–2 signature: numerator is residual times total step span $6+8$; denominator is $\alpha_s$ times the complementary step $8$ times the lepton-anchored factor $1+\eta_\ell\log(6/8)$. No tactics or lemmas beyond unfolding those defs.
why it matters
Feeds leptonAnchoredAnchorTest, the concrete anchor-scale falsification target: up prediction must match transported anchor residuals, and the down sector must induce a single consistent $c_+$. Equality of this gen-1–2 expression with its gen-2–3 twin is exactly that one-parameter down-sector consistency test under lepton anchoring.
In the broader RS picture this sits on the $\varphi$-ladder mass formula (yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$) and isolates the sub-leading correction Item 8 must close. If the two $c_+$ values disagree, lepton-anchored closure fails at the anchor scale; if they agree, the down sector collapses to a unique positive amplitude once $\eta$ is frozen from leptons.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.