downGen12Residual
plain-language theorem explainer
Defines the down-quark generation-1–2 residual as the φ-ladder rung residual of the PDG strange-to-down mass ratio at integer step 6. Anyone assembling the down residual pair or extracting the mixed-scheme η cites this constant. It is a one-line specialization of the rung-residual formula to fixed PDG inputs.
Claim. The down-sector generation-1–2 residual is $\log_\varphi(m_s^{\mathrm{PDG}}/m_d^{\mathrm{PDG}})-6$, where $m_d^{\mathrm{PDG}}=4.67$ and $m_s^{\mathrm{PDG}}=93.4$ (MeV-scale PDG inputs as used in the module).
background
Item 8 concerns the unified sub-leading mass correction on the Recognition Science φ-ladder. Masses sit near integer rungs; the residual is the fractional excess of the observed log-ratio over that integer step, measured in rung units.
The rung residual of a positive ratio at step $n$ is $\log_\varphi(\mathrm{ratio})-n=\ln(\mathrm{ratio})/\ln\varphi-n$. Here the ratio is the PDG strange-to-down mass quotient and the step is 6, the generation-1–2 spacing used for the down sector in this closure target.
The module builds residual pairs (gen12, gen23) per sector so that refined-family coefficients $(c,\eta)$ can be solved uniquely when the data satisfy the nondegeneracy hypotheses.
proof idea
Pure definition: apply the rung-residual map to the quotient of the fixed PDG strange and down mass constants with integer step 6. No proof obligations beyond the noncomputable real arithmetic of $\log$ and $\varphi$.
why it matters
Supplies the gen12 coordinate of the exact down residual pair, which the module quotes as roughly $+0.23$ rungs, and is the first argument to the down-quark η extractor (reported near $-0.88$ from mixed-scheme PDG). Those objects feed the refined-family solvability and uniqueness path that would close Item 8 for the down sector and make the all-sector generalization falsifiable. Ties the PDG mass ladder to the φ-rung bookkeeping used throughout the mass formula (yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}}$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.