alpha_seed_lt_176
plain-language theorem explainer
The theorem proves that the geometric seed defined as 44 pi lies strictly below 176. Researchers refining the inverse fine-structure constant interval (137.030, 137.039) in Recognition Science cite this bound to fix the upper edge of the additive seed contribution. The term proof unfolds the seed definition and applies nonlinear arithmetic on the standard fact that pi is less than 4.
Claim. Let $44 pi$ denote the geometric seed. Then $44 pi < 176$.
background
The Alpha-Inverse Precision Refinement module (Q8) defines the additive seed formula as alpha inverse add equals 4 pi times 11 approximately 138.23, together with the exponential resummation alpha inverse equals alpha seed times exp of negative w sub 8 ln phi over alpha seed, where w sub 8 is approximately 2.490. The seed itself is the geometric baseline 4 pi times 11, representing the baseline spherical closure cost over 11-edge interaction paths. The module states that alpha inverse lies in (137.030, 137.039) with zero sorry or axiom, and targets 1 ppm refinement via curvature correction.
proof idea
The proof is a one-line wrapper that unfolds the definition of alpha seed as 44 times Real.pi and invokes nlinarith with the fact Real.pi_lt_four.
why it matters
This bound secures the upper limit on the additive seed contribution and thereby supports the proved interval alpha inverse in (137.030, 137.039) stated in the module documentation. It anchors the alpha band near 137.03 within the Recognition Science framework without curvature or gap corrections. The result closes a basic inequality needed for the Q8 refinement step before higher-order terms are introduced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.