module module high

`IndisputableMonolith.Numerics.Interval.AlphaBounds`

The Numerics.Interval.AlphaBounds module certifies that alpha_seed equals 4π·11 and lies strictly above 138.230048. Researchers verifying fine-structure constant intervals in Recognition Science cite these results when assembling dimensionless predictions. The module assembles the inequality by importing the closed-form w8 weight and Alpha constants, then applying Taylor expansions of the exponential at three nearby points.

claim$\alpha_{\rm seed}=4\pi\cdot11>138.230048$

background

Recognition Science constrains the fine-structure constant via the eight-tick octave and the J-uniqueness relation. The upstream W8Bounds module supplies the explicit gap weight w8=(348+210√2−(204+130√2)φ)/7≈2.490569. The Alpha module provides the base seed definition. This module introduces the interval bounds that certify the numerical value of alpha_seed using those inputs.

The local setting is the preparation of rigorous interval certificates for all subsequent dimensionless constants before mass ladders or mixing angles are evaluated.

proof idea

The module is organized as a chain of auxiliary bound lemmas. Each lemma invokes the Taylor polynomial of degree 10 for exp together with an explicit remainder estimate at the evaluation points 0.48, 0.481 and 0.483; the resulting ceiling and floor inequalities are then combined to sandwich alpha_seed.

why it matters in Recognition Science

These alpha bounds are imported by HartreeRydbergScoreCard (rows P1-C04, P1-C02, P1-C03), Masses.NumericalPredictions (all verified mass intervals), CKMGeometry (mixing-angle derivation), ElectronGMinus2ScoreCard (Schwinger term), and ElectronMass.Necessity (T9 forcing). The module therefore supplies the numerical foundation required by the T8-to-T11 chain.

scope and limits

Does not derive alpha from the functional equation.
Does not compare the interval to experimental data.
Does not extend the Taylor analysis beyond the three listed abscissae.
Does not produce closed-form expressions for alpha.

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