w8_value
plain-language theorem explainer
Gap weight w₈ from the eight-tick basis satisfies |w₈ - 2.490569275454| < 5×10^{-6}. Recognition Science numerics work cites this for compatibility checks against legacy constant tables. The short proof imports the certified interval bounds and reduces the claim via absolute-value rewriting plus linear arithmetic.
Claim. Let $w_8 = (348 + 210 sqrt(2) - (204 + 130 sqrt(2)) phi)/7$ be the gap weight from the eight-tick projection. Then $|w_8 - 2.490569275454| < 5 times 10^{-6}$.
background
The GapWeight module defines w8_from_eight_tick as the normalized projection weight of the gap onto the fundamental 8-tick basis, given by the closed form (348 + 210 sqrt(2) - (204 + 130 sqrt(2)) phi)/7. The present module supplies numeric match certificates for this expression. Upstream theorem w8_matches_certified establishes the tighter interval 2.490564399 < w8_from_eight_tick < 2.490572090 by invoking verified bounds from Numerics.W8Bounds.
proof idea
The proof invokes w8_matches_certified to obtain the interval bounds, rewrites the target via abs_lt, and discharges both resulting inequalities with linarith.
why it matters
This supplies a numeric anchor for the gap weight w₈ in the eight-tick octave (T7) of the forcing chain. It supports the abstract Constants bundle in LawOfExistence by providing a verified approximation for legacy code. The declaration closes a compatibility interface without altering the parameter-free closed form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.