f_gap_gt
plain-language theorem explainer
The theorem establishes a strict lower bound of 1.195 on the gap term f_gap, defined as the product of the eight-tick weight w8 and the natural logarithm of the golden ratio phi. Researchers tightening numerical intervals for the inverse fine-structure constant in Recognition Science cite this result when verifying the alpha band. The proof is a tactic-mode calc chain that starts from a norm_num base inequality and lifts it via two applications of mul_lt_mul_of_pos using supplied lower bounds on w8 and log phi together with positivity of w8.
Claim. $1.195 < w_8 log phi$ where $w_8$ is the canonical gap weight from the eight-tick projection and $phi$ is the golden ratio.
background
The module supplies rigorous interval bounds on the inverse fine-structure constant alphaInv via symbolic derivations. The gap term f_gap is defined as w8_from_eight_tick times Real.log phi, where w8_from_eight_tick is the normalized projection weight onto the fundamental 8-tick basis given by the closed-form expression (348 + 210 sqrt(2) - (204 + 130 sqrt(2)) phi)/7. Upstream results include the positivity theorem w8_pos and the equivalent definition of f_gap in AlphaHigherOrder as a first-order curvature correction.
proof idea
The proof unfolds the definition of f_gap by simp, obtains the lower bound w8_computed_gt from W8Bounds and log_phi_gt_048, invokes w8_pos for positivity, and applies a calc block. The chain begins with the norm_num fact 1.195 < 2.490564399 * 0.48, then uses mul_lt_mul_of_pos_right to replace the constant by w8, and mul_lt_mul_of_pos_left to replace 0.48 by log phi.
why it matters
This supplies a concrete numerical floor on the gap correction term that enters the interval estimates for alpha inverse near 137.03. It draws on the eight-tick structure through w8_from_eight_tick and supports the overall alpha band claim in the Recognition framework. No downstream uses appear in the current graph, indicating it functions as a terminal numerical anchor in the AlphaBounds module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.