w8_computed_gt
plain-language theorem explainer
The theorem establishes that the eight-tick gap weight exceeds 2.490564399. Researchers verifying Recognition Science constants cite it when anchoring interval bounds for the gap term inside alpha calculations. The tactic proof substitutes upper bounds on phi and sqrt(2), proves the expression is monotone decreasing in each variable, evaluates the resulting corner value directly, and chains the inequalities back to the true w8.
Claim. $2.490564399 < w_8$ where $w_8 = (348 + 210 sqrt(2) - (204 + 130 sqrt(2)) phi)/7$ and $phi$ is the golden ratio.
background
The module supplies rigorous numerical bounds for the gap weight w8_from_eight_tick, defined as the closed-form expression (348 + 210 sqrt(2) - (204 + 130 sqrt(2)) phi)/7. This quantity is the normalized projection weight of the gap onto the fundamental 8-tick basis. The local setting is the W8 Numerical Bounds section, which uses tight intervals for phi and sqrt(2) to certify inequalities without external floating-point libraries.
proof idea
The proof imports the upstream bounds sqrt(2) <= 1.4143 and phi < 1.6180340. It first shows that raising phi lowers the expression because the coefficient of phi is negative, then fixes phi at its upper bound and shows that raising sqrt(2) also lowers the value because the coefficient (210 - 130 phi) is negative. These two monotonicity steps produce a corner value at the upper bounds. Direct norm_num confirms the corner exceeds 2.490564399; le_trans then chains the inequalities to the unfolded w8_from_eight_tick.
why it matters
This result supplies the lower half of the certified interval used by gap_weight_approx and w8_matches_certified. Those theorems feed f_gap_gt and f_gap_gt_strong in the alpha bounds module. Within the framework it closes the numerical verification step for the eight-tick octave, ensuring the gap weight lies inside (2.490564399, 2.490572090) and thereby supporting the alpha inverse band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.