up_generation_spacing
The theorem asserts that the rung integers assigned to up-type quarks satisfy the differences r_up(c) minus r_up(u) equals 11 and r_up(t) minus r_up(u) equals 17. Researchers verifying Recognition Science mass ladders against PDG data would cite this to confirm the generation structure on the phi-ladder. The proof reduces the claim to arithmetic by unfolding the rung definitions and applying an omega solver.
claimLet $r_ {up}(q)$ denote the phi-ladder rung integer assigned to up-type quark $q$. Then $r_{up}(c) - r_{up}(u) = 11$ and $r_{up}(t) - r_{up}(u) = 17$.
background
In the Recognition Science mass formula, quarks sit on a phi-ladder with rung integers drawn from the Anchor module. For the up sector (B_pow = -1, r0 = 35) the assignments are u at rung 4, c at rung 15, and t at rung 21. The abbreviation r_up extracts these integers while E_passive supplies the passive edge count 11 for D = 3. Upstream constants active_edges_per_tick, cube_edges, passive_field_edges, and wallpaper_groups = 17 enter the normalization of the mass anchors and alpha derivations.
proof idea
The proof is a term-mode simplification that unfolds r_up, tau, E_passive, passive_field_edges, cube_edges, active_edges_per_tick, D, and wallpaper_groups, after which omega decides the resulting integer arithmetic.
why it matters in Recognition Science
This spacing result is used directly in the construction of QuarkVerificationCert inside quark_verification_cert_exists, which bundles rung spacings with sector parameters to certify the full set of quark mass predictions. It closes the verification step for the up-generation ladder, consistent with the phi-ladder and eight-tick octave structure. The sibling theorem down_generation_spacing performs the analogous check for the down sector.
scope and limits
- Does not derive the rung integers from the forcing chain T0-T8.
- Does not compute numerical mass values or compare them to PDG data.
- Does not address the down-quark sector spacings.
- Assumes the specific rung assignments supplied by the Anchor module.
Lean usage
theorem cert_exists : Nonempty QuarkVerificationCert := ⟨{ rung_spacing_up := up_generation_spacing, rung_spacing_down := down_generation_spacing, sector_params_up := upquark_sector_params, sector_params_down := downquark_sector_params, all_masses_positive := quark_mass_positive }⟩formal statement (Lean)
107theorem up_generation_spacing :
108 r_up "c" - r_up "u" = 11 ∧ r_up "t" - r_up "u" = 17 := by
proof body
Term-mode proof.
109 simp only [r_up, tau, Anchor.E_passive, Anchor.W, passive_field_edges,
110 cube_edges, active_edges_per_tick, D, wallpaper_groups]
111 omega
112