top_charm_ratio_bounds
plain-language theorem explainer
Recognition Science assigns the top-to-charm quark mass ratio m_t/m_c to the rung difference 21-15 on the phi-ladder, yielding the exact claim 17 < φ^6 < 18. Quark-mass phenomenologists comparing RS predictions to PDG values would cite this bound. The proof is a one-line term reference to the already-established phi_pow_6_bounds theorem.
Claim. $17 < φ^6 < 18$, where $φ = (1 + √5)/2$ and the exponent 6 is the rung difference 21-15 for the top and charm quarks.
background
The module supplies machine-checked interval bounds for every RS mass prediction expressed on the phi-ladder. Each bound is an algebraic theorem proved from the identity φ² = φ + 1 and rational arithmetic; no floating-point evaluation appears. The local setting is the table of RS-native predictions that includes φ^6 ∈ (17,18) for the generation mass ratio, here specialized to m_t/m_c. Upstream, phi_pow_6_bounds records the Fibonacci reduction φ^6 = 8φ + 5 together with the elementary bounds 1.5 < φ < 1.62.
proof idea
The declaration is a one-line wrapper that applies phi_pow_6_bounds.
why it matters
The result closes one cell in the machine-verified numerical-predictions table of the Masses module. It supplies the concrete interval that Recognition Science claims for the top/charm ratio and therefore feeds any downstream comparison of the phi-ladder against experimental quark spectra. The bound rests on the self-similar fixed-point property of φ (T6) and the eight-tick octave structure that fixes the rung spacing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.