Physics Alpha Running Correction Score Card Running Ratio Lt One

The running ratio

The fine-structure constant, written α, measures the strength of the electromagnetic force. At everyday low energies its inverse is about 137.036. At the mass of the Z boson, the heaviest carrier of the weak force, the inverse falls to about 127.951. The ratio of these two numbers, α⁻¹(M_Z)/α⁻¹(0), is the running ratio. It is less than 1 because vacuum polarization screens the bare charge: virtual particle pairs weaken the force at large distances, so the force appears stronger when probed at short range.

The machine-checked library of formal theorems proves this ratio lies in a narrow band. The theorem running_ratio_lt_one establishes that the ratio is below 1. Two companion theorems pin it between 0.933 and 0.935. The proof uses the framework's own value for α⁻¹(0), which the forcing chain places between 137.030 and 137.039, and the measured PDG value 127.951 for α⁻¹(M_Z). The particle content below the Z mass, three charged leptons and five light quarks, enters the one-loop vacuum polarization integral; the framework certifies that this content carries zero free parameters.

In Recognition Science, the band for α⁻¹(0) is a certified window of a construction, not a prediction of the measured constant. The framework's own no-go result proves it cannot derive the fine-structure constant: the ledger closure on the cube is blind to the U(1) kinetic normalization, and every positive value of the inverse coupling is realized by some normalization. The band is about 429000 times wider than the CODATA 2022 measurement 137.035999177(21), and the construction value is excluded by that measurement at more than 30000 sigma. The running ratio theorem is an internal consistency check, not a match to experiment.

What the theorem changes: it certifies that the framework's low-energy window, when run up to the Z mass with standard QED corrections, lands in the same narrow band as the measured high-energy value. The size of the electromagnetic running is thus a derived fact inside the framework, even though the constant it starts from is not.

/-- The running ratio is less than 1 (vacuum polarization screens). -/
theorem running_ratio_lt_one : running_ratio < 1 := by
  unfold running_ratio alpha_inv_mz_pdg alpha_inv_0
  rw [div_lt_one (by linarith [Numerics.alphaInv_gt])]
  linarith [Numerics.alphaInv_gt]

/-- 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

theorem zero_free_params : particle_content_free_params = 0 := rfl

What this page does not claim

The framework derives the fine-structure constant itself. The band (137.030, 137.039) is a prediction that any measurement could confirm. The running ratio theorem makes the framework's low-energy alpha value match the CODATA measurement.

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: