RatioFamilyCoeffs
plain-language theorem explainer
Packages the two real scalars (c_neg, c_pos) that parameterize the smallest sign-split ratio family for sub-leading mass residuals. Anyone working Item 8 closure, quark residual fits, or the all-sector out-of-sample lepton test cites this carrier. It is a bare two-field structure with no proof content.
Claim. A coefficient pair $(c_{-}, c_{+}) \in \mathbb{R}^{2}$ for the sign-split residual family: $c_{-}$ multiplies corrections on sectors with negative $B$-power sign, and $c_{+}$ multiplies those with positive sign.
background
Item 8 is the open quark sub-leading mass correction in the Recognition mass ladder. The module builds the smallest closed-form candidate that could fix both up- and down-quark residual pairs with shared global coefficients, then freeze those coefficients for later out-of-sample tests (leptons, etc.).
Sector geometry supplies an integer $B$-power per sector (cube edge counting): leptons $-22$, up quarks $-1$, down quarks $23$, electroweak $+1$. Only the sign of that power enters the candidate family, selecting one of two global scalars.
A residual signature carries that sign, an ordered SDGT step pair (e.g. lepton $(11,6)$), and a coupling $\kappa$. The family then predicts the gen-$1\to 2$ and gen-$2\to 3$ residual corrections from a single active coefficient.
proof idea
No proof: a two-field structure definition. Fields are real scalars cNeg and cPos. Downstream ratioFamily pattern-matches the signature sign and picks one field as the active coefficient $c$; gen-$1\to 2$ inherits the sign of $c$ and gen-$2\to 3$ inherits $-c$.
why it matters
This is the parameter space for the Item 8 closure target. The proposition item8ClosureTarget asserts unique existence of such a pair matching exact up- and down-quark residuals. Freezing $(c_{-},c_{+})$ turns every later sector into an out-of-sample test: allSectorTest asks whether the same $c_{-}$ (shared by up quarks and leptons under negative $B$-power) reproduces observed lepton residuals under the lepton signature $(11,6)$.
Structural rigidity is immediate: consistency_of_ratioFamily forces any predicted residual pair to obey the cross-product identity $g_{12}s_{12}+g_{23}s_{23}=0$, and consistency_necessary is the contrapositive against data. The module later refines the family with an $\eta$ tilt when PDG data violate that identity; the two-coefficient carrier remains the baseline against which refined solvability and uniqueness are measured.
In the broader RS chain this sits under the mass formula (yardstick $\cdot\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$) as the candidate for universal sub-leading corrections once the $\varphi$-ladder and sector $B$-powers are fixed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.