Constants Alpha Genesis Measurement Verdict Alpha Inv Uncertainty Eq

The measured value and its verdict

The fine-structure constant α is a dimensionless number that sets the strength of the electromagnetic force between charged particles. Its inverse, 1/α, is what experimenters usually quote, and the CODATA 2022 adjustment gives 1/α = 137.035999177(21). The number in parentheses is the one-sigma uncertainty: the last two digits, 21, mean the measurement is uncertain by about 0.000000021. That is a precision of roughly 1.5 parts in ten billion, one of the most accurate measurements in all of physics.

In Recognition Science, a machine-checked library of formal theorems, a module called the Measurement Verdict confronts this measured value with the framework's own first-order prediction for 1/α. The theorem alpha_inv_uncertainty_eq states that the stored CODATA uncertainty is exactly 0.000000021. This is not a derived result; it is a direct import of the measured value into the formal system, a definitional equality that pins the number down so that later theorems can reason about it.

The verdict itself is stark. The same module proves that the first-order Alpha Genesis value exceeds the CODATA value by more than 0.0007. Since the uncertainty is 2.1e-8, that overshoot is more than 30,000 standard deviations. In plain terms: the framework's first-order prediction is excluded by measurement with overwhelming force. The exact residual is about 7.67e-4, but the certified margin of 0.0007 is the honest, conservative statement that the prediction fails before any correction is applied.

What the declaration does not claim is just as important. It does not say the framework's prediction is correct, nor that any correction will save it. It does not derive the fine-structure constant from first principles; the seed that produces the first-order value is an identification, not a derived coupling. The theorem merely records the measured uncertainty so that the comparison can be made, and the comparison is a failure for the first-order value. The module is quarantined: it imports the external CODATA measurement, and nothing in the forward construction depends on it. This is a page where the framework's own machinery documents its own empirical defeat.

/-- CODATA uncertainty is exactly the stored one-sigma value. -/
theorem alpha_inv_uncertainty_eq : alpha_inv_CODATA_uncertainty = (0.000000021 : ℝ) := rfl

/-- The first-order Alpha Genesis value is above CODATA by at least `0.0007`.
This is the formal version of Anil's measurement objection, stated coarsely
but with a fully certified margin. -/
theorem alphaInvGenesis_exceeds_CODATA_by_0007 :
    alpha_inv_CODATA + (0.0007 : ℝ) < alphaInvGenesis := by
  rw [alphaInvGenesis_eq_alphaInv]
  unfold Constants.alphaInv
  have hseed_lo : (138.230048 : ℝ) < Constants.alpha_seed := Numerics.alpha_seed_gt
  have hseed_pos : 0 < Constants.alpha_seed := lt_trans (by norm_num) hseed_lo
  have hload_hi : Constants.f_gap / Constants.alpha_seed < (0.0086705 : ℝ) :=
    exponentialLoad_lt_0086705
  have hexp_mono : Real.exp (-0.0086705 : ℝ) < Real.exp (-(Constants.f_gap / Constants.alpha_seed)) := by
    exact Real.exp_lt_exp.mpr (by linarith)
  have hexp_lo : (0.99136694 : ℝ) < Real.exp (-(Constants.f_gap / Constants.alpha_seed)) :=
    lt_trans exp_neg_0086705_gt hexp_mono
  have hmul :
      (138.230048 : ℝ) * (0.99136694 : ℝ) <
        Constants.alpha_seed * Real.exp (-(Constants.f_gap / Constants.alpha_seed)) := by
    have h1 :
        (138.230048 : ℝ) * (0.99136694 : ℝ) <
          Constants.alpha_seed * (0.99136694 : ℝ) :=
      mul_lt_mul_of_pos_right hseed_lo (by norm_num)
    have h2 :
        Constants.alpha_seed * (0.99136694 : ℝ) <
          Constants.alpha_seed * Real.exp (-(Constants.f_gap / Constants.alpha_seed)) :=
      mul_lt_mul_of_pos_left hexp_lo hseed_pos
    exact lt_trans h1 h2
  have htarget :
      alpha_inv_CODATA + (0.0007 : ℝ) <
        (138.230048 : ℝ) * (0.99136694 : ℝ) := by
    norm_num [alpha_inv_CODATA]
  exact lt_trans htarget hmul

/-- The certified `0.0007` overshoot is more than `30000` one-sigma
uncertainties. -/
theorem margin_0007_gt_30000_sigma :
    (30000 : ℝ) * alpha_inv_CODATA_uncertainty < (0.0007 : ℝ) := by
  norm_num [alpha_inv_CODATA_uncertainty]

What this page does not claim

The declaration does not claim the framework's first-order prediction is correct. It does not derive the fine-structure constant from first principles. It does not claim any correction will bring the prediction into agreement with 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/Constants/AlphaGenesis/MeasurementVerdict.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: