w8_pos
plain-language theorem explainer
Positivity of the eight-tick gap weight w₈ follows from rational bounds on √2, √5 and φ. Workers on the α pipeline invoke it to guarantee the gap term f_gap stays positive before deriving interval bounds. The tactic proof substitutes worst-case upper bounds on φ and √2, verifies the numerator remains positive by linear arithmetic, then unfolds the closed-form definition to obtain the quotient inequality.
Claim. $0 < w_8$ where $w_8 = (348 + 210√2 - (204 + 130√2)φ)/7$ and φ denotes the golden ratio.
background
The gap weight w₈ supplies the coefficient in the gap term f_gap = w₈ ln(φ) inside the α pipeline. The module defines it as the normalized projection weight of the gap onto the fundamental 8-tick basis, given explicitly by the closed form (348 + 210√2 − (204 + 130√2)φ)/7. This expression is parameter-free and replaces earlier numeric certificates.
proof idea
The proof first establishes rational bounds √2 < 71/50, √5 < 56/25, φ < 81/50 and φ > 21/13 via Real.sqrt_lt and linarith. It shows the coefficient of φ is non-positive from the lower bound on φ. Upper bounds are substituted into the numerator; norm_num confirms the resulting rational is positive, nlinarith propagates the inequality, and mul_le_mul_of_nonpos_right handles the √2 term. Ring rewrites the expression, after which the definition is unfolded and div_pos yields the result.
why it matters
This theorem is invoked directly by gap_weight_pos in Measurement.WindowNeutrality and by the interval bounds f_gap_gt, f_gap_gt_strong and f_gap_lt in Numerics.Interval.AlphaBounds. Those results feed the unification lemmas alpha_lt_0_1 and alphaInv_gt_2. It thereby anchors positivity for the structural bound on 1/α and closes the eight-tick projection step in the gap-weight construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.