signClassAllSectorTarget
plain-language theorem explainer
Existence of one four-parameter sign-class coefficient set that simultaneously matches residual pairs in the up-quark, down-quark, and lepton sectors. Auditors of Item 8 all-sector closure cite this as the full six-equation target (four unknowns plus free lepton coupling). The body is a pure existential Prop over those coefficients; no proof is attached.
Claim. For a free lepton coupling $\kappa_{\mathrm{lep}}\in\mathbb{R}$, there exist four real coefficients $(c_{-},\eta_{-},c_{+},\eta_{+})$ such that the sign-class family, evaluated on the up-quark residual signature at $\alpha_s=2/17$, the down-quark residual signature at the same $\alpha_s$, and the lepton residual signature at coupling $\kappa_{\mathrm{lep}}$, equals the exact up, exact down, and observed lepton residual pairs respectively.
background
Item 8 concerns the unified sub-leading mass correction on the $\varphi$-ladder: after the integer SDGT rung steps, residual pairs $(r_{12},r_{23})$ measure $\log_\varphi$ of observed mass ratios minus those steps, in rung units. The module builds the smallest precise target that would close quark sub-leading corrections and make the all-sector claim falsifiable.
A residual signature packages sign of $B_{\mathrm{pow}}$, generation steps, and a coupling. Leptons use the negative class with steps $(11,6)$; down quarks the positive class with $(6,8)$; up quarks the matching positive-class signature. Couplings for quarks are fixed to the RS strong value $\alpha_s=2/17$; the lepton coupling $\kappa_{\mathrm{lep}}$ stays free.
Sign-class coefficients are four globals: amplitude and log-asymmetry for each $B_{\mathrm{pow}}$ sign. The sign-class family maps those coefficients and a signature to a predicted residual pair. Exact up/down and observed lepton pairs are the numerical targets (PDG-derived rung residuals).
proof idea
Not a proved theorem: a def whose body is a Prop. It asserts existence of a SignClassCoeffs record such that three equalities hold in parallel: sign-class family on the up signature at $\alpha_s$ equals the exact up residual pair; same family on the down signature equals the exact down pair; same family on the lepton signature at $\kappa_{\mathrm{lep}}$ equals the observed lepton pair. No tactics or lemmas discharge the existential; downstream work must construct or refute the coefficients.
why it matters
This is the full all-sector closure target for Item 8: six residual equations (gen12 and gen23 across three sectors) against four shared coefficients plus one free lepton coupling. The module already proves per-sector refined-family uniqueness and solvability, sign-class collapse when the two $\eta$ values agree, and a structural rigidity obstruction for the simpler ratio family. Landing a proof (or disproof) of this Prop would decide whether independent $\eta$ per sign class unifies quarks and leptons under one sub-leading formula.
No downstream consumers are wired yet; the declaration sits at the end of the concrete-instantiation section as the named falsifiable claim. In the broader RS ladder picture it sits under mass residuals after the integer rung steps, not under the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.