alpha_seed_lt
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not supply a matching lower bound on alpha_seed.
- Does not incorporate the gap correction f_gap.
- Does not apply to the higher-order or precision variants of alpha_seed defined elsewhere.
formal statement (Lean)
26theorem alpha_seed_lt : alpha_seed < (138.230092 : ℝ) := by
proof body
Term-mode proof.
27 simp only [alpha_seed]
28 have h := Real.pi_lt_d6
29 linarith
30
31/-! ## f_gap bounds -/
32