mu_pred_lower
The theorem proves that the phi-ladder prediction for the proton-electron mass ratio exceeds 1898. Recognition Science mass modelers cite this lower bound when constructing the bracketed interval for the dimensionless ratio against CODATA data. The proof unfolds the ratio definition, applies the positivity lemma for the electron prediction to convert to a product inequality, bounds the product below 969 using the supplied mass intervals, and closes the chain with linarith.
claim$1898 < m_p^pred / m_e^pred$, where $m_e^pred = phi^{59}/4194304000000$ MeV lies in $(0.5098, 0.5102)$ and $m_p^pred = phi^{43}/1000000$ MeV lies in $(969, 970.4)$.
background
The module records proved interval bounds on the predicted proton-electron mass ratio in the phi-ladder framework of Recognition Science. The ratio is defined as proton_binding_pred divided by electron_pred, with electron_pred = phi^59 / 4194304000000 and proton_binding_pred = phi^43 / 1000000. Upstream theorems supply the tight intervals electron_mass_bounds and proton_mass_bounds together with the positivity lemma electron_pred_pos.
proof idea
The proof unfolds mu_pred and invokes electron_pred_pos to rewrite the target inequality as 1898 * electron_pred < proton_binding_pred. It applies the upper bound from electron_mass_bounds to obtain 1898 * electron_pred < 1898 * 0.5102, shows the right-hand side is less than 969 by norm_num, and combines with the lower bound from proton_mass_bounds via linarith.
why it matters in Recognition Science
This lower bound is paired with mu_pred_upper inside the downstream theorem mu_pred_bracket to produce the full interval (1898, 1904). The module compares the resulting prediction to the CODATA value 1836.15 and notes the 4 percent deviation arising from the proton sitting between phi-ladder rungs 47 and 48. It fills the Phase 0 row P0-MU of the physical derivation plan and supports the mass formula yardstick * phi^(rung - 8 + gap(Z)).
scope and limits
- Does not establish numerical agreement with the CODATA proton-electron ratio.
- Does not derive the underlying phi-ladder expressions for the individual masses.
- Does not incorporate higher-order binding corrections or rung adjustments.
- Does not address ratios involving other particles or sectors.
Lean usage
theorem mu_pred_bracket : (1898 : ℝ) < mu_pred ∧ mu_pred < (1904 : ℝ) := ⟨mu_pred_lower, mu_pred_upper⟩formal statement (Lean)
70theorem mu_pred_lower : (1898 : ℝ) < mu_pred := by
proof body
Tactic-mode proof.
71 unfold mu_pred
72 have he_pos : 0 < electron_pred := electron_pred_pos
73 rw [lt_div_iff₀ he_pos]
74 -- want: 1898 * electron_pred < proton_binding_pred
75 have he_hi : electron_pred < (0.5102 : ℝ) := electron_mass_bounds.2
76 have hp_lo : (969 : ℝ) < proton_binding_pred := proton_mass_bounds.1
77 -- 1898 * electron_pred < 1898 * 0.5102 = 968.3596 < 969 < proton_binding_pred
78 have step1 : (1898 : ℝ) * electron_pred < (1898 : ℝ) * (0.5102 : ℝ) := by
79 have h1898 : (0 : ℝ) < 1898 := by norm_num
80 exact mul_lt_mul_of_pos_left he_hi h1898
81 have step2 : (1898 : ℝ) * (0.5102 : ℝ) < (969 : ℝ) := by norm_num
82 linarith
83