gap_weight_pos
plain-language theorem explainer
The gap weight w₈, the normalized projection onto the eight-tick basis, is strictly positive. Researchers deriving the fine-structure constant from Recognition Science neutrality constraints would cite this when confirming parameter signs in the α⁻¹ formula. The proof is a direct one-line application of the closed-form positivity result for w₈.
Claim. $0 < w_8$, where $w_8 = (348 + 210 sqrt(2) - (204 + 130 sqrt(2)) phi)/7$ is the canonical gap weight obtained from eight-tick window neutrality.
background
The module axiomatizes eight-tick neutrality and its link to ledger exactness, extending to the gap weight w₈ that enters the α⁻¹ derivation via scheduler invariants such as sumFirst8 and blockSumAligned8. The upstream definition supplies the closed-form expression for w₈ as the normalized projection of the gap onto the fundamental 8-tick basis, numerically near 2.49057. The companion theorem w8_pos supplies the positivity claim for this explicit formula.
proof idea
One-line wrapper that applies the theorem w8_pos from Constants.GapWeight, which itself uses rational bounds on sqrt(2) and phi to show the numerator remains positive.
why it matters
Secures positivity of w₈ for the α⁻¹ derivation that follows from eight-tick neutrality constraints. It fills the T7 eight-tick octave step in the forcing chain and supports the module claim that window-8 neutrality uniquely determines the gap weight appearing in the fine-structure formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.