downGen23Residual
plain-language theorem explainer
Defines the generation-2–3 residual for the down-quark sector: the φ-ladder excess of the PDG bottom/strange mass ratio over an eight-rung step. Downstream residual pairs and η extractions cite it as the gen23 coordinate of the observed down signature. The body is a one-line specialization of the rung-residual formula to those PDG masses and step 8.
Claim. The down-sector generation-2–3 residual is $\log_\varphi(m_b^{\mathrm{PDG}}/m_s^{\mathrm{PDG}}) - 8$, with $m_b^{\mathrm{PDG}} = 4180$ and $m_s^{\mathrm{PDG}} = 93.4$ (MeV-scale PDG inputs).
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. Residuals are measured in φ-ladder rung units rather than raw mass ratios.
The rung residual of a positive ratio against an integer step is $\log_\varphi(\mathrm{ratio}) - \mathrm{step}$, i.e. $\log(\mathrm{ratio})/\log\varphi$ minus the step. It isolates the sub-leading correction once the leading integer rung jump is subtracted. Here the ratio is the PDG bottom over strange mass, and the step is 8 (the gen23 SDGT step used for the down family).
Sibling constants fix the PDG inputs: bottom at 4180 and strange at 93.4. The companion gen12 residual uses the analogous strange/down ratio against step 6; together they form the observed down residual pair.
proof idea
Pure definitional specialization: apply rungResidual to the quotient pdg_bottom / pdg_strange with natural step 8. No lemmas, tactics, or algebraic rewriting; the value is the real number that formula returns.
why it matters
Feeds the exact down residual pair (downExact), whose gen23 field is this residual (doc: approximate values gen12 ≈ +0.23, gen23 ≈ −0.10 rungs). That pair is the data input for down-quark η via etaFromData on steps 6 and 8 (downQuarkEta, reported ≈ −0.88 under the mixed PDG scheme).
In the Item 8 program, these numerical residuals are the observed signature against which refined-family solvability and uniqueness (∃! (c, η) per sector) are checked. The mass formula sits on the φ-ladder (yardstick · φ^(rung−8+gap(Z))); this residual is precisely the fractional rung defect that the sub-leading η correction is meant to absorb. Closing Item 8 for down quarks depends on treating this coordinate as fixed PDG-derived data inside the refined family.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.