Encyclopedia Numerics Numerics Interval Alpha Bounds F Gap Gt Strong

ARTICLE 3 claims 3 theorems

Numerics Interval Alpha Bounds F Gap Gt Strong

A machine-checked theorem pins down a number that appears in the Recognition Science account of the inverse fine-structure constant, and the honest reading is that the number is far from the measured value.

Verify this page

The numerical gap

The inverse fine-structure constant α⁻¹ is a pure number, about 137.036, that physicists measure with extraordinary precision. It describes the strength of the electromagnetic force between charged particles. In the Recognition Science framework, a chain of formal theorems derives a candidate expression for this constant from a ledger, a discrete record of recognition events, and the expression lands near the measured value. The declaration f_gap_gt_strong is one small piece of that derivation: it proves, with machine-checked certainty, that a certain numerical gap is larger than 1.1979.

That gap, written f_gap, is the product of two framework-internal numbers: w8, a constant that emerges from the framework's eight-tick recognition cycle, and the natural logarithm of the golden ratio φ. The theorem f_gap_gt_strong states that this product exceeds 1.1979. The proof is a chain of inequalities: it bounds w8 from below using a previously proved computation, bounds log φ from below using a Taylor-series estimate, and multiplies the two bounds together. The result is a rigorous lower bound, not an approximation. The companion theorem f_gap_lt shows the same gap is less than 1.203, so the full interval for f_gap is (1.1979, 1.203).

The reason this gap matters is that it feeds into the framework's interval bounds for α⁻¹. The same module proves α⁻¹ lies between 137.030 and 137.039, a band about 0.009 wide. The CODATA 2022 measured value is 137.035999177(21), with an uncertainty of 21 in the last two digits. The framework's band is about 429,000 times wider than the measurement's error bar. The docstring for the module says this plainly: the band holding both the framework's construction and the measurement at the same time is not agreement. A separate theorem in the library proves the framework's central value exceeds the measured value by more than 30,000 measurement sigmas.

In Recognition Science, the framework models the inverse fine-structure constant through a seed of 44π, which evaluates to about 138.23, and then applies a correction involving the gap f_gap. The result is an interval that contains the measured value. But the framework does not claim to derive the exact value of α⁻¹. The expression is an identification, not a derived coupling, and the exact value remains an open problem. The theorem f_gap_gt_strong is a precise, machine-checked statement about a number that appears in the derivation; it does not by itself establish anything about the physical constant.

THEOREM f_gap_gt_strong · IndisputableMonolith/Numerics/Interval/AlphaBounds.lean
f_gap_gt_strong · IndisputableMonolith/Numerics/Interval/AlphaBounds.lean:217 
/-- Stronger lower bound for the gap term using log(φ) > 0.481. -/
theorem f_gap_gt_strong : (1.1979 : ℝ) < f_gap := by
  simp only [f_gap]
  have h_w8_lo := W8Bounds.w8_computed_gt
  have h_log_lo := log_phi_gt_0481
  have h_w8_pos : 0 < w8_from_eight_tick := IndisputableMonolith.Constants.w8_pos
  have h0481 : 0 < (0.481 : ℝ) := by norm_num
  calc (1.1979 : ℝ) < 2.490564399 * (0.481 : ℝ) := by norm_num
    _ < w8_from_eight_tick * (0.481 : ℝ) := by
      exact mul_lt_mul_of_pos_right h_w8_lo h0481
    _ < w8_from_eight_tick * log IndisputableMonolith.Constants.phi := by
      exact mul_lt_mul_of_pos_left h_log_lo h_w8_pos
THEOREM alphaInv_gt · alphaInv_lt · IndisputableMonolith/Numerics/Interval/AlphaBounds.lean
alphaInv_gt · IndisputableMonolith/Numerics/Interval/AlphaBounds.lean:321 
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
alphaInv_lt · IndisputableMonolith/Numerics/Interval/AlphaBounds.lean:381 
theorem alphaInv_lt : alphaInv < (137.039 : ℝ) := by
  simp only [alphaInv]
  have hseed_pos : (0 : ℝ) < alpha_seed := lt_trans (by norm_num) alpha_seed_gt
  have hy_lo : (0.00866 : ℝ) < f_gap / alpha_seed := by
    have hmul : (0.00866 : ℝ) * alpha_seed < f_gap := by
      have h1 : (0.00866 : ℝ) * alpha_seed < (0.00866 : ℝ) * (138.230092 : ℝ) := by
        exact mul_lt_mul_of_pos_left alpha_seed_lt (by norm_num)
      have h2 : (0.00866 : ℝ) * (138.230092 : ℝ) < (1.1979 : ℝ) := by norm_num
      exact lt_trans h1 (lt_trans h2 f_gap_gt_strong)
    exact (lt_div_iff₀ hseed_pos).2 (by simpa [mul_comm, mul_left_comm, mul_assoc] using hmul)
  have hexp_hi : Real.exp (-(f_gap / alpha_seed)) < ((495689 / 500000 : ℚ) : ℝ) := by
    have hmono : Real.exp (-(f_gap / alpha_seed)) < Real.exp (-(0.00866 : ℝ)) := by
      exact Real.exp_lt_exp.mpr (by linarith [hy_lo])
    exact lt_trans hmono exp_neg_00866_lt
  have hmul :
      alpha_seed * Real.exp (-(f_gap / alpha_seed)) <
        alpha_seed * (((495689 / 500000 : ℚ) : ℝ)) := by
    exact mul_lt_mul_of_pos_left hexp_hi hseed_pos
  have hseed_hi :
      alpha_seed * (((495689 / 500000 : ℚ) : ℝ)) <
        (138.230092 : ℝ) * (((495689 / 500000 : ℚ) : ℝ)) := by
    exact mul_lt_mul_of_pos_right alpha_seed_lt (by norm_num)
  calc
    alpha_seed * Real.exp (-(f_gap / alpha_seed))
        < alpha_seed * (((495689 / 500000 : ℚ) : ℝ) : ℝ) := hmul
    _ < (138.230092 : ℝ) * (((495689 / 500000 : ℚ) : ℝ) : ℝ) := hseed_hi
    _ < (137.039 : ℝ) := by norm_num
THEOREM alphaInv_gt · IndisputableMonolith/Numerics/Interval/AlphaBounds.lean
alphaInv_gt · IndisputableMonolith/Numerics/Interval/AlphaBounds.lean:321 
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

What this page does not claim

The theorem f_gap_gt_strong does not claim that the gap is close to the measured inverse fine-structure constant. The framework does not claim to derive the exact value of α⁻¹; the exact value remains an open problem. The band (137.030, 137.039) is not claimed to be a precise prediction; it is a wide interval that contains the measured value.

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