refinedAllSectorTest
plain-language theorem explainer
Defines the all-sector falsification proposition: three refined-family coefficients, fixed by up- and down-quark residual data, must also reproduce the lepton residuals (six equations, three unknowns). Anyone auditing Item 8 closure or the unified sub-leading mass formula cites this Prop as the target statement. The body is a pure existential definition over RefinedCoeffs, not a proved theorem.
Claim. For a real lepton coupling $\kappa_\ell$, the refined all-sector test holds when there exist refined coefficients such that the refined residual prediction on the up-quark signature (at $\alpha_s$) equals the exact up residual, the same coefficients on the down-quark signature equal the exact down residual, and on the lepton signature (at $\kappa_\ell$) equal the observed lepton residual.
background
Item 8 in the Recognition Science mass program is the open quark sub-leading correction. This module builds the smallest precise theorem layer that would close that item and make an all-sector generalization falsifiable. The refined family augments the sign-split ratio family by a single $\eta$ correction per sector, with closed-form $\eta$ from PDG residuals and SDGT steps via etaFromData.
Sector signatures package generation steps and residual pairs. Quark signatures use the strong coupling; the lepton signature takes a free $\kappa_\ell$. Refined coefficients are the three free parameters of the refined prediction map. Upstream work already gives per-sector solvability and uniqueness ($\exists!$ of $(c,\eta)$ for each sign class) and shows the bare sign-split family is structurally rigid in a way PDG data violates, so the $\eta$ term is forced.
The local setting is verification of a unified sub-leading mass formula on the $\phi$-ladder mass residuals, not a derivation of the leading rung formula itself.
proof idea
No proof: this is a definition of a Prop. The body is a single existential quantifier over RefinedCoeffs conjoined with three equalities of refinedPrediction against the fixed targets upExact, downExact, and leptonObserved on the three sector signatures. Instantiating or discharging the Prop is left to later theorems; the definition only packages the joint matching condition.
why it matters
Doc-comment calls this the strongest available falsification target for Item 8: coefficients frozen on quark data must also hit lepton residuals. That is the all-sector closure statement the module is built to make precise. Sibling results already give per-sector $\exists!$ and the $\eta$ closed form; this Prop lifts those to a single three-coefficient, three-sector claim (six residual equations). It sits at the end of the Item 8 closure ladder rather than feeding a named parent theorem yet (used_by is empty). In framework terms it tests whether the sub-leading correction on the $\phi$-ladder mass formula is universal across lepton and quark sectors, not merely a per-sector fit. Open question: whether a concrete $\kappa_\ell$ and coefficient triple make the Prop true against PDG inputs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.