leptonAnchoredAnchorTest
plain-language theorem explainer
Packages the lepton-anchored Item 8 falsification target as a single proposition: the up residual predicted from the lepton-derived coupling must equal the transported anchor-scale up residual, and the down sector must yield one common positive coefficient from both generation pairs. Mass-formula and verification authors cite it when stating what would close the quark sub-leading correction out of sample. It is a bare Prop definition (conjunction of two equalities), not a proved theorem.
Claim. The lepton-anchored anchor test is the proposition that (i) the up-quark residual predicted at the lepton candidate coupling equals the exact anchor-scale up residual, and (ii) the positive down-sector coefficient induced by the generation-1–2 residual pair equals that induced by the generation-2–3 pair.
background
Item 8 in the Recognition mass program is the open quark sub-leading correction. This module builds the smallest precise target that would close it and make the all-sector generalization falsifiable. The refined residual family introduces a shared tilt $\eta$ and sign-split coefficients so that generation pairs need not obey the rigid sign-split consistency identity that raw PDG data violate.
Leptons supply scheme-free residuals with small perturbative $\eta\approx 0.065$. The documented strategy is therefore: fix $\eta$ and the negative-sector coefficient from the two lepton equations (both generations share the negative $B$-power sign with up quarks); freeze that pair; predict up residuals at the anchor scale $\mu^*=182,\mathrm{GeV}$; and treat down quarks via an independent positive coefficient. An RG bridge (RunningCouplings) is meant to carry PDG quark masses to that scale so the comparison is scheme-consistent.
Under that reading, the present definition is the concrete anchor-scale checklist: up prediction must match the transported anchor residual, and the down sector must induce a single consistent positive coefficient across generation pairs.
proof idea
No proof: this is a noncomputable def of a Prop. The body is the conjunction of two equalities already named in the module (lepton-anchored up prediction at the lepton candidate coupling equals the exact anchor up residual; down positive coefficient from gen 1–2 equals that from gen 2–3). Downstream work would prove or refute the proposition, not unfold a tactic script here.
why it matters
Without a named falsification target, the lepton-anchored closure story stays narrative. This definition pins that target: quarks become genuine out-of-sample tests once $\eta$ and the negative coefficient are frozen on clean lepton data, matching the module’s stated resolution path for Item 8.
It sits beside the proved structural pieces already in the module (ratio-family consistency obstruction, closed-form $\eta$ from data, refined-family solvability and uniqueness per sign sector, full $\exists!$ for negative sectors). Those results justify that a refined family can fit a sector uniquely; this Prop states what must still hold at the anchor scale for the lepton-first strategy to close quarks.
In the broader RS ladder, masses sit on the $\varphi$-rung formula with sector gaps; sub-leading residuals and running couplings are the remaining verification layer. No downstream theorems yet depend on this symbol (used_by empty), so it is presently a named goal rather than an ingredient in a larger proved chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.