alpha_seed_gt_132
plain-language theorem explainer
The inequality establishes that the geometric seed exceeds 132. Researchers bounding the fine-structure constant in Recognition Science cite it to fix the lower edge of the alpha inverse interval near 137.03. The proof reduces directly to the definition alpha_seed = 44 pi and applies nonlinear arithmetic on the library fact pi > 3.
Claim. $132 < 44π$ where $44π$ denotes the geometric seed $α_{seed}$ obtained from the 11-edge ledger structure.
background
The AlphaPrecision module refines the inverse fine-structure constant via an additive seed formula $α^{-1}{add} = 4π × 11$ and an exponential resummation $α^{-1} = α{seed} × exp(−w_8 ln φ / α_{seed})$, with $w_8 ≈ 2.490$. The local definition sets $α_{seed} := 44 × Real.pi$, which equals $4π$ times the number of passive edges and represents the baseline spherical closure cost over 11-edge interaction paths. This theorem supplies the strict lower bound on that seed. It depends on the sibling definition of alpha_seed together with the standard inequality Real.pi > 3.
proof idea
The term proof first unfolds the definition of alpha_seed to expose the product 44 * Real.pi. It then invokes the nlinarith tactic, supplying the library lemma Real.pi_gt_three as the sole witness, which immediately yields the desired strict inequality.
why it matters
The result anchors the proved interval $α^{-1} ∈ (137.030, 137.039)$ stated in the module documentation, a 60 ppm window around the CODATA 2022 value. It supplies the lower-bound step inside the Q8 precision refinement of the fine-structure constant and rests on the geometric seed construction from the ledger structure. No downstream theorems yet consume it, and the claim touches no open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.