Verification Pdgcomparison

The comparison module

verification pdgcomparison is a module in the Recognition Science library that performs a machine-checked comparison between the framework's predictions and experimental values published by the Particle Data Group (PDG) and CODATA. The module stores experimental numbers as fixed constants, such as the electron mass 0.51099895069 GeV and the muon mass 105.6583755 MeV, alongside their reported uncertainties. It also stores the framework's own predicted interval for the inverse fine-structure constant, from 137.030 to 137.039.

The central comparison concerns the inverse fine-structure constant α⁻¹. The module proves, as a formal theorem, that the framework's interval contains the CODATA 2022 measured value of 137.035999177(21). That sounds like a success, but the module itself is explicit about what it is worth. The framework's interval is about 429,000 times wider than the measurement's uncertainty. The theorem alpha_result_could_not_have_failed proves that the band is so wide that no conceivable measurement could have fallen outside it. In other words, the comparison could not have failed, so it carries no evidential weight.

The module is deliberately quarantined from the framework's main proof chain. It imports experimental values, which are not derived from Recognition Science, so its results are informational rather than part of the forced derivation. Separate modules in the library prove a stronger statement: the framework's central construction value for α⁻¹ is excluded by the CODATA measurement at more than 30,000 standard deviations. The framework does not derive the measured fine-structure constant, and the module does not claim otherwise.

What the module does establish, in plain language, is a precise and honest boundary. It shows exactly where the framework's construction window sits relative to a high-precision measurement, and it proves that the window is too broad to be tested by that measurement. The practical consequence is that the reader can see, with machine-checked certainty, that this particular comparison is not evidence for or against the framework. It is a documented non-result, kept separate from the framework's certified claims.

/-- **THEOREM**: The RS prediction interval CONTAINS the CODATA central value.

    This is the key result: the Recognition Science prediction
    137.030 < α⁻¹ < 137.039
    contains the experimental value
    α⁻¹ = 137.035999177(21)
-/
theorem alphaInv_RS_contains_CODATA :
    alphaInv_RS_lo < alphaInv_CODATA_2022 ∧ alphaInv_CODATA_2022 < alphaInv_RS_hi := by
  constructor
  · -- 137.030 < 137.035999177
    unfold alphaInv_RS_lo alphaInv_CODATA_2022
    norm_num
  · -- 137.035999177 < 137.039
    unfold alphaInv_CODATA_2022 alphaInv_RS_hi
    norm_num

/-- The band could not have failed: it is more than 100000 times the measurement's
    own uncertainty, so containment was fixed before the experiment reported. -/
theorem alpha_result_could_not_have_failed :
    100000 * alpha_result.exp_sigma < alpha_result.rs_hi - alpha_result.rs_lo := by
  unfold alpha_result
  norm_num

/-- RS predicts: 137.030 < α⁻¹ < 137.039 -/
def alphaInv_RS_lo : ℝ := 137.030

What this page does not claim

The module does not claim that the framework derives the measured fine-structure constant. The module does not claim that the band's containment of the CODATA value is evidence for the framework. The module does not claim that the framework's construction value agrees with the measurement; separate theorems prove it is excluded at more than 30,000 sigma.

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/Verification/PDGComparison.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: