down_generation_spacing
plain-language theorem explainer
The declaration proves that the rung spacing between strange and down quarks is 11 and between bottom and down is 17 in the down-type sector. Researchers verifying quark mass hierarchies against the phi-ladder would reference this when confirming generation ratios. The proof reduces the statement via simplification over rung definitions and edge-count constants, then discharges the arithmetic with the omega tactic.
Claim. Let $r_ {rm down}(q)$ be the rung index assigned to down-type quark flavor $q$ in the Recognition Science mass formula. Then $r_{rm down}(text{s}) - r_{rm down}(text{d}) = 11$ and $r_{rm down}(text{b}) - r_{rm down}(text{d}) = 17$.
background
In the Recognition Science framework, quark masses are determined by the formula involving powers of the golden ratio phi on a ladder indexed by integer rungs r, with sector-specific offsets. For the down-quark sector the base rung for the first generation is fixed at r=4, and subsequent generations follow from the structural constants of the theory. The relevant upstream constants are the number of passive field edges per tick, which equals 11 for three spatial dimensions, and the number of wallpaper groups, which is 17. These arise from the definitions cube_edges(d) = d * 2^(d-1) and passive_field_edges(d) = cube_edges(d) - 1, together with the crystallographic count of 17 wallpaper groups.
proof idea
The proof is a term-mode wrapper. It invokes simp only on the definitions of r_down, tau, Anchor.E_passive, Anchor.W, passive_field_edges, cube_edges, active_edges_per_tick, D and wallpaper_groups. This reduces the goal to two arithmetic statements on natural numbers, which the omega tactic then solves automatically.
why it matters
This theorem supplies the rung spacing data for the down sector that is assembled into the QuarkVerificationCert in the downstream result quark_verification_cert_exists. It thereby contributes to the machine-checked verification that the predicted mass ratios m(s)/m(d) = phi^11 and m(b)/m(d) = phi^17 are consistent with the Recognition Science forcing chain, specifically the T7 eight-tick octave and the D=3 spatial dimension that fixes the passive edge count at 11. The result is quarantined from absolute mass derivation, as experimental values remain imported constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.