module module high

`IndisputableMonolith.Numerics.Interval.AlphaBounds`

This module supplies rigorous interval bounds on the fine-structure constant alpha using the eight-tick weight and Taylor expansions. Physicists checking Recognition Science numerical predictions against measured values cite these bounds. It assembles closed-form W8 expressions and seed inequalities to certify strict lower and upper limits without floating-point approximations.

claim$4π·11 > 138.230048$ together with companion interval bounds on the alpha seed derived from the eight-tick gap weight $w_8 = (348 + 210√2 - (204 + 130√2)φ)/7$.

background

The module imports W8Bounds, which supplies the parameter-free closed form for the gap weight $w_8$ arising from the eight-tick octave (T7). It also imports the Alpha module to anchor the seed value $4π·11$. These feed interval arithmetic lemmas that certify inequalities for alpha in RS-native units where $c=1$, $ℏ=φ^{-5}$.

proof idea

This is a definition module, no proofs. It consists of named constants and lemmas (alpha_seed_gt, exp_taylor_10_at_048, etc.) that encode Taylor ceilings and error bounds for the exponential at selected points near 0.048.

why it matters in Recognition Science

The module feeds HartreeRydbergScoreCard (P1-C04, P1-C02), Masses.NumericalPredictions, CKMGeometry, ElectronGMinus2ScoreCard (P1-C05), and ElectronMass.Necessity. It supplies the verified alpha interval required for the machine-checked numerical predictions and the T9 necessity argument.

scope and limits

Does not derive the numerical value of alpha from first principles.
Does not extend beyond the listed Taylor orders and seed points.
Does not address renormalization-group running of alpha.
Does not replace the analytic Alpha module with these numeric bounds.

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