downAnchorCPosFromGen23
plain-language theorem explainer
Defines the positive-sector coefficient induced by the down-quark generation-2–3 residual under lepton-anchored transport. Citation target for anyone checking whether gen-1–2 and gen-2–3 anchors force a single consistent c₊. Pure closed-form arithmetic: residual times (6+8) over α_s·6·(1−η_ℓ log(6/8)), with a global minus sign.
Claim. The down-sector positive coefficient inferred from the generation-2–3 residual is $$c_{+}^{\mathrm{down}}(2\!\to\!3) = -\frac{R^{\mathrm{down}}_{23}\,(6+8)}{\alpha_s\,\cdot\,6\,\cdot\,(1-\eta_\ell\,\log(6/8))},$$ with $R^{\mathrm{down}}_{23}$ the transported down residual, $\alpha_s$ the strong coupling, and $\eta_\ell$ the lepton-sector $\eta$.
background
Module Item8ClosureTarget builds the smallest precise theorem layer that would close the open quark sub-leading correction (Item 8) and make the all-sector generalization falsifiable. The refined residual family introduces sector coefficients $(c,\eta)$ (and a positive-sector $c_{+}$ when the signature is positive) so that generation steps $s_{12},s_{23}$ and couplings $g_{12},g_{23}$ match observed mass residuals.
For the lepton-anchored strategy, lepton $\eta$ is frozen from the lepton sector and residuals are transported to the quark anchor scale. The down sector is positive-signature, so both generation legs induce a candidate $c_{+}$. Consistency of those two candidates is the second conjunct of the anchor-scale falsification target.
The numerical factors 6 and 8 are the generation step sizes appearing in the ratio-family denominators; $\alpha_s$ is the strong coupling from the running-couplings import; the log term is the same $\eta L$ structure that appears in the closed-form $\eta$ identities of the module summary.
proof idea
Definitional, not a proof. The body is a single noncomputable real expression: negate the product of the gen-2–3 down residual with $(6+8)$, then divide by $\alpha_s\cdot 6\cdot(1-\eta_\ell\log(6/8))$. No lemmas are applied; the formula is the explicit inversion of the refined-family positive-sector map at the lepton-anchored $\eta$ and the gen-2–3 step.
why it matters
Feeds leptonAnchoredAnchorTest, the concrete anchor-scale lepton-anchored falsification target: the up prediction must match transported anchor residuals, and the down sector must induce a single consistent $c_{+}$. Equality of this value with its gen-1–2 twin is exactly that second conjunct.
In the Item 8 program this is the numerical witness that the refined family, after lepton $\eta$ freeze-in, does not overconstrain the down positive sector. If the two induced $c_{+}$ disagree, the lepton-anchored closure path fails on PDG data. The construction sits inside the sub-leading mass-formula layer (phi-ladder yardstick corrections), not the T0–T8 forcing chain itself, but it is the operational check that makes the quark residual item falsifiable rather than merely fitted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.