alpha_sq_bounds
plain-language theorem explainer
The lemma establishes that the square of the fine-structure constant lies strictly between 0.0000532 and 0.0000533. Researchers deriving lepton masses or bounding radiative corrections within the Recognition Science necessity proofs would cite these bounds to control error propagation on the mass ladder. The proof is a short tactic sequence that squares the prior interval for alpha and compares the results numerically.
Claim. $0.0000532 < {alpha}^2 < 0.0000533$, where $alpha$ is the fine-structure constant.
background
The declaration sits inside the module proving T9 necessity: the electron mass formula is forced from T8 ledger quantization together with geometric constants obtained earlier. The fine-structure constant is introduced as the reciprocal of its inverse, and the sibling lemma alpha_bounds already supplies the interval 0.007297 < alpha < 0.0072977. The local setting is therefore the controlled numerical propagation of these constants into mass and correction formulas.
proof idea
The proof calls the alpha_bounds lemma, applies the square-strict-inequality lemma to each endpoint, then uses calc chains with norm_num to insert the squared numerical thresholds.
why it matters
The result is invoked by radiative_correction_bounds in the same module and by step_e_mu_bounds (and its v2) in the lepton-generations necessity files. It therefore participates in the T9 claim that the electron mass is forced, while remaining inside the alpha band (137.030, 137.039) already fixed by the Recognition Science constants. No scaffolding or open question is closed by this lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.