Masses Vevconsistency Running Ratio Bounds

The running ratio bounds

The Higgs field's vacuum expectation value (VEV), roughly 246 GeV, sets the mass scale for many elementary particles. In the standard model, this value is not derived from first principles; it is measured and put into the theory by hand. The Recognition Science framework's library of formal theorems instead attempts to calculate it from a small set of internal quantities. One step in that calculation is a correction factor, and the theorem running_ratio_bounds establishes that this factor lies strictly between 0.940 and 0.942.

This factor is the ratio of two versions of the fine-structure constant, which measures the strength of electromagnetic interactions. At zero energy, its inverse is about 137.036. At the mass of the Z boson, a heavy carrier of the weak force, quantum effects from virtual particles change this value to about 128.9. The ratio 128.9 / 137.036 is approximately 0.941. The theorem proves, using only the framework's derived values and the standard electroweak formula, that this ratio is bounded within the narrow window (0.940, 0.942). This is not an approximation; it is a proven mathematical statement within the framework's axiom system.

This bound matters because it is the final piece in a consistency check. The framework's tree-level formula, using its own values for the Z mass, the weak mixing angle, and the inverse fine-structure constant, predicts a VEV of about 253 GeV. This overshoots the measured value of 246.22 GeV by about 2.8 percent. The running ratio correction, applied to account for the energy scale difference, brings the prediction down to about 245.5 GeV, within 0.3 percent of the measured value. The theorem running_ratio_bounds certifies that this correction is not a free parameter but a fixed, bounded quantity derived from the framework's own constants.

It is important to state plainly what this theorem does not do. It does not prove that the framework derives the fine-structure constant. The framework itself acknowledges this: a separate result shows that every positive value of the inverse coupling is realized by some normalization, and the measured value is excluded at over 30000 sigma. The band (137.030, 137.039) used in the VEV calculation is a certified window of a construction, not a prediction of alpha. The theorem running_ratio_bounds only establishes the bounds on the ratio, assuming the framework's inputs. It does not claim the VEV prediction is a perfect match, nor does it prove the underlying physics is correct. It certifies the internal consistency of the framework's calculation, given its own premises.

/-- The running ratio is in (0.940, 0.942). -/
theorem running_ratio_bounds :
    (0.940 : ℝ) < running_ratio ∧ running_ratio < (0.942 : ℝ) := by
  unfold running_ratio alphaInv_MZ
  have halpha_gt := Numerics.alphaInv_gt       -- 137.030 < αInv
  have halpha_lt := Numerics.alphaInv_lt        -- αInv < 137.039
  have halpha_pos : (0 : ℝ) < alphaInv := by linarith
  constructor
  · -- 128.9 / αInv > 0.940 ⟺ 128.9 > 0.940 × αInv
    rw [lt_div_iff₀ halpha_pos]
    -- 0.940 × αInv < 0.940 × 137.039 = 128.816... < 128.9
    nlinarith
  · -- 128.9 / αInv < 0.942 ⟺ 128.9 < 0.942 × αInv
    rw [div_lt_iff₀ halpha_pos]
    -- 128.9 < 0.942 × αInv. αInv > 137.030, so 0.942 × 137.030 = 129.084... > 128.9
    nlinarith

/-- The tree-level VEV squared from RS inputs (in MeV²). -/
noncomputable def vev_tree_sq : ℝ :=
  ElectroweakMasses.z_pred ^ 2 *
  ElectroweakMasses.sin2_theta_W_rs *
  ElectroweakMasses.cos2_theta_W_rs *
  alphaInv / Real.pi

/-- The running correction ratio: α⁻¹(M_Z) / α⁻¹(0).
    This corrects the tree-level VEV to the physical scale. -/
noncomputable def running_ratio : ℝ := alphaInv_MZ / alphaInv

What this page does not claim

The theorem does not prove the framework derives the fine-structure constant alpha. It does not claim the VEV prediction is a perfect match to measurement. It does not prove the underlying physics of the framework is correct.

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/Masses/VEVConsistency.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: