leptonAnchoredTarget
plain-language theorem explainer
Lepton-anchored closure is the proposition that one refined coefficient set fits lepton residuals at coupling κ_lep and simultaneously recovers the anchor-scale up- and down-quark residual pairs. Item-8 auditors cite it as the precise all-sector target for the sub-leading φ-ladder correction. It is a pure definition of an existential Prop; no proof content.
Claim. For a lepton coupling $\kappa_{\mathrm{lep}}\in\mathbb{R}$ and given anchor residual pairs $(r^{u}_{12},r^{u}_{23})$ and $(r^{d}_{12},r^{d}_{23})$, there exist refined coefficients such that the refined family matches the observed lepton residuals on the lepton signature at $\kappa_{\mathrm{lep}}$, and the same coefficients reproduce those anchor pairs on the up- and down-quark signatures at $\alpha_s=2/17$.
background
Item 8 of the Recognition verification stack concerns sub-leading corrections to the φ-ladder mass formula (yardstick times $\varphi$ to a rung offset). A residual is the rung-unit defect $\log_\varphi(\mathrm{observed\ ratio})-\mathrm{integer\ step}$. A residual pair packages the two generation steps $1\to 2$ and $2\to 3$.
This module supplies the smallest precise theorem framework that would close the open quark sub-leading item and make the all-sector generalization falsifiable. The plain sign-split ratio family is structurally rigid (gen12·s₁₂ + gen23·s₂₃ = 0), which PDG data violates; the refined family absorbs that obstruction via an η parameter with closed-form identities. Sector-wise solvability and uniqueness ($\exists!$) for refined coefficients are already proved.
The RS strong coupling is fixed at $\alpha_s=2/17$ (wallpaper-group fraction, within ~0.3σ of PDG). Anchor residual pairs are the out-of-sample quark targets once lepton-sector coefficients are frozen.
proof idea
Definitional packaging only: no tactics, no lemmas. The body is $\exists$ refined coefficients such that three equalities hold at once: refined prediction on the lepton signature at $\kappa_{\mathrm{lep}}$ equals the observed lepton residual pair; the same coefficients on the up-quark signature at $\alpha_s$ equal the supplied up-anchor pair; likewise for the down-quark signature and down-anchor pair.
why it matters
Names the lepton-anchored form of the Item 8 closure target: fit leptons (free $\kappa_{\mathrm{lep}}$), then demand the same global refined coefficients predict quark residuals at the anchor scale. That is the concrete falsifiable claim for unified sub-leading mass corrections across sectors.
The module already closes supporting pieces: consistency obstruction of the unrefined ratio family, closed-form η from data, constructive $\exists!$ per sign sector, and collapse of the sign-class family when the two η values agree. No downstream consumers are wired yet (used_by empty). Discharging this target would finish the open quark sub-leading item against the φ-ladder mass formula and the broader forcing-chain constants (φ from T6, eight-tick structure from T7).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.