w8Interval
plain-language theorem explainer
The definition supplies a closed real interval [2.490564399, 2.490572090] that brackets the gap weight w8 from the eight-tick construction. Researchers checking numerical consistency of alpha inverse bounds cite this interval to anchor computations. It is a direct assignment of the Icc constructor to two hardcoded rational endpoints.
Claim. Define the closed interval $I := [2.490564399, 2.490572090] = [2490564399/1000000000, 2490572090/1000000000] subset mathbb{R}$ as the bounding set for the gap weight $w_8$ in alpha inverse estimates.
background
The W8 Numerical Bounds module treats the gap weight w8 as the parameter-free closed form (348 + 210 sqrt(2) - (204 + 130 sqrt(2)) phi)/7, where phi denotes the golden ratio. The module supplies tight numerical intervals around the approximate value 2.490569 by importing GapWeight and using sibling bounds on sqrt(2) and phi. This definition records one such interval for downstream use in alphaInv bounds.
proof idea
The declaration is a direct definition that constructs Set.Icc with the explicit lower rational 2490564399/1000000000 and upper rational 2490572090/1000000000.
why it matters
The interval anchors numerical checks for the gap weight arising in the eight-tick octave (T7). It supports verification that alpha inverse lies inside the predicted band (137.030, 137.039) by supplying a concrete set containing the exact w8 value. The definition closes a numerical scaffolding step that feeds alphaInv bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.