electron_pred_pos
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.