Constants Alpha Genesis Measurement Verdict Exp Neg 0086705 Taylor Floor

The Taylor floor

The fine-structure constant α measures the strength of the electromagnetic interaction between charged particles. Its inverse, 1/α, is approximately 137.035999177, a value determined by experiment and compiled by CODATA. A proposed theoretical derivation, called the first-order Alpha Genesis value, predicts a different number. The declaration exp_neg_0086705_taylor_floor is a small but essential piece of the machine-checked argument that this prediction is wrong.

The declaration establishes a lower bound on the value of the exponential function at a specific negative input. It proves that the natural exponential of −0.0086705 is greater than 0.99136694. This is not a numerical approximation from a calculator; it is a formally verified theorem. The proof works by taking the first twelve terms of the Taylor series for the exponential function and subtracting a bound on the error from the remaining terms. This yields a rational number that is guaranteed to be less than the true value of the exponential.

This particular lower bound appears in a chain of reasoning about the Alpha Genesis model. The model's prediction for 1/α involves an exponential factor. The bound from exp_neg_0086705_taylor_floor helps to show that this factor is too small to bring the model's value down to the measured one. The final, coarse verdict is a theorem: the first-order Alpha Genesis value exceeds the CODATA value by more than 0.0007. Since the one-sigma uncertainty on the CODATA value is 2.1e-8, this overshoot is more than 30,000 standard deviations. The proposed value is excluded by measurement.

What this declaration does not do is prove that the fine-structure constant is wrong, or that the Alpha Genesis model is fundamentally flawed. It only certifies a numerical fact about the exponential function, which is then used in a larger argument. The declaration itself says nothing about physics. It is a lemma about real numbers, and its role is to provide a rigorous foundation for a much larger claim about a physical constant.

In Recognition Science, this declaration is part of a quarantine module. It imports measured data from an external source, which is why it is kept separate from the forward construction of the Alpha Genesis value. The point of the quarantine is to keep the formal system clean: the theorem about the exponential function uses only the standard axioms of the logic, while the comparison against CODATA is a separate, labeled step. The declaration is a piece of mathematical infrastructure, not a physical law.

private lemma exp_neg_0086705_taylor_floor :
    (49568347 / 50000000 : ℚ) <
      exp_taylor_12_at_neg_0086705 - exp_error_12_at_neg_0086705 := by
  norm_num [exp_taylor_12_at_neg_0086705, exp_error_12_at_neg_0086705, Nat.factorial]

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

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

What this page does not claim

This declaration does not prove that the Alpha Genesis model is wrong, only that its first-order value is excluded by measurement. This declaration does not derive the fine-structure constant from first principles. This declaration does not claim that the exponential function is defined by its Taylor series.

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: