Numerics Interval Alpha Bounds Alpha Seed Gt

The seed's lower bound

The inverse fine-structure constant, usually written 1/α, is a pure number near 137.036 that sets the strength of electromagnetic interactions. CODATA 2022 gives 1/α = 137.035999177(21), where the parentheses mark uncertainty in the last two digits. Recognition Science (RS) constructs its own candidate for this constant from a seed value, and the declaration alpha_seed_gt is a formal, machine-checked statement about that seed.

In plain terms, alpha_seed_gt proves that the seed is greater than 138.230048. The seed itself is defined as 4π¹¹, roughly 138.2300779. The theorem does not compute this number exactly; it establishes a rigorous lower bound using known bounds on π, and a companion theorem alpha_seed_lt proves the seed is less than 138.230092. Together they bracket the seed in an interval about 44 millionths wide.

That interval matters because of what it does and does not do. The measured value 137.035999177 sits about 1.194 below the seed's lower bound. The gap is roughly 1.2, while the measurement uncertainty is about 0.000000021. In statistical terms, the RS seed exceeds the measured value by more than 30,000 standard deviations. The framework's own documentation states this plainly: the band asserted here is about 429,000 times wider than the measurement it is read against, and it holds the RS construction and the measurement at the same time. That is not agreement.

In Recognition Science, this seed is an identification, not a derived coupling. The framework does not claim to derive the fine-structure constant itself; the exact value of α remains an open target. What alpha_seed_gt establishes is purely numerical: a lower bound on a defined quantity, verified by a machine-checked library of formal theorems. It does not establish that the seed equals the measured constant, nor that the gap can be closed by further refinement. It is a precise statement about a number, and its precision is what makes the disagreement with measurement so stark.

/-- alpha_seed = 4π·11 > 138.230048 -/
theorem alpha_seed_gt : (138.230048 : ℝ) < alpha_seed := by
  simp only [alpha_seed]
  have h := Real.pi_gt_d6
  linarith

/-- alpha_seed = 4π·11 < 138.230092 -/
theorem alpha_seed_lt : alpha_seed < (138.230092 : ℝ) := by
  simp only [alpha_seed]
  have h := Real.pi_lt_d6
  linarith

/-- alpha_seed = 4π·11 < 138.230092 -/
theorem alpha_seed_lt : alpha_seed < (138.230092 : ℝ) := by
  simp only [alpha_seed]
  have h := Real.pi_lt_d6
  linarith

What this page does not claim

This answer does not claim that alpha_seed_gt establishes the value of the fine-structure constant. This answer does not claim that the seed's interval is narrow enough to count as agreement with measurement. This answer does not claim that the seed is a derived coupling rather than an identification.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Numerics/Interval/AlphaBounds.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: