f_gap_bounds_hypothesis
plain-language theorem explainer
The declaration defines the proposition that the gap weight lies strictly between two fixed rational bounds. Researchers certifying the alpha pipeline constants would cite it to enforce numerical control without free parameters. The definition is a direct conjunction of the precomputed lower and upper inequalities.
Claim. Let $f_ {gap} = w_8 ln phi$ where $phi$ is the golden ratio and $w_8$ is the eight-tick projection weight. The hypothesis asserts $L < f_{gap} < U$, with $L$ and $U$ the rationals $2993443258792019287026689/2500000000000000000000000$ and $5986887286510633232418913/5000000000000000000000000$ cast to reals.
background
The GapWeight module defines the gap term as $f_{gap} = w8_from_eight_tick * ln phi$, replacing earlier numeric certificates to uphold the no-free-parameters requirement. The module doc states that $w8_from_eight_tick$ is the normalized DFT-8 neutral spectral deficit weight on the canonical phi-pattern. Upstream, AlphaHigherOrder.f_gap supplies the form $w8 * log phi$, while fGapLowerBound and fGapUpperBound supply the explicit rational endpoints. The LawOfExistence.Constants structure bundles related CPM parameters such as Knet and Cproj.
proof idea
This is a direct definition of the bounding proposition. It assembles the conjunction of the strict lower inequality using fGapLowerBound and the strict upper inequality using fGapUpperBound, both cast to reals and compared against the already-defined f_gap.
why it matters
The hypothesis supplies certified numerical control on the gap weight that enters the alpha pipeline and the master gap generator at z=1. It directly supports the module's shift from numeric certificates to a parameter-free closed form tied to the eight-tick octave. No downstream uses are recorded yet, leaving open its integration into broader constant derivations or the LawOfExistence bundle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.