pith. machine review for the scientific record. sign in
def definition def or abbrev high

alphaInverseLower

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  30def alphaInverseLower : ℝ := 137.030

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.