candidate_1_bounds

This module studies the ~0.001 additive correction δ₂ needed to close the 8 ppm gap between the Recognition Science inverse fine-structure constant α⁻¹_RS ≈ 137.0349 and the CODATA value 137.035999206(21). Admissible corrections must be built from counting-layer integers and the transcendentals π, φ, stay O(10⁻³), introduce no free parameters, and admit a cube-geometry reading.

Candidate 1 is the explicit real 1/(102 π²). The factor 102 is the same seam denominator that already appears in the curvature term 103/(102 π⁵) of α⁻¹_RS; replacing π⁵ by π² is read as a lower-order curvature correction from face × wallpaper channels. Numerically 102 π² ≈ 1006.08, so the candidate is ≈ 0.000994, about 10% below the target δ₂ ≈ +0.00110.

The theorem supplies certified decimal enclosures of that value, using only the standard six-decimal bounds on π and elementary positivity and order facts for multiplication and division.

Split the conjunction. For the lower bound, unfold the definition and use positivity of the denominator 102 π². From π < 3.141593 obtain π² < (3.141593)², scale by 102, and compare to the decimal 1007.049 by norm_num. Multiplying the resulting upper bound on the denominator by 0.000993 stays strictly below 1, so lt_div_iff₀ yields 0.000993 < 1/(102 π²).

The upper bound is symmetric: from 3.141592 < π obtain a strict lower bound 1004.017 < 102 π², multiply by 0.000996 to exceed 1, and apply div_lt_iff₀. Both sides are pure interval arithmetic; no Recognition-specific lemmas beyond the definition of the candidate are required.

Within the alpha-correction analysis, this is the first certified numerical placement of a cube-geometry candidate against the structural target δ₂ ≈ 0.00110. The primer landmark is the RS α⁻¹ band (137.030, 137.039): the existing seed 4π·11 − w₈ ln φ + 103/(102 π⁵) already lands inside that band, and δ₂ is the residual needed to match CODATA at the ppm level.

The candidate reuses the seam integer 102 from the curvature term, so a positive match would have been a parameter-free combinatorial correction. The bound shows it is ~10% low, which is why sibling candidates (1/824, and others) are evaluated next. No downstream theorem currently consumes the bound (used_by is empty); it is a local verification fact that any later selection or rejection of candidate 1 can quote without re-running floating-point checks.