alpha_cube_bounds
plain-language theorem explainer
The lemma establishes that the cube of the fine-structure constant satisfies 0.000000388 < alpha^3 < 0.000000389. Researchers deriving the electron mass in the Recognition Science T9 necessity chain cite it to bound error propagation in radiative corrections. The proof applies the prior alpha interval lemma, invokes monotonicity of cubing via nlinarith, and closes the numerical gaps with norm_num comparisons.
Claim. $0.000000388 < {alpha}^3 < 0.000000389$, where $alpha$ denotes the fine-structure constant.
background
The module develops T9 necessity, showing that the electron mass formula is forced once T8 ledger quantization and the geometric constants (including alpha) are fixed. Alpha is defined as the reciprocal of the derived inverse fine-structure constant and lies in the narrow interval (0.007297, 0.0072977) by the sibling lemma alpha_bounds, which itself rests on the numeric bounds alphaInv_gt and alphaInv_lt imported from Numerics.Interval.AlphaBounds. The local setting is therefore a chain of interval propagations that keep all derived quantities inside the Recognition Science phi-ladder and eight-tick octave constraints.
proof idea
The tactic proof first obtains the alpha interval from the sibling alpha_bounds lemma. It then splits into two goals. For the lower bound it uses nlinarith on the squared non-negativity facts to establish (0.007297)^3 < alpha^3, followed by a calc chain that inserts the target constant via norm_num. For the upper bound the same pattern is applied with the tighter 0.0072977 upper limit on alpha, again closing with norm_num.
why it matters
This bound is the immediate predecessor of radiative_correction_bounds, which feeds the final electron-mass necessity theorem in the same module. It therefore closes the numeric control step required by the T9 forcing chain (T5 J-uniqueness through T8 D=3) once alpha has been obtained from the RCL and phi-ladder. The declaration touches no open scaffolding; it simply propagates the already-proved alpha interval into the cubic term needed for the radiative correction estimate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.