fGapUpperBound
plain-language theorem explainer
The declaration defines a specific rational as the upper bound for the gap weight f_gap in the Recognition Science constants pipeline. Researchers certifying the w8 projection in the eight-tick octave would cite this value to close the numerical enclosure around the computed gap term. It is introduced by direct assignment of the rational literal chosen to satisfy the strict inequality required by the bounds hypothesis.
Claim. The upper bound on the gap weight is the rational number $5986887286510633232418913 / 5000000000000000000000000$.
background
In the GapWeight module the gap weight w8 is the normalized 8-tick projection weight on the canonical phi-pattern, entering the gap term as f_gap = w8 ln(phi). The module documentation requires this weight to be parameter-free and obtained from the normalized DFT-8 neutral spectral deficit after the projection step that distinguishes it from raw sums.
proof idea
This is a direct definition that assigns the explicit rational literal 5986887286510633232418913 / 5000000000000000000000000. No lemmas from the upstream list are applied; the body is a hardcoded constant chosen to serve as the upper endpoint.
why it matters
The definition supplies the upper rational used by the downstream f_gap_bounds_hypothesis to assert that the computed f_gap lies strictly between the lower and upper bounds. It supports the no-free-parameters claim for w8 in the eight-tick octave (T7) of the forcing chain and closes the transition from earlier numeric certificates to the canonical projection weight.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.