Physics Alpha Running Correction Score Card

The running correction scorecard

The fine-structure constant α measures the strength of electromagnetic interactions. Its value changes with the energy scale at which you probe it, an effect called running. The single largest radiative correction to electroweak mass predictions is the running of α from zero energy to the mass of the Z boson, about 91 GeV. In the standard model, this correction is not a free parameter: it is calculable from the known particle content below that scale, namely three charged leptons, five light quarks, and the W boson.

The standard one-loop vacuum polarization formula gives Δα = α/(3π) Σ_f N_c Q_f² [log(M_Z²/m_f²) − 5/3]. The scorecard module in the Recognition Science library applies this formula to the framework's predicted value of α⁻¹(0), which lies in the band (137.030, 137.039). Using the measured PDG value α⁻¹(M_Z) = 127.951 ± 0.009, the module proves the running ratio α⁻¹(M_Z)/α⁻¹(0) falls in (0.933, 0.935). This ratio is less than one because vacuum polarization screens the charge.

In Recognition Science, the particle content below M_Z is not assumed but derived from the framework's forcing chain. The module therefore certifies that the corrected vacuum expectation value, computed from the RS-native α(0), lands within the PDG band with zero additional free parameters. The machine-checked library proves the band statements as formal theorems: α⁻¹(0) > 137.030, α⁻¹(0) < 137.039, 0.933 < running_ratio < 0.935, and running_ratio < 1. These combine into a single certificate structure with no axioms beyond the standard three.

The honesty condition is explicit. Recognition Science does not claim to derive the measured fine-structure constant. The band (137.030, 137.039) is the certified window of a construction at a specific normalization, about 429000 times wider than the CODATA 2022 measurement 137.035999177(21). The library proves every value inside the band is realized by some normalization, so no measurement could have contradicted it, and the construction value is excluded at more than 30000 sigma. The scorecard's value is structural: it shows the running correction, the largest radiative effect, is consistent with the framework's derived particle content and adds no free parameters.

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

theorem zero_free_params : particle_content_free_params = 0 := rfl

/-- α⁻¹(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

What this page does not claim

The module does not claim to derive the measured fine-structure constant α. The band (137.030, 137.039) is not a prediction about α; it is a construction window at a specific normalization. The scorecard does not claim the running correction is measured, only that it is consistent with the PDG 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/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: