Physics Alpha Running Correction Score Card Alpha Running Correction Score Card

The running correction scorecard

The fine-structure constant α measures the strength of the electromagnetic force. Its value changes with the energy scale at which you probe it, an effect called running. The standard model predicts this running from the particle content: below the Z boson mass, three charged leptons, five light quarks, and the W boson contribute to vacuum polarization, a quantum screening effect. The one-loop formula for the correction is Δα = α/(3π) Σ_f N_c Q_f² [log(M_Z²/m_f²) − 5/3], where the sum runs over fermions with their color factors and charges.

The scorecard declaration certifies (formally proves in the framework's machine-checked library) a band for the inverse fine-structure constant at zero momentum transfer: α⁻¹(0) lies strictly between 137.030 and 137.039. Using the measured value α⁻¹(M_Z) = 127.951 ± 0.009 from the Particle Data Group, the running ratio α⁻¹(M_Z)/α⁻¹(0) falls strictly between 0.933 and 0.935. The certificate also records that the particle content below M_Z is fixed at exactly three charged leptons and five light quarks, with zero additional free parameters.

In Recognition Science, this band is the certified window of a construction, not a claim about the measured alpha. The framework's own irreducibility proof shows the forced ledger closure on the cube cannot determine the U(1) kinetic normalization κ_γ; every positive value of the inverse coupling is realized by some normalization. The (137.030, 137.039) band is the window on the witness value at κ_γ = 1, about 429000 times wider than the CODATA 2022 measurement 137.035999177(21). The framework proves that every value inside the band is realized by some normalization, so no measurement could have contradicted it, and that the construction value is excluded by the measurement at more than 30000 sigma.

What the scorecard establishes is a consistency statement: the framework's construction window and the empirical running correction can hold simultaneously. The running ratio being less than one reflects vacuum polarization screening, a standard physics fact. The certificate does not derive the fine-structure constant itself; that remains an open target, as the irreducibility proof makes explicit.

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 }⟩

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

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 certificate does not derive the fine-structure constant itself; that remains an open target. The band (137.030, 137.039) is not a prediction that can be tested by measurement, since every value inside it is realized by some normalization. The scorecard does not claim the one-loop formula is exact beyond its stated approximation.

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: