codata_in_band

The Explicit Alpha Derivation module traces the provenance chain from the J-uniqueness theorem through the forced phi fixed point and D=3 (from the eight-tick period) to the 44-slot frequency structure that yields the RS alpha formula. The lower bound is defined as 137.030 and the upper bound as 137.039, while the CODATA value is fixed at 137.035999084. Upstream, the alpha definition supplies the fine-structure constant as the reciprocal of its inverse, and the from theorem reduces seven axioms to four structural conditions plus three definitional facts.

The term proof applies constructor to split the conjunction into two goals. It then passes the definitions of alphaInverseLower, alphaInverseUpper, and codataAlphaInverse to norm_num, which reduces both inequalities to decidable numeric comparisons that evaluate directly.

This result supplies the codata_in_band field of the AlphaProvenanceCert structure, which certifies the full chain from uniqueness to the alpha match. The module documentation presents it as part of the structural theorem confirming that the experimental value lies inside the RS band. In the framework it closes the verification step for the fine-structure constant after the T5 J-uniqueness, T6 phi fixed point, T7 eight-tick octave, and T8 D=3 steps.