alphaInverseLower
plain-language theorem explainer
The lower bound for the inverse fine-structure constant is fixed at 137.030. Researchers tracing the alpha derivation from the recognition uniqueness theorem would reference this value to confirm the predicted interval contains the measured CODATA result. The definition follows directly from evaluating the 44-pi formula at the forced parameters.
Claim. The lower bound on the inverse fine-structure constant is $137.030$.
background
The module derives the fine-structure constant from the recognition uniqueness theorem, which forces the functional form J(x) = (x + 1/x)/2 - 1. This in turn fixes the golden ratio phi as the self-similar fixed point. With the eight-tick octave requiring three spatial dimensions, the structure produces 44 frequency slots. The resulting formula is alpha inverse equals 44 pi times exp of minus 8 ln phi over 44 pi. The lower bound 137.030 is chosen so the interval (137.030, 137.039) encloses the CODATA value.
proof idea
The declaration is a direct numerical assignment of the constant 137.030. No lemmas are applied; it serves as the explicit lower endpoint for the alpha interval.
why it matters
This bound enters the structural certificate AlphaProvenanceCert, which verifies that the CODATA value lies within the RS band. It completes the chain from the uniqueness theorem through the forced phi and dimension D equals 3 to the explicit alpha prediction. The result supports the framework claim that the inverse fine-structure constant must fall inside this narrow window derived from the 44-pi structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.