ratioFamily
plain-language theorem explainer
Maps two global coefficients and a sector residual signature to a pair of generation-step mass corrections. Sign of B_pow picks cNeg or cPos; SDGT step fractions weight the split; one coupling multiplies both. Item-8 workers cite it as the smallest closed-form candidate family for quark (and lepton) sub-leading residuals. Body is pure match-and-arithmetic, not a derived theorem.
Claim. Given coefficients $(c_{-},c_{+})$ and a residual signature with sign bit $s$, positive integer steps $s_{12},s_{23}$, and coupling $\kappa$, set $c:=c_{-}$ if $s$ is negative and $c:=c_{+}$ if positive, and $T:=s_{12}+s_{23}$. The ratio family returns the residual pair $\delta_{12}=c\,\kappa\,s_{23}/T$ and $\delta_{23}=-c\,\kappa\,s_{12}/T$.
background
Module Item8ClosureTarget builds the smallest precise theorem framework that would close the open quark sub-leading correction (Item 8) and make the all-sector generalization falsifiable. The objects here are residual signatures and residual pairs: a signature packages the B_pow sign class, the two SDGT rung spacings (cube-cell counts from the Q₃ decomposition) for generations 1→2 and 2→3, and one coupling scalar; a residual pair is simply the two real corrections $(\delta_{12},\delta_{23})$.
Ratio-family coefficients are the two globals $(c_{-},c_{+})$ allowed by the smallest sign-split candidate. The design intent, from the doc-comment, is to use only sign selection, ordered step fractions, and one coupling, so that $\delta_{12}$ inherits the sign of $c$ and $\delta_{23}$ inherits $-c$, matching the empirical pattern $\delta_{12}>0$, $\delta_{23}<0$ when $c>0$.
proof idea
Definition, not a proof. Match on the signature sign to pick $c_{-}$ or $c_{+}$; form the real total $T=s_{12}+s_{23}$; return the structure with gen12 equal to $c\cdot\kappa\cdot s_{23}/T$ and gen23 equal to the negative of $c\cdot\kappa\cdot s_{12}/T$. No lemmas are applied.
why it matters
Baseline closed-form candidate for Item 8 (unified sub-leading mass formula). Downstream, consistency_of_ratioFamily proves the structural rigidity $\delta_{12}s_{12}+\delta_{23}s_{23}=0$ for every coefficient set and signature; the module summary notes that PDG data violates this identity, which is why the refined $\eta$-family is introduced. predictedResiduals is the thin alias used as the exact prediction map. refined_at_eta_zero shows the refined family collapses exactly to this definition when $\eta=0$, so the ratio family is the $\eta\to 0$ limit of the solvable unique-coefficient family that later yields $\exists!$ sector closures.
In the Recognition mass picture (phi-ladder yardstick with rung and gap corrections), this is the candidate law for the generation-step residuals once the leading rung is fixed. Freezing $(c_{-},c_{+})$ here is what would turn later lepton, genetic, and theta instantiations into out-of-sample tests rather than free fits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.