electron_pred_pos
Positivity of the predicted electron mass follows from its placement inside a positive numerical interval on the phi-ladder. Researchers verifying dimensionless mass ratios in Recognition Science cite the result to license division when forming mu_pred. The argument extracts the strict lower bound supplied by the interval theorem and concludes via linear arithmetic.
claim$0 < m_e^pred$ where $m_e^pred = phi^{59}/4194304000000$ is the Recognition Science prediction for the electron mass.
background
The MuRatioScoreCard module records interval bounds on the predicted proton-electron mass ratio inside the phi-ladder construction of Recognition Science. The electron term is defined as phi raised to the 59th power divided by 4194304000000, corresponding to the lepton-sector assignment at rung 2. The upstream theorem electron_mass_bounds establishes the concrete interval 0.5098 < electron_pred < 0.5102 by unfolding the definition and applying norm_num arithmetic.
proof idea
The lemma invokes electron_mass_bounds to obtain the lower bound 0.5098 < electron_pred and feeds that fact to the linarith tactic, which deduces strict positivity from the known positive lower bound.
why it matters in Recognition Science
The lemma is invoked by mu_pred_lower, mu_pred_pos, and mu_pred_upper to justify the division step in mu_pred = proton_binding_pred / electron_pred. It thereby supports the proved bracket 1898 < mu_pred < 1904 that forms the Phase 0 verification of the proton-electron ratio against the CODATA value. The step rests on the phi-ladder mass formula and the positivity requirement for ratio formation.
scope and limits
- Does not derive the exponent 59 from the forcing chain.
- Does not compare the prediction to the experimental electron mass.
- Does not establish bounds on the proton prediction.
- Does not address binding-energy corrections beyond the current rung assignment.
formal statement (Lean)
51private lemma electron_pred_pos : 0 < electron_pred := by
proof body
Term-mode proof.
52 have hb := electron_mass_bounds
53 linarith [hb.1]
54