f_gap_lt
plain-language theorem explainer
The product of the eight-tick gap weight and the natural logarithm of the golden ratio is bounded above by 1.203. Interval workers tightening the Recognition Science prediction for the inverse fine-structure constant cite this result. The proof chains two multiplication inequalities on the supplied upper bounds for each factor and closes with a numerical check.
Claim. $w_8 log phi < 1.203$, where $w_8$ is the eight-tick gap weight and $phi = (1 + sqrt(5))/2$ the golden ratio.
background
The module supplies rigorous interval bounds on alpha inverse using the Recognition derivation. The gap term is defined as the product of the eight-tick gap weight and log of the golden ratio, serving as a first-order curvature correction in the alpha expression. The eight-tick gap weight is the normalized projection onto the 8-tick basis, given in closed form by (348 + 210 sqrt(2) - (204 + 130 sqrt(2)) phi)/7. Upstream, w8_pos establishes its positivity while log_phi_lt_0483 supplies the concrete upper bound log phi < 0.483.
proof idea
Tactic-mode calc block. It pulls w8_computed_lt and log_phi_lt_0483, asserts w8 positivity, then applies mul_lt_mul_of_pos_left to replace log phi by 0.483, followed by mul_lt_mul_of_pos_right to replace w8 by its upper bound, and finishes with norm_num to confirm the product lies below 1.203.
why it matters
The bound is invoked inside alphaInv_gt to obtain alphaInv > 137.030, closing the lower edge of the predicted interval (137.030, 137.039). It supports the T7 eight-tick octave and the alpha band in the Recognition framework. No open question is directly addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.