top_to_up_ratio
The theorem shows that the RS up-sector mass ratio of the top quark to the up quark equals phi to the 17th power. Quark-mass modelers comparing phi-ladder predictions to PDG data would cite this when checking exponent differences for rungs 21 and 4. The proof reduces the ratio by unfolding the mass definition, substituting edge constants from AlphaDerivation, and simplifying the resulting phi exponents via field_simp and zpow arithmetic.
claimIn the up-quark sector the ratio of the top-quark mass to the up-quark mass satisfies $m_t / m_u = phi^{17}$, where each mass is given by $phi^{30+r}/(2 times 10^6)$ MeV with rung integers $r_t=21$ and $r_u=4$.
background
The QuarkVerification module supplies machine-checked comparisons of RS mass predictions against PDG values while treating experimental numbers as imported constants. For the up sector (B_pow = -1, r0 = 35) the mass formula simplifies to $m(UpQuark,r) = phi^{30+r}/(2 times 10^6)$ MeV. The rungs are fixed by Anchor: u at r=4, c at r=15, t at r=21. Upstream constants include phi from Constants, D=3, and the edge counts active_edges_per_tick=1, cube_edges=D*2^{D-1}, passive_field_edges=11, and wallpaper_groups=17 from AlphaDerivation.
proof idea
The term proof first applies simp to replace r_up, tau, Anchor.E_passive, Anchor.W and the AlphaDerivation edge definitions. It unfolds rs_mass_MeV, repeats the simp step, introduces phi positivity, invokes field_simp, rewrites with zpow_natCast and zpow_add_0, and finishes with congr.
why it matters in Recognition Science
The result confirms the exact exponent gap of 17 between the t and u rungs inside the up-sector mass formula, completing one verification step for the phi-ladder mass predictions. It sits inside the T5-T6 forcing chain that fixes phi as the self-similar fixed point and supports the D=3 spatial dimension used throughout the framework. No downstream theorems are recorded, yet the declaration contributes to the module's zero-sorry status for quark-sector checks.
scope and limits
- Does not derive the mass formula from the Recognition Composition Law.
- Does not incorporate PDG experimental uncertainties or error bars.
- Does not address down-quark sector ratios or mixed-generation comparisons.
- Does not compute absolute mass values, only their ratio.
formal statement (Lean)
141theorem top_to_up_ratio :
142 rs_mass_MeV .UpQuark (r_up "t") / rs_mass_MeV .UpQuark (r_up "u") =
143 Constants.phi ^ (17 : ℕ) := by
proof body
Term-mode proof.
144 simp only [r_up, tau, Anchor.E_passive, Anchor.W, passive_field_edges,
145 cube_edges, active_edges_per_tick, D, wallpaper_groups]
146 unfold rs_mass_MeV
147 simp only [B_pow, r0, Anchor.E_passive, Anchor.W, passive_field_edges,
148 cube_edges, active_edges_per_tick, D, wallpaper_groups, A]
149 have hphi := Constants.phi_pos
150 have hphi_ne : Constants.phi ≠ 0 := ne_of_gt hphi
151 field_simp
152 rw [← zpow_natCast, ← zpow_add₀ hphi_ne]
153 congr 1
154
155/-! ## Certificate -/
156