Numerics Interval Alpha Bounds Alpha Inv Lt Strong

A certified upper bound

The inverse fine-structure constant α⁻¹ is a pure number, about 137.036, that sets the strength of electromagnetic interaction between charged particles. In the Recognition Science framework, the constant emerges from a chain of derived structure rather than being inserted by hand. The declaration alphaInv_lt_strong is a machine-checked theorem stating that this framework-derived value is less than 137.039.

The proof is a formal bound, not a numerical evaluation. It works by combining a lower bound on a gap function f_gap with known bounds on the golden ratio φ, ultimately showing the derived inverse constant stays below the stated threshold. The companion theorem alphaInv_gt establishes the value exceeds 137.030, so the framework pins α⁻¹ to an interval roughly 0.009 wide.

That interval is about 429,000 times wider than the CODATA 2022 measurement of 137.035999177(21). The framework's own documentation is explicit: this is not agreement. A separate module proves the RS value exceeds the measured value by more than 30,000 measurement sigmas, and that any band holding both the construction and the measurement would be wider than that exclusion. The bound here is a consistency check on the framework's internal derivation, not a match to experiment.

The declaration does not claim the framework's α⁻¹ equals the measured value, nor that the interval contains it. It establishes only an upper limit on the framework's own derived quantity, certified by a machine-checked proof. The exact value of α⁻¹ within the framework, and any reconciliation with measurement, remains open.

/-- Upper bound alias retained for backwards compatibility after the canonical
exponential α update. -/
theorem alphaInv_lt_strong : alphaInv < (137.039 : ℝ) := by
  exact alphaInv_lt

theorem alphaInv_gt : (137.030 : ℝ) < alphaInv := by
  simp only [alphaInv]
  have hseed_pos : (0 : ℝ) < alpha_seed := lt_trans (by norm_num) alpha_seed_gt
  have hy_hi : f_gap / alpha_seed < (0.00871 : ℝ) := by
    have hmul : f_gap < (0.00871 : ℝ) * alpha_seed := by
      have h1 : f_gap < (1.203 : ℝ) := f_gap_lt
      have h2 : (1.203 : ℝ) < (0.00871 : ℝ) * (138.230048 : ℝ) := by norm_num
      have h3 : (0.00871 : ℝ) * (138.230048 : ℝ) < (0.00871 : ℝ) * alpha_seed := by
        exact mul_lt_mul_of_pos_left alpha_seed_gt (by norm_num)
      exact lt_trans h1 (lt_trans h2 h3)
    exact (div_lt_iff₀ hseed_pos).2 (by simpa [mul_comm, mul_left_comm, mul_assoc] using hmul)
  have hexp_lo : ((991327 / 1000000 : ℚ) : ℝ) < Real.exp (-(f_gap / alpha_seed)) := by
    have hmono : Real.exp (-(0.00871 : ℝ)) < Real.exp (-(f_gap / alpha_seed)) := by
      exact Real.exp_lt_exp.mpr (by linarith [hy_hi])
    exact lt_trans exp_neg_00871_gt hmono
  have hseed_mul :
      (138.230048 : ℝ) * (((991327 / 1000000 : ℚ) : ℝ)) <
        alpha_seed * (((991327 / 1000000 : ℚ) : ℝ)) := by
    exact mul_lt_mul_of_pos_right alpha_seed_gt (by norm_num)
  have hmul :
      alpha_seed * (((991327 / 1000000 : ℚ) : ℝ)) <
        alpha_seed * Real.exp (-(f_gap / alpha_seed)) := by
    exact mul_lt_mul_of_pos_left hexp_lo hseed_pos
  calc
    (137.030 : ℝ) < (138.230048 : ℝ) * (((991327 / 1000000 : ℚ) : ℝ) : ℝ) := by norm_num
    _ < alpha_seed * (((991327 / 1000000 : ℚ) : ℝ) : ℝ) := hseed_mul
    _ < alpha_seed * Real.exp (-(f_gap / alpha_seed)) := hmul

/-- Upper bound alias retained for backwards compatibility after the canonical
exponential α update. -/
theorem alphaInv_lt_strong : alphaInv < (137.039 : ℝ) := by
  exact alphaInv_lt

What this page does not claim

The framework's inverse fine-structure constant equals the measured value. The interval [137.030, 137.039] contains the CODATA 2022 measurement. The declaration alphaInv_lt_strong is a numerical evaluation rather than a formal bound.

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: