structural_mass_bounds
plain-language theorem explainer
Structural mass bounds establish that the electron structural mass satisfies 10856 < m < 10858 in Recognition Science units, where m equals 2^{-22} phi^{51}. Lepton mass modelers cite the result when propagating the interval through phi-residue factors to obtain muon and tau predictions. The tactic proof rewrites the mass via its forced closed form, invokes the phi_pow51 interval lemmas, and chains division inequalities with numerical comparisons using lt_trans.
Claim. Let $m$ denote the electron structural mass in Recognition Science units. Then $10856 < m < 10858$, where $m = 2^{-22} phi^{51}$.
background
In Recognition Science the electron structural mass is obtained from the phi-ladder mass formula after fixing the appropriate rung and gap for the electron. Module T9 Necessity proves the mass formula is forced from T8 ledger quantization together with geometric constants derived earlier in the T0-T8 chain. The local setting is that all mass scales descend from the self-similar fixed point phi (T6) and the eight-tick octave (T7). Upstream results supply the Chain structure for recognition sequences and the tight rational bounds on phi^{51} from Numerics.Interval.PhiBounds.
proof idea
The proof invokes the forced closed-form lemma for electron_structural_mass, rewrites 2^{-22} as 1/4194304 and phi^{51} via goldenRatio, then applies the lemmas phi_pow51_gt and phi_pow51_lt. Division by the positive denominator 4194304 preserves the inequalities via div_lt_div_of_pos_right. Coarse numerical comparisons 10856 < 45537548334/4194304 and 45537549354/4194304 < 10858 are combined with lt_trans after rewriting the mass expression to the scaled form.
why it matters
This theorem anchors the T9 necessity claim that the electron mass is geometrically determined from the phi-ladder. It feeds directly into the lepton generations necessity theorems such as predicted_mass_mu_lower and muon_mass_pred_bounds_tight, which use the interval (10856, 10858) to bound the muon mass in (105.3, 106.5). In the framework it closes part of the mass ladder descending from the eight-tick octave and D=3, with the phi fixed point from T6; the result also supports downstream neutrino and quark mass checks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.