fGapLowerBound
plain-language theorem explainer
This definition supplies the explicit rational lower bound for the gap weight f_gap in the Recognition Science constants pipeline. Researchers deriving the fine-structure constant alpha would cite the bound when certifying that the computed f_gap lies strictly inside the supplied interval. The declaration is a direct constant definition with no lemmas or computational steps.
Claim. The lower bound for the gap weight is the rational number $2993443258792019287026689 / 2500000000000000000000000$.
background
The GapWeight module defines the single gap term as $f_{gap} = w_8 · ln(φ)$, where $w_8$ is the 8-tick projection weight obtained from the canonical φ-pattern. The module replaces earlier numeric certificates with parameter-free closed forms to uphold the no-free-parameters claim. The supplied lower bound is paired with a matching upper bound inside the hypothesis f_gap_bounds_hypothesis, which asserts the strict inequality ((fGapLowerBound : ℚ) : ℝ) < f_gap ∧ f_gap < ((fGapUpperBound : ℚ) : ℝ).
proof idea
The declaration is a direct definition of a fixed rational constant.
why it matters
The bound enters the hypothesis f_gap_bounds_hypothesis that certifies the numerical range of f_gap inside the alpha pipeline. It supports the closed-form w8_from_eight_tick, the normalized DFT-8 neutral spectral deficit weight on the 8-tick basis (T7 eight-tick octave). The definition closes the numeric-certificate requirement for the framework constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.