w8_computed_lt
plain-language theorem explainer
The theorem certifies that the gap weight w8, given by the closed form (348 + 210√2 − (204 + 130√2)φ)/7, satisfies w8 < 2.490572090. Researchers verifying numerical intervals for Recognition Science constants cite it to close the certified range around the computed value ≈2.490569. The proof obtains the bound by substituting the supplied lower estimates for √2 and φ, proving the expression is monotone in each variable so that the corner yields an upper bound, then confirming the numeric corner lies below the target.
Claim. $w_8 < 2.490572090$ where $w_8 = (348 + 210√2 − (204 + 130√2)φ)/7$.
background
The module supplies tight numerical bounds on the gap weight w8_from_eight_tick, the normalized projection of the gap onto the eight-tick basis. Its definition is the parameter-free expression (348 + 210√2 − (204 + 130√2)φ)/7, which evaluates to approximately 2.490569. The upstream result w8_from_eight_tick supplies this closed form; alphaInv supplies the related dimensionless inverse fine-structure constant obtained from the structural seed and gap.
proof idea
Lower bounds on √2 and φ are imported from the sibling results sqrt2_gt_14142 and phi_gt_161803395. Monotonicity is established in two steps: the coefficient of φ is negative, so replacing φ by its lower bound increases the expression; the coefficient of √2 is likewise negative once φ is fixed, so replacing √2 by its lower bound increases it further. The resulting corner value is shown strictly less than 2.490572090 by norm_num. The definition of w8 is unfolded and the chain is closed by lt_of_le_of_lt.
why it matters
The bound is invoked directly by gap_weight_approx to obtain the interval 2.490 < w8 < 2.491 and by w8_matches_certified to certify the tighter interval (2.490564399, 2.490572090). It is also used in f_gap_lt to bound the gap term appearing in alphaInv. Within the framework it numerically anchors the eight-tick octave (T7) and supplies the concrete value of the gap weight that enters the mass formula and the alpha band (137.030, 137.039).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.