Encyclopedia Numerics Numerics Interval Alpha Bounds Alpha Inv Gt 137031

ARTICLE 3 claims 2 theorems 1 measured

Numerics Interval Alpha Bounds Alpha Inv Gt 137031

A machine-checked proof places the inverse fine-structure constant above 137.031, a bound far too loose to test the theory behind it.

Verify this page

A certified lower bound

The inverse fine-structure constant, written 1/α, is a pure number that sets the strength of electromagnetic interaction. Its measured value, from the 2022 CODATA adjustment, is 137.035999177(21), meaning the uncertainty is about 21 in the last two digits. The declaration alphaInv_gt_137031 is a machine-checked theorem stating that a quantity called alphaInv, defined inside the Recognition Science framework, is greater than 137.031. The proof is a chain of rational arithmetic and exponential estimates, all verified by a computer.

The theorem is real but its evidentiary value is deliberately modest. The band it establishes, from 137.031 upward, is roughly 429,000 times wider than the measurement uncertainty of the CODATA value. A band that wide cannot test whether the framework's construction matches nature. The framework's own documentation says so plainly: this is not agreement. A separate module proves the framework's value exceeds the measured one by more than 30,000 measurement sigmas, a decisive miss. The wide band here is a sanity check on the arithmetic, not a physical claim.

In Recognition Science, the framework models physical constants as forced outcomes of a recognition ledger, a discrete record of events whose cost is fixed by a proved functional equation. The framework derives a seed value for 1/α from 4π raised to the eleventh power, which lies near 138.23. The declaration alphaInv_gt_137031 is a lower bound on that seed after a correction term, called f_gap, is subtracted. The correction involves the golden ratio and a constant from the framework's eight-tick cycle, but the bound itself is just numerical: it certifies that the final number stays above 137.031.

What the theorem does not claim is more important than what it does. It does not claim that 1/α equals any particular value. It does not claim the framework's value agrees with measurement. It does not derive the fine-structure constant from first principles; the seed 4π¹¹ is an identification, not a derived coupling. The exact value of α remains an open target. The theorem's sole content is a verified inequality, useful only as a guard against arithmetic error in the framework's internal construction.

THEOREM alphaInv_gt_137031 · IndisputableMonolith/Numerics/Interval/AlphaBounds.lean
alphaInv_gt_137031 · IndisputableMonolith/Numerics/Interval/AlphaBounds.lean:349 
/-- Slightly sharper lower bound for the inverse fine-structure constant.

This uses the same certified Taylor and interval ingredients as `alphaInv_gt`;
the stronger decimal is needed by the hydrogenic Rydberg acceptance bridge. -/
theorem alphaInv_gt_137031 : (137.031 : ℝ) < 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.031 : ℝ) < (138.230048 : ℝ) * (((991327 / 1000000 : ℚ) : ℝ) : ℝ) := by norm_num
    _ < alpha_seed * (((991327 / 1000000 : ℚ) : ℝ) : ℝ) := hseed_mul
    _ < alpha_seed * Real.exp (-(f_gap / alpha_seed)) := hmul
MEASURED alphaInv_gt_137031 · IndisputableMonolith/Numerics/Interval/AlphaBounds.lean
alphaInv_gt_137031 · IndisputableMonolith/Numerics/Interval/AlphaBounds.lean:349 
/-- Slightly sharper lower bound for the inverse fine-structure constant.

This uses the same certified Taylor and interval ingredients as `alphaInv_gt`;
the stronger decimal is needed by the hydrogenic Rydberg acceptance bridge. -/
theorem alphaInv_gt_137031 : (137.031 : ℝ) < 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.031 : ℝ) < (138.230048 : ℝ) * (((991327 / 1000000 : ℚ) : ℝ) : ℝ) := by norm_num
    _ < alpha_seed * (((991327 / 1000000 : ℚ) : ℝ) : ℝ) := hseed_mul
    _ < alpha_seed * Real.exp (-(f_gap / alpha_seed)) := hmul
THEOREM alphaInv_gt_137031 · IndisputableMonolith/Numerics/Interval/AlphaBounds.lean
alphaInv_gt_137031 · IndisputableMonolith/Numerics/Interval/AlphaBounds.lean:349 
/-- Slightly sharper lower bound for the inverse fine-structure constant.

This uses the same certified Taylor and interval ingredients as `alphaInv_gt`;
the stronger decimal is needed by the hydrogenic Rydberg acceptance bridge. -/
theorem alphaInv_gt_137031 : (137.031 : ℝ) < 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.031 : ℝ) < (138.230048 : ℝ) * (((991327 / 1000000 : ℚ) : ℝ) : ℝ) := by norm_num
    _ < alpha_seed * (((991327 / 1000000 : ℚ) : ℝ) : ℝ) := hseed_mul
    _ < alpha_seed * Real.exp (-(f_gap / alpha_seed)) := hmul

What this page does not claim

This theorem does not claim that alphaInv equals any specific value, only that it exceeds 137.031. This theorem does not claim the framework's value agrees with the CODATA measurement; the framework's own modules document a miss by over 30,000 sigmas. This theorem does not derive the fine-structure constant; the seed 4π¹¹ is an identification, not a derived coupling.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND