Physics Alpha Running Correction Score Card Running Ratio Gt

The running ratio bound

The fine-structure constant, a number near 1/137, measures the strength of electromagnetic interactions. In quantum electrodynamics, its value changes with the energy scale at which it is probed, an effect called running. The ratio of the constant's inverse at the Z boson mass (about 91 GeV) to its value at low energy is a standard quantity in particle physics. A machine-checked library of formal theorems, built on the Recognition Science framework, proves that this ratio lies strictly between 0.933 and 0.935.

The theorem, named running_ratio_gt, establishes only the lower bound: the ratio exceeds 0.933. A companion theorem, running_ratio_lt, establishes the upper bound below 0.935. Together they bracket the ratio in a band about 0.002 wide. The proof uses the framework's derived value for the inverse fine-structure constant at zero energy, which falls between 137.030 and 137.039, and the measured PDG value of 127.951 at the Z mass. The ratio of these two numbers lands in the stated interval.

The band is a property of the framework's construction, not a measurement of the fine-structure constant itself. The framework's own documentation states plainly that it does not derive the measured fine-structure constant. The inverse coupling at low energy is a boundary datum, and the framework proves that every positive value of the inverse coupling is realized by some normalization. The band is the certified window of a construction at a specific normalization, about 429000 times wider than the CODATA 2022 measurement it is read against. The framework also proves that its construction value is excluded by that measurement at more than 30000 sigma.

What the theorem does establish is a consistency check on the framework's particle content. The scorecard module counts 3 charged leptons and 5 light quarks below the Z mass, with zero additional free parameters. The running ratio band follows from this content and the framework's low-energy value. The theorem is checked by the machine, with no unproved assumptions beyond the standard logical axioms. It is a precise statement about a ratio, not about the absolute value of the coupling.

/-- The running ratio exceeds 0.933. -/
theorem running_ratio_gt : (0.933 : ℝ) < running_ratio := by
  unfold running_ratio alpha_inv_mz_pdg alpha_inv_0
  rw [lt_div_iff₀ (by linarith [Numerics.alphaInv_gt] : (0 : ℝ) < alphaInv)]
  calc (0.933 : ℝ) * alphaInv < 0.933 * 137.039 := by nlinarith [Numerics.alphaInv_lt]
    _ = 127.857387 := by norm_num
    _ < 127.951 := by norm_num

/-- The running ratio is below 0.935. -/
theorem running_ratio_lt : running_ratio < (0.935 : ℝ) := by
  unfold running_ratio alpha_inv_mz_pdg alpha_inv_0
  rw [div_lt_iff₀ (by linarith [Numerics.alphaInv_gt] : (0 : ℝ) < alphaInv)]
  calc (0.935 : ℝ) * alphaInv > 0.935 * 137.030 := by nlinarith [Numerics.alphaInv_gt]
    _ = 128.12305 := by norm_num
    _ > 127.951 := by norm_num

/-- The running ratio exceeds 0.933. -/
theorem running_ratio_gt : (0.933 : ℝ) < running_ratio := by
  unfold running_ratio alpha_inv_mz_pdg alpha_inv_0
  rw [lt_div_iff₀ (by linarith [Numerics.alphaInv_gt] : (0 : ℝ) < alphaInv)]
  calc (0.933 : ℝ) * alphaInv < 0.933 * 137.039 := by nlinarith [Numerics.alphaInv_lt]
    _ = 127.857387 := by norm_num
    _ < 127.951 := by norm_num

/-- α⁻¹(0) > 137.030. -/
theorem alpha_inv_0_gt : (137.030 : ℝ) < alpha_inv_0 :=
  Numerics.alphaInv_gt

/-- α⁻¹(0) < 137.039. -/
theorem alpha_inv_0_lt : alpha_inv_0 < (137.039 : ℝ) :=
  Numerics.alphaInv_lt

theorem alphaRunningCorrectionScoreCardCert_holds :
    Nonempty AlphaRunningCorrectionScoreCardCert :=
  ⟨{ alpha_0_band := ⟨alpha_inv_0_gt, alpha_inv_0_lt⟩
     ratio_lt_one := running_ratio_lt_one
     ratio_band := ⟨running_ratio_gt, running_ratio_lt⟩
     leptons := rfl
     quarks := rfl
     zero_params := zero_free_params }⟩

What this page does not claim

The theorem does not claim that the fine-structure constant itself is derived or predicted by the framework. The theorem does not claim that the band is a measurement or a falsifiable prediction. The theorem does not claim that the ratio band is narrow compared to experimental precision.

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/Physics/AlphaRunningCorrectionScoreCard.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: