Encyclopedia Constants Constants Alpha Genesis Measurement Verdict Exp Neg 0086705 Gt

ARTICLE 3 claims 3 theorems

Constants Alpha Genesis Measurement Verdict Exp Neg 0086705 Gt

A machine-checked proof shows a candidate value for the fine-structure constant misses the measured value by more than 30,000 times the measurement's uncertainty.

Verify this page

The measurement verdict

The fine-structure constant α measures the strength of electromagnetic interaction between charged particles. Its inverse, 1/α, is approximately 137.035999177, a value determined by the CODATA international adjustment of 2022 with an uncertainty of 0.000000021. The Recognition Science framework, which derives physical constants from a forced cost function, produces a first-order candidate for 1/α. The declaration exp_neg_0086705_gt is a lemma in the framework's machine-checked library of formal theorems. It establishes that the exponential of negative 0.0086705 is greater than 0.99136694, a numerical fact used to certify a larger claim.

The larger claim is a formal theorem: the framework's first-order genesis value for 1/α exceeds the CODATA value by at least 0.0007. Since CODATA's one-sigma uncertainty is 2.1e-8, this overshoot is more than 30,000 standard deviations. The theorem is proved in the library's MeasurementVerdict module, which is quarantined because it imports CODATA data through an external anchor. The proof uses a Taylor series floor for the exponential function, discharged by the norm_num tactic, so the entire derivation stays within the standard axioms of the ambient type theory.

In Recognition Science, this verdict is decisive for the current first-order construction. The value is excluded by measurement before any seam correction is derived. The theorem does not claim that the framework's approach to α is wrong overall, nor does it prove that a corrected value will succeed. It establishes only that the first-order candidate, as it stands, is incompatible with the measured value by a certified margin. The exact reported residual is about 7.67e-4; the certified margin of 0.0007 is the stronger, honest fact needed for the reply to the measurement objection.

What the declaration does not claim is equally important. It does not derive the fine-structure constant from first principles; the seed for the genesis value is an identification, not a derived coupling. It does not prove the Riemann Hypothesis or any other unproven conjecture. It does not claim that the framework's approach is validated by this comparison; rather, it formalizes the strongest measurement-side objection and confirms it. The theorem is a quarantine module, meaning nothing in the forward construction imports it, so the verdict does not contaminate the rest of the framework's derivations.

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]
THEOREM exp_neg_0086705_gt · IndisputableMonolith/Constants/AlphaGenesis/MeasurementVerdict.lean
exp_neg_0086705_gt · IndisputableMonolith/Constants/AlphaGenesis/MeasurementVerdict.lean:126 
/-- `exp(-0.0086705) > 0.99136694`. -/
private lemma exp_neg_0086705_gt : (0.99136694 : ℝ) < Real.exp (-0.0086705 : ℝ) := by
  have hx_abs : |(-0.0086705 : ℝ)| ≤ 1 := by norm_num
  have h_bound := Real.exp_bound hx_abs (n := 12) (by norm_num : 0 < 12)
  have h_abs := abs_sub_le_iff.mp h_bound
  have h_taylor_eq :
      (∑ m ∈ Finset.range 12, (-0.0086705 : ℝ)^m / m.factorial) =
        (exp_taylor_12_at_neg_0086705 : ℝ) := by
    simp only [exp_taylor_12_at_neg_0086705, Finset.sum_range_succ, Finset.sum_range_zero,
      Nat.factorial]
    norm_num
  have h_err_eq :
      |(-0.0086705 : ℝ)|^12 * ((Nat.succ 12 : ℕ) / ((Nat.factorial 12 : ℕ) * 12)) =
        (exp_error_12_at_neg_0086705 : ℝ) := by
    simp only [exp_error_12_at_neg_0086705, Nat.factorial, Nat.succ_eq_add_one]
    norm_num
  have h_lower_raw :
      (exp_taylor_12_at_neg_0086705 : ℝ) ≤
        |(-0.0086705 : ℝ)|^12 * ((Nat.succ 12 : ℕ) / ((Nat.factorial 12 : ℕ) * 12)) +
          Real.exp (-0.0086705 : ℝ) := by
    simpa [h_taylor_eq, add_comm, add_left_comm, add_assoc] using h_abs.2
  have h_lower :
      (exp_taylor_12_at_neg_0086705 : ℝ) - (exp_error_12_at_neg_0086705 : ℝ) ≤
        Real.exp (-0.0086705 : ℝ) := by
    have h_lower' :
        (exp_taylor_12_at_neg_0086705 : ℝ) ≤
          (exp_error_12_at_neg_0086705 : ℝ) + Real.exp (-0.0086705 : ℝ) := by
      calc
        (exp_taylor_12_at_neg_0086705 : ℝ)
            ≤ |(-0.0086705 : ℝ)|^12 *
                ((Nat.succ 12 : ℕ) / ((Nat.factorial 12 : ℕ) * 12)) +
                  Real.exp (-0.0086705 : ℝ) := h_lower_raw
        _ = (exp_error_12_at_neg_0086705 : ℝ) + Real.exp (-0.0086705 : ℝ) := by
              rw [h_err_eq]
    linarith
  have h_num :
      (0.99136694 : ℝ) <
        (exp_taylor_12_at_neg_0086705 : ℝ) - (exp_error_12_at_neg_0086705 : ℝ) := by
    have h' : (((49568347 / 50000000 : ℚ) : ℝ)) <
        (exp_taylor_12_at_neg_0086705 : ℝ) - (exp_error_12_at_neg_0086705 : ℝ) := by
      exact_mod_cast exp_neg_0086705_taylor_floor
    norm_num at h' ⊢
    exact h'
  exact lt_of_lt_of_le h_num h_lower

What this page does not claim

The fine-structure constant is derived from first principles; its seed is an identification, not a derived coupling. The framework's overall approach to α is disproved; only the first-order candidate is excluded by measurement. The Riemann Hypothesis or any other unproven conjecture is established by this declaration.

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