module module high

`IndisputableMonolith.Numerics.Interval.AlphaBounds`

Module Numerics.Interval.AlphaBounds supplies machine-verified interval bounds on the fine-structure constant via the seed quantity 4 pi * 11. Scorecard and prediction modules for electron g-2, masses, CKM angles, and Hartree-Rydberg quantities import these bounds to certify agreement with measured intervals. The module consists of Taylor-expansion lemmas with explicit remainder controls together with direct comparisons that establish the seed inequality and related exponential bounds at points near 0.48.

claim$\alpha_{\rm seed} = 4\pi\cdot 11 > 138.230048$, with companion upper and lower bounds obtained from Taylor remainders of $\exp$ at arguments 0.48, 0.481, 0.483.

background

The module imports W8Bounds, whose central object is the closed-form eight-tick weight $w_8 = (348 + 210\sqrt{2} - (204 + 130\sqrt{2})\phi)/7 \approx 2.490569$, and Constants.Alpha. These supply the numerical constants needed to convert the Recognition Science phi-ladder and J-cost into concrete interval statements for $\alpha^{-1}$. The local setting is the numerics layer that turns the abstract T5 J-uniqueness and T7 eight-tick octave into machine-checked inequalities lying inside the target band (137.030, 137.039).

proof idea

The module is a collection of definition and lemma blocks. Each block introduces a Taylor polynomial of degree 10 for exp together with an explicit error term, then applies interval arithmetic to obtain strict inequalities at the three evaluation points 0.48, 0.481, 0.483. The seed comparison alpha_seed_gt is obtained by direct arithmetic on the imported constants.

why it matters in Recognition Science

The bounds are imported by HartreeRydbergScoreCard (P1-C02, P1-C03, P1-C04), Masses.NumericalPredictions, CKMGeometry, ElectronGMinus2ScoreCard (P1-C05), and ElectronMass.Necessity. They close the numerical verification step that links the eight-tick octave and phi-ladder to the experimental alpha band required by the downstream physical derivations.

scope and limits

Does not derive the value of alpha from the functional equation; only certifies interval membership.
Does not contain floating-point computations; all statements are formal inequalities.
Does not address higher-order QED corrections beyond the leading Schwinger term.
Does not replace the abstract T5 J-uniqueness; supplies only its numerical consequences.

used by (5)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Constants.HartreeRydbergScoreCard module_import
IndisputableMonolith.Masses.NumericalPredictions module_import
IndisputableMonolith.Physics.CKMGeometry module_import
IndisputableMonolith.Physics.ElectronGMinus2ScoreCard module_import
IndisputableMonolith.Physics.ElectronMass.Necessity module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants.Alpha module_import
IndisputableMonolith.Numerics.Interval.W8Bounds module_import

declarations in this module (31)

theorem alpha_seed_gt L20
theorem alpha_seed_lt L26
def exp_taylor_10_at_048 L33
def exp_error_10_at_048 L37
lemma exp_048_taylor_ceiling L41
lemma exp_048_lt L45
def exp_taylor_10_at_0481 L78
def exp_error_10_at_0481 L82
lemma exp_0481_taylor_ceiling L86
lemma exp_0481_lt L90
def exp_taylor_10_at_0483 L123
def exp_error_10_at_0483 L127
lemma exp_0483_taylor_floor L131
lemma exp_0483_gt L135
lemma log_phi_gt_048 L169
lemma log_phi_gt_0481 L176
lemma log_phi_lt_0483 L183
theorem f_gap_gt L190
theorem f_gap_gt_strong L204
theorem f_gap_lt L216
def exp_taylor_10_at_neg_00871 L232
def exp_error_10_at_neg_00871 L236
lemma exp_neg_00871_taylor_floor L240
lemma exp_neg_00871_gt L244
def exp_taylor_10_at_neg_00866 L268
def exp_error_10_at_neg_00866 L272
lemma exp_neg_00866_taylor_ceiling L276
lemma exp_neg_00866_lt L280
theorem alphaInv_gt L307
theorem alphaInv_lt L335
theorem alphaInv_lt_strong L365