Precision Band for the Fine-Structure Constant

1. Setting

The alpha page is the benchmark for the whole derivations surface. It is not a numerology page. The Lean proof bounds the closed-form expression for alpha inverse between 137.030 and 137.039, and CODATA sits inside. The inputs are J-cost uniqueness, phi forcing, the eight-tick weight, and the 44 pi geometric seed.

2. Equations

(E1)

$$ \alpha^{-1}=44\pi\exp!\left(-\frac{w_8\ln\varphi}{44\pi}\right),\qquad 137.030<\alpha^{-1}<137.039 $$

Closed-form alpha inverse and its Lean-certified band.

3. Prediction or structural target

• alpha inverse: predicted in (137.030, 137.039) (dimensionless); empirical 137.035999084(21). Source: CODATA 2022

This entry is one of the marquee derivations. The numerical or formal target is explicit, and the falsifier identifies the failure mode.

4. Formal anchor

The primary anchor is Numerics.Interval.AlphaBounds..alphaInv_gt.

theorem alphaInv_gt : (137.030 : ℝ) < alphaInv := by
  simp only [alphaInv]
  have hseed_pos : (0 : ℝ) < alpha_seed := lt_trans (by norm_num) alpha_seed_gt
  have hy_hi : f_gap / alpha_seed < (0.00871 : ℝ) := by
    have hmul : f_gap < (0.00871 : ℝ) * alpha_seed := by
      have h1 : f_gap < (1.203 : ℝ) := f_gap_lt
      have h2 : (1.203 : ℝ) < (0.00871 : ℝ) * (138.230048 : ℝ) := by norm_num
      have h3 : (0.00871 : ℝ) * (138.230048 : ℝ) < (0.00871 : ℝ) * alpha_seed := by
        exact mul_lt_mul_of_pos_left alpha_seed_gt (by norm_num)

5. What is inside the Lean module

Key theorems:

• alpha_seed_gt
• alpha_seed_lt
• exp_048_taylor_ceiling
• exp_048_lt
• exp_0481_taylor_ceiling
• exp_0481_lt
• exp_0483_taylor_floor
• exp_0483_gt
• log_phi_gt_048
• log_phi_gt_0481
• log_phi_lt_0483
• f_gap_gt

Key definitions:

• exp_taylor_10_at_048
• exp_error_10_at_048
• exp_taylor_10_at_0481
• exp_error_10_at_0481
• exp_taylor_10_at_0483
• exp_error_10_at_0483
• exp_taylor_10_at_neg_00871
• exp_error_10_at_neg_00871

6. Derivation chain

• alphaInv_gt - Lower bound 137.030
• alphaInv_lt - Upper bound 137.039
• alphaInv_lt_strong - Strong upper bound
• f_gap_gt - f_gap lower bound
• f_gap_lt - f_gap upper bound
• alpha_seed_gt - alpha_seed lower
• alpha_seed_lt - alpha_seed upper

7. Falsifier

A future consensus value for alpha inverse outside (137.030, 137.039), after experimental systematics are settled, refutes the RS alpha derivation.

8. Where this derivation stops

Below this page the chain reduces to the RS forcing sequence: J-cost uniqueness, phi forcing, the eight-tick cycle, and the D=3 recognition substrate. If any upstream theorem changes, this page must be versioned rather than patched silently. The published URL is stable, but the version field is the contract.

11. Why this belongs in the derivations corpus

The corpus is organized around load-bearing consequences, not around file names. This entry is included because Numerics.Interval.AlphaBounds contributes a reusable theorem or definitional bridge that other pages can cite. Keeping the page public gives readers a stable URL, a JSON record, and a direct path into the Lean theorem page. If the entry becomes redundant with a stronger derivation later, the current slug should be retired rather than silently rewritten; the replacement should absorb its anchors and preserve the audit history.