r_down_values
plain-language theorem explainer
The declaration fixes the phi-ladder rung integers for the down-type quarks at 4 for the down quark, 15 for the strange quark, and 21 for the bottom quark. Workers verifying Recognition Science mass formulas against PDG data cite it to lock the down-quark sector parameters B_pow = 23 and r0 = -5. The proof reduces the conjunction by simplification over the rung definition and the imported constants from AlphaDerivation, then discharges the arithmetic via omega.
Claim. $r_ {down}(d) = 4$, $r_{down}(s) = 15$, and $r_{down}(b) = 21$.
background
The QuarkVerification module supplies machine-checked rung integers that enter the down-quark mass formula 2^{23} phi^{-10+r}/10^6 MeV. The rung function r_down is defined in the Anchor module using the sector constants B_pow and r0 together with the normalization factors E_passive and W. Upstream constants include active_edges_per_tick = 1, cube_edges(d) = d * 2^{d-1}, passive_field_edges(d) = cube_edges(d) - 1, and wallpaper_groups = 17; the last three appear in the alpha normalization and the overall scale factor.
proof idea
The term proof invokes simp only on the definition of r_down together with tau, Anchor.E_passive, Anchor.W, passive_field_edges, cube_edges, active_edges_per_tick, D, and wallpaper_groups, then applies the omega tactic to resolve the resulting integer equalities.
why it matters
The result supplies the three rung values required by the down-quark mass predictions in the same module. It parallels the up-quark sector verification and anchors the phi-ladder mass formula yardstick * phi^{rung-8+gap(Z)} for D = 3. No downstream theorems yet depend on it; the declaration closes the explicit rung list for the down sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.