electron_strength_gt_100
plain-language theorem explainer
The theorem shows that fixing the perturbative residue at 0.04942583 forces the recognition strength ratio for the electron above 100. Researchers comparing geometric mass ladders to Standard Model beta-function running would cite this numerical bound when quantifying the required enhancement of the underlying recognition coupling. The proof unfolds the strength definition, substitutes the given value, invokes a prior lower bound on the geometric residue, and chains a pair of strict inequalities with a positivity check on the denominator.
Claim. Let $r = 0.04942583$. Then $100 < F_e / r$, where $F_e$ is the geometric residue attached to the electron fermion.
background
The module formalizes the discrepancy between the geometric mass formula, which requires a large residue $F(Z)$ of order 13.95 for the electron, and the small perturbative residue $f_{RG} approx 0.05$ obtained from Standard Model running. Recognition strength is defined as the ratio $F(Z)/f_{RG}$ that bridges this gap; the present theorem supplies a concrete lower bound once $f_{RG}$ is fixed at the stated numerical value. The geometric residue lower bound is supplied by the sibling result electron_geo_gt_13_953, while the arithmetic comparison relies on the transitivity lemma lt_trans imported from ArithmeticFromLogic.
proof idea
Unfold electron_strength and recognition_strength, rewrite the hypothesis to substitute the numerical residue, obtain positivity of the denominator by norm_num, pull in the geometric residue inequality electron_geo_gt_13_953, verify by norm_num that 100 times the residue is less than 13.953, apply lt_trans to reach the numerator inequality, and finish with lt_div_iff₀.
why it matters
The result supplies a concrete numerical anchor for the structural dominance hypothesis stated in the module comment, showing that the geometric residue dominates the perturbative correction by more than two orders of magnitude for the electron. It therefore contributes directly to the recognition coupling module's demonstration of the gap between geometric predictions and RG transport. Within the broader framework the bound illustrates the scale at which the recognition force must exceed its QED shadow to reproduce the observed mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.