alpha_seed_lt
plain-language theorem explainer
The theorem establishes that the geometric seed alpha_seed, defined as 4π·11, satisfies alpha_seed < 138.230092. Researchers deriving certified interval bounds on the inverse fine-structure constant cite this result to tighten upper estimates inside the alphaInv pipeline. The proof unfolds the definition via simp and closes the inequality with the standard pi bound together with linear arithmetic.
Claim. Let $a := 4π·11$. Then $a < 138.230092$.
background
In this module the geometric seed alpha_seed is introduced as the baseline spherical closure cost over 11-edge interaction paths, given explicitly by the definition 4 * Real.pi * 11. The surrounding module supplies rigorous interval bounds on α⁻¹ derived from the ledger structure and the Recognition Composition Law. Upstream results include the core definition in Constants.Alpha together with variants in AlphaHigherOrder and AlphaPrecision, plus the gap weight f_gap that appears as a logarithmic correction from the eight-tick projection.
proof idea
The proof is a one-line wrapper that applies simp only [alpha_seed] to unfold the definition, introduces the known inequality Real.pi_lt_d6, and closes the goal with linarith.
why it matters
The bound is invoked by the downstream theorem alphaInv_lt that establishes alphaInv < 137.039. It therefore contributes to the certified interval (137.030, 137.039) for α⁻¹ that the framework predicts from the J-uniqueness and phi-ladder constructions. The result closes one numerical step in the pipeline that converts the eight-tick octave and D = 3 into observable constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.