electron_mass_ledger_hypothesis
plain-language theorem explainer
The theorem shows that the electron residue, the logarithmic ratio of observed to structural mass in phi units, differs from gap(1332) minus the refined shift by less than 0.002 when the lower and upper residue hypotheses hold. Recognition Science researchers deriving particle masses from the forcing chain would cite this as the T9 step that closes the ledger-fraction account for the electron. The proof obtains explicit interval bounds from two prior theorems on the residue and on the gap-minus-shift expression, rewrites the absolute-value goal
Claim. Assuming the lower and upper hypotheses on the electron residue hold, $|r - (g(1332) - s)| < 0.002$, where $r = (1/2)log_φ(m_obs/m_struct)$ is the residue, $g(Z) = ln(1 + Z/φ)/ln(φ)$ is the gap function, and $s$ is the refined shift.
background
The electron residue is defined as log_φ(mass_ref_MeV / electron_structural_mass). The gap function is the closed-form display map g(Z) = ln(1 + Z/φ)/ln(φ) that appears in the RSBridge.Anchor module and equals the integrated mass anomalous dimension at the anchor scale. The module formalizes T9, the first structural break for the electron mass, by expressing the residue as the refined ledger fraction 2W + (W + E_total)/(4 E_passive) + α² + E_total α³ with W = 17, E_total = 12, E_passive = 11. Upstream results supply the concrete numerical bounds: electron_residue_bounds converts the two necessity hypotheses into the interval (-20.7063, -20.7057), while gap_minus_shift_bounds supplies the matching interval for g(1332) - refined_shift.
proof idea
The term proof introduces the two necessity hypotheses, applies electron_residue_bounds to obtain the residue interval, invokes gap_minus_shift_bounds for the target interval, rewrites the goal with abs_lt, and discharges both sides by linear arithmetic on the four endpoint inequalities.
why it matters
This is the T9 theorem that confirms the electron mass matches the gap-minus-refined-shift ledger fraction to the stated tolerance. It sits inside the T0-T8 forcing chain, using the phi fixed point from T6 and the three-dimensional gap construction. The result feeds the structural mass formula on the phi-ladder and the alpha-band constants. The note in the declaration records that the present bounds only reach 0.002 while empirical agreement is 10^{-6}; tighter necessity hypotheses would close that gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.