charm_up_ratio_bounds
Recognition Science assigns the charm to up quark mass ratio as phi to the eleventh power and proves the inequality 198 < phi^11 < 200. Quark mass modelers would cite this bound when checking the predicted ratio of approximately 199 against data. The proof is a one-line wrapper that directly invokes the phi_pow_11_bounds theorem.
claim$198 < phi^{11} < 200$, where $phi = (1 + sqrt(5))/2$ is the golden ratio and the exponent 11 encodes the rung difference for the charm and up quarks on the phi-ladder.
background
Recognition Science places particle masses on a phi-ladder whose ratios are integer powers of the golden ratio phi satisfying phi^2 = phi + 1. The NumericalPredictions module collects formally proved bounds on these ratios, including phi^6 for the bottom/strange ratio, phi^7 for the neutrino mass-squared ratio, and phi^11 for the charm/up ratio. The local setting is given by the module statement that every listed interval is a Lean theorem proved from algebraic identities alone, with no floating-point evaluation. This declaration depends on the upstream theorem phi_pow_11_bounds, which states the same inequality and is proved by rewriting to phi_pow_11_eq followed by linarith on the bounds phi > 1.618 and phi < 1.62.
proof idea
The proof is a one-line wrapper that directly invokes the phi_pow_11_bounds theorem.
why it matters in Recognition Science
The result supplies the phi^11 entry in the module's table of machine-verified predictions, confirming the mass ratio m_c/m_u ≈ 199. It supports the general mass formula yardstick * phi^(rung - 8 + gap(Z)) and the forcing chain landmarks T5 (J-uniqueness) and T6 (phi as self-similar fixed point). No downstream uses appear in the module and no open questions are addressed.
scope and limits
- Does not derive the rung assignments 15 and 4 for charm and up quarks.
- Does not prove the mass formula itself.
- Does not incorporate experimental error bars beyond the stated interval.
- Does not extend the bound to other quark families or leptons.
formal statement (Lean)
147theorem charm_up_ratio_bounds :
148 (198 : ℝ) < phi ^ 11 ∧ phi ^ 11 < (200 : ℝ) := phi_pow_11_bounds
proof body
Term-mode proof.
149
150/-- The bottom/strange mass ratio: m_b/m_s = φ^(21-15) = φ⁶ ≈ 17.9. -/