rungResidual
plain-language theorem explainer
Defines the rung-unit residual of an observed positive mass (or coupling) ratio against an integer ladder step: log base φ of the ratio, minus that step. Anyone fitting sub-leading mass corrections in the Item 8 closure cites it as the raw residual coordinate. The body is a one-line change-of-base formula, not a theorem.
Claim. For a positive real ratio $r$ and a natural number step $n$, the rung residual is $\log_\varphi(r) - n$, equivalently $\frac{\ln r}{\ln \varphi} - n$. It is the excess (or deficit) of the observed ratio relative to a pure $\varphi^n$ jump on the $\varphi$-ladder, measured in rung units.
background
Item 8 Closure Target builds the smallest precise theorem layer that would close the open quark sub-leading mass correction and make the all-sector generalization falsifiable. Masses in Recognition Science sit on a $\varphi$-ladder: ratios of successive generation masses are expected to be near integer powers of the golden ratio $\varphi$, the self-similar fixed point forced at T6.
The integer $n$ is the nominal generation step (e.g. 6 and 8 for down-sector gen12/gen23, 13 and 11 for up-sector anchors). Any mismatch between the observed ratio and $\varphi^n$ is a sub-leading correction. Measuring that mismatch in rung units means taking the base-$\varphi$ logarithm and subtracting $n$, so a pure ladder jump has residual zero and a fractional rung shift appears as a small real number.
Downstream residual defs feed PDG mass ratios and anchor-scale transported masses into this coordinate; the refined residual family then solves for sector coefficients $(c,\eta)$ against those numbers.
proof idea
Pure definition, not a proof. The body is the change-of-base identity $\log_\varphi r = \ln r / \ln \varphi$, minus the coerced natural step. No lemmas are applied; Constants.phi supplies the ladder base.
why it matters
This is the primitive residual coordinate for the entire Item 8 residual stack. Every sector residual in the module is a thin wrapper: downGen12Residual, downGen23Residual, the lepton gen12 residual and its positivity lemma, and the four anchor-scale up/down residuals all call it on a concrete mass ratio and step.
Those residuals are the data side of the refined family whose solvability and uniqueness (refinedFamily_neg_solvable / _unique, refined_neg_sector_closure) give $\exists!$ sector coefficients. Closing Item 8 means matching sub-leading mass corrections on the $\varphi$-ladder (mass formula yardstick $\cdot \varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$); without a uniform rung-unit residual there is no common currency between PDG ratios, anchor transport, and the sign-split / refined families. The module's proved rigidity (consistency_of_ratioFamily) and $\eta$-from-data identities act on exactly these numbers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.