alpha_seed_gt
plain-language theorem explainer
The declaration proves that the Recognition Science geometric seed 4π·11 exceeds 138.230048. Interval analysts deriving bounds on the inverse fine-structure constant cite this result to establish positivity and scaling for the gap term in alphaInv. The proof reduces the definition via simplification and invokes a standard lower bound on pi to close the inequality with linear arithmetic.
Claim. $138.230048 < 4π · 11$
background
The module Numerics.Interval.AlphaBounds supplies rigorous interval bounds on the inverse fine-structure constant alphaInv. It relies on the geometric seed alpha_seed defined as 4 * pi * 11, which encodes the baseline spherical closure cost over 11-edge interaction paths in the ledger structure. Upstream results include the definition of alpha_seed in Constants.Alpha as this exact expression, along with variants in AlphaHigherOrder and AlphaPrecision that retain the same 44 pi form. The local setting is the derivation of symbolic bounds for alpha inverse using the Recognition framework's constants.
proof idea
The proof applies simplification to unfold alpha_seed into 4 * Real.pi * 11. It then obtains a lower bound on pi from Real.pi_gt_d6 and closes the comparison with linarith.
why it matters
This result supplies the lower bound on alpha_seed required by the downstream theorems alphaInv_gt and alphaInv_lt, which together place alpha inverse inside the interval (137.030, 137.039) predicted by the Recognition Science constants. It anchors the numerics for the fine-structure constant derived from the phi-ladder and the eight-tick octave. The bound supports the framework's claim that alpha inverse lies in that narrow band without invoking higher-order corrections.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.