electron_geo_gt_13_953
plain-language theorem explainer
The theorem establishes a strict lower bound of 13.953 on the geometric residue for the electron at rung Z=1332. Physicists comparing the phi-ladder mass formula to perturbative RG transport would cite it to quantify the discrepancy that defines recognition strength. The tactic proof fixes the electron Z-value by native decision and reduces the inequality directly to the first conjunct of the pre-established gap bounds at that rung.
Claim. $13.953 < F(1332)$, where $F(Z)$ is the geometric residue of a fermion with rung index $Z$ on the phi-ladder.
background
The Recognition Coupling module compares the geometric mass formula, which requires a large residue $F(Z)$ for each particle, against the small residue $f_{RG}$ obtained by integrating Standard Model beta functions. For the electron the geometric side yields $F(1332) > 13.953$ while the RG side is approximately 0.0494, so the ratio $F(Z)/f_{RG}$ measures the extra strength needed to reconcile the two pictures. The module treats this ratio as a non-universal diagnostic rather than a fixed constant.
proof idea
The proof first obtains $ZOf Fermion.e = 1332$ by native_decide. It then applies simpa with the rewrite rules for geometric_residue and the equality, discharging the goal against the left-hand side of gap_1332_bounds.
why it matters
The bound supplies the concrete numerator for the downstream strength comparison electron_strength_gt_100. It closes the geometric half of the discrepancy described in the module documentation, connecting the phi-ladder mass formula (yardstick times phi to the power of rung minus 8 plus gap) to the eight-tick octave and D=3 structure of the forcing chain. It leaves open whether a single universal recognition strength can be extracted from the family of such ratios.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.