f_gap_gt_strong
plain-language theorem explainer
f_gap exceeds 1.1979 using the eight-tick gap weight and a lower bound on log φ. Interval analysts tightening bounds on the inverse fine-structure constant cite this result. The proof chains a precomputed lower bound on w8 with log φ > 0.481 via two applications of multiplication inequalities for positive terms.
Claim. $f_mathrm{gap} > 1.1979$ where $f_mathrm{gap} = w_8 log phi$ and $phi = (1 + sqrt{5})/2$ is the golden ratio.
background
The module supplies interval bounds on alphaInv from the Recognition Science constants. f_gap is defined as w8_from_eight_tick times the natural logarithm of phi. Upstream results establish that w8_from_eight_tick is the normalized projection weight onto the 8-tick basis (approximately 2.490569) and is positive, while log_phi_gt_0481 proves log phi > 0.481 by comparing the exponential of 0.481 against a rational lower bound on phi.
proof idea
The proof simplifies the definition of f_gap. It introduces the lower bound w8_computed_gt on w8_from_eight_tick, the lemma log_phi_gt_0481, and the positivity theorem w8_pos. A calc chain then verifies the numerical seed inequality 1.1979 < 2.490564399 * 0.481, multiplies the w8 lower bound on the right, and replaces the constant 0.481 by log phi on the left using mul_lt_mul_of_pos_left.
why it matters
This bound is invoked by alphaInv_lt to obtain alphaInv < 137.039, placing the result inside the Recognition Science alpha band (137.030, 137.039). It strengthens the gap contribution that originates from the eight-tick octave (T7) in the forcing chain and the phi-ladder mass formula. The declaration closes a concrete numerical step required for the interval estimate on the inverse fine-structure constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.