downExact
plain-language theorem explainer
Packages the exact down-quark sub-leading residual pair from PDG mass ratios against the φ-ladder SDGT steps: generation 1→2 residual ≈ +0.23 rungs and 2→3 residual ≈ −0.10 rungs. Anyone citing Item 8 quark closure or all-sector residual tests needs this datum. The definition is a two-field structure assembly of the precomputed gen12 and gen23 residuals.
Claim. The exact down-quark residual pair is the pair of real numbers $(r_{12}, r_{23})$ where $r_{12}$ is the rung residual of the PDG strange-to-down mass ratio against a 6-rung $\varphi$-ladder step, and $r_{23}$ is the rung residual of the PDG bottom-to-strange mass ratio against an 8-rung step. Numerically $r_{12}\approx +0.23$ and $r_{23}\approx -0.10$.
background
Item 8 of the Recognition Science verification program concerns sub-leading mass corrections on the $\varphi$-ladder. Masses are predicted as yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$; residuals measure how far PDG mass ratios sit from pure integer-rung steps.
A residual pair is simply two real corrections: one for generation $1\to 2$ and one for $2\to 3$. For down quarks the inputs are the PDG ratios $m_s/m_d$ (tested at step 6) and $m_b/m_s$ (tested at step 8). The module builds the smallest precise target that would close Item 8 by fitting both quark sectors inside one closed coefficient family, then treating leptons as out-of-sample.
Upstream, each component residual is already defined via rungResidual on the corresponding PDG ratio and step size. This definition only bundles those two numbers into the common ResidualPair carrier used by every sector test.
proof idea
No proof: pure structure construction. The gen12 field is set to the precomputed down-quark 1→2 residual (PDG strange/down vs 6-rung step). The gen23 field is set to the precomputed down-quark 2→3 residual (PDG bottom/strange vs 8-rung step). Noncomputable only because the residual arithmetic uses real division and logs.
why it matters
This is the down-quark half of the Item 8 closure target. Downstream, item8ClosureTarget and item8Specialized demand a unique coefficient pair whose predicted residuals match both upExact and this down pair at $\kappa=\alpha_s=2/17$. The refined variants (refinedItem8ClosureTarget, refinedItem8Specialized) do the same with a three-parameter log-asymmetry family and a universal $\eta$.
allSectorTest and refinedAllSectorTest freeze coefficients on the two quark residual pairs (including this one) and ask whether the same coefficients reproduce lepton residuals under the lepton signature—an out-of-sample falsification. Without a fixed down residual pair, the quark-side equations are not pinned and the all-sector test cannot run.
In the broader RS chain this sits under the mass formula on the $\varphi$-ladder (T6 forces $\varphi$), not under the forcing steps T0–T8 themselves. Closing Item 8 would convert quark sub-leading corrections from open scaffolding into a frozen, testable family.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.