alphaInv_lt_strong
plain-language theorem explainer
The declaration supplies a strict upper bound alphaInv < 137.039 that is retained solely for backwards compatibility after the canonical exponential update to the fine-structure constant. Numerics researchers working on Recognition Science interval bounds would cite it when porting older code that expects the 137.039 ceiling. The proof is a one-line exact application of the preceding alphaInv_lt theorem.
Claim. $alphaInv < 137.039$, where $alphaInv = alpha_seed * exp(-f_gap / alpha_seed)$ is the dimensionless inverse fine-structure constant obtained from the structural seed and gap with no free parameters.
background
The module Numerics.Interval.AlphaBounds supplies rigorous interval bounds on the inverse fine-structure constant using the symbolic derivation from the structural seed. The central definition is alphaInv := alpha_seed * Real.exp(-(f_gap / alpha_seed)), which evaluates numerically near 137.036. The upstream theorem alphaInv_lt already establishes the same strict inequality alphaInv < 137.039 by direct simplification and interval arithmetic on the seed and gap terms.
proof idea
The proof is a one-line wrapper that applies the preceding alphaInv_lt theorem directly via the exact tactic. No additional rewriting or case analysis is performed.
why it matters
The result preserves an explicit 137.039 ceiling that matches the framework interval (137.030, 137.039) for alpha^{-1} in RS-native units. It feeds no downstream theorems in the current graph but closes the compatibility path after the exponential resummation update to alphaInv. The bound sits inside the T5 J-uniqueness and T6 phi-fixed-point steps of the forcing chain, where the fine-structure constant emerges from the Recognition Composition Law without adjustable parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.