Encyclopedia Constants Constants Alpha Genesis Measurement Verdict Exponential Load Lt 0086705

ARTICLE 3 claims 3 theorems

Constants Alpha Genesis Measurement Verdict Exponential Load Lt 0086705

A machine-checked theorem certifies that a proposed route to the fine-structure constant misses the measured value by more than 30,000 times the experimental uncertainty.

Verify this page

The exponential load bound

The fine-structure constant α governs the strength of electromagnetic interactions, and its inverse 1/α is measured with extraordinary precision. The CODATA 2022 value is 137.035999177, with a one-sigma uncertainty of 0.000000021. In the Recognition Science framework, a first-order construction called Alpha Genesis aims to derive this constant from first principles.

The declaration exponentialLoad_lt_0086705 establishes a precise numerical bound: the ratio of a certain gap function to a seed value in the framework is less than 0.0086705. This is a theorem proved in the machine-checked library of formal theorems, meaning the inequality is certified by computer-verified logic.

This bound feeds into a larger verdict. The framework's library proves that the first-order Alpha Genesis value for 1/α exceeds the CODATA value by at least 0.0007. Since the experimental uncertainty is 2.1e-8, this overshoot is more than 30,000 sigma. In plain terms, the first-order construction is excluded by measurement with overwhelming statistical significance.

The declaration does not claim that the Alpha Genesis construction is correct, nor that it is close to the measured value. It establishes the opposite: the first-order value is ruled out. The bound is a quarantine module, importing external CODATA data and kept separate from the forward construction, precisely so the negative verdict cannot contaminate the derivation chain.

What matters for the reader is the epistemic posture. The framework does not merely assert its derivation; it subjects it to the sharpest available experimental test and reports the failure plainly. The exponential load bound is a load-bearing honesty certificate, not a step toward confirmation.

THEOREM exponentialLoad_lt_0086705 · IndisputableMonolith/Constants/AlphaGenesis/MeasurementVerdict.lean
exponentialLoad_lt_0086705 · IndisputableMonolith/Constants/AlphaGenesis/MeasurementVerdict.lean:173 
/-- Tight upper bound on the natural exponential load `f_gap / alpha_seed`. -/
theorem exponentialLoad_lt_0086705 :
    Constants.f_gap / Constants.alpha_seed < (0.0086705 : ℝ) := by
  have hfg_hi : Constants.f_gap < (1.198514 : ℝ) := by
    unfold Constants.f_gap
    have hw_hi := Numerics.W8Bounds.w8_computed_lt
    have hlog_hi := log_phi_lt_048122
    have hw_pos : 0 < Constants.w8_from_eight_tick := Constants.w8_pos
    have hlog_pos : 0 < Real.log Constants.phi := by
      exact Real.log_pos Constants.one_lt_phi
    calc
      Constants.w8_from_eight_tick * Real.log Constants.phi
          < Constants.w8_from_eight_tick * (0.48122 : ℝ) :=
            mul_lt_mul_of_pos_left hlog_hi hw_pos
      _ < (2.490572090 : ℝ) * (0.48122 : ℝ) :=
            mul_lt_mul_of_pos_right hw_hi (by norm_num)
      _ < (1.198514 : ℝ) := by norm_num
  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
  rw [div_lt_iff₀ hseed_pos]
  calc
    Constants.f_gap < (1.198514 : ℝ) := hfg_hi
    _ < (0.0086705 : ℝ) * Constants.alpha_seed := by nlinarith [hseed_lo]
THEOREM alphaInvGenesis_exceeds_CODATA_by_0007 · IndisputableMonolith/Constants/AlphaGenesis/MeasurementVerdict.lean
alphaInvGenesis_exceeds_CODATA_by_0007 · IndisputableMonolith/Constants/AlphaGenesis/MeasurementVerdict.lean:197 
/-- 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
THEOREM margin_0007_gt_30000_sigma · IndisputableMonolith/Constants/AlphaGenesis/MeasurementVerdict.lean
margin_0007_gt_30000_sigma · IndisputableMonolith/Constants/AlphaGenesis/MeasurementVerdict.lean:233 
/-- 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 Alpha Genesis value is close to the measured value. It does not claim the framework's derivation of the fine-structure constant is correct. It does not claim the exponential load bound itself is a physical constant with independent meaning.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND