allSectorTest
plain-language theorem explainer
Defines the all-sector verification proposition: a single coefficient triple for the log-asymmetry residual family must match the exact up-quark, down-quark, and observed lepton residual pairs at once. Quark data freeze the shared negative-sign coefficient; leptons then supply an out-of-sample check under a free lepton coupling κ. Anyone closing Item 8 or testing cross-sector universality of the sub-leading mass law would cite this Prop. The body is a pure existential conjunction over predicted residuals, not a proved theorem.
Claim. For a real lepton coupling $\kappa_{\mathrm{lep}}$, the all-sector test holds if there exist ratio-family coefficients such that the predicted residual pair on the up-quark signature at $\alpha_s=2/17$ equals the exact up residuals, the predicted pair on the down-quark signature at the same $\alpha_s$ equals the exact down residuals, and the predicted pair on the lepton signature at $\kappa_{\mathrm{lep}}$ equals the observed lepton residuals.
background
Item 8 concerns the sub-leading correction to sector mass ratios on the $\varphi$-ladder: after the integer SDGT rung steps, a residual pair (gen12, gen23) remains in rung units. The module builds a precise target for a unified log-asymmetry ratio family that absorbs those residuals with a small coefficient set and a universal $\eta$.
Signatures package each sector's rung spacings and sign class of $B_{\mathrm{pow}}$ (negative or positive). Up and down quarks use the RS strong coupling $\alpha_s=2/17$; leptons use a free $\kappa_{\mathrm{lep}}$, with leading candidate $1/(4\pi\cdot 11)$ from the electromagnetic seed. Predicted residuals map coefficients and a signature to a residual pair; exact and observed pairs are the PDG-derived targets (down approx. $+0.23$, $-0.10$; leptons approx. $+0.08$, $-0.13$).
Leptons share the negative sign class with up quarks, so the negative-side coefficient is already fixed once quarks close. Reproducing lepton residuals with that same coefficient is therefore a genuine cross-sector test, not a refit.
proof idea
No proof: this is a definition of a proposition. The body is an existential over RatioFamilyCoeffs whose three conjuncts equate predictedResiduals on the up-quark signature at alphaStrong, the down-quark signature at alphaStrong, and the lepton signature at the free kappaLepton to upExact, downExact, and leptonObserved respectively. Downstream work would discharge or refute the Prop by constructing or ruling out such coefficients.
why it matters
Closes the narrative arc of the Item 8 module: after per-sector solvability and uniqueness for the refined family, and after quark-only refined closure with $\kappa=\alpha_s=2/17$ and a single $\eta$, this Prop asks whether those quark-frozen coefficients also hit the lepton residuals. That is the falsifiable all-sector generalization the module summary advertises.
In Recognition Science terms it tests whether the sub-leading mass correction is universal across sign classes and gauge sectors on the $\varphi$-ladder, with couplings fixed by RS fractions rather than free fits. The doc stresses overdetermination: coefficients locked by quarks must still match leptons. No downstream theorems yet depend on it (used_by is empty); it is the named target for a future closure theorem or a concrete counterexample against PDG residual data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.