Pith. sign in
module module high

IndisputableMonolith.Constants.GapWeight

show as:
view Lean formalization →

Defines the canonical gap weight w₈, the parameter-free normalized projection of the recognition gap onto the fundamental eight-tick basis (numerically ≈ 2.49057). Also introduces the derived gap load f_gap and its bound interface. Cited by the α⁻¹ construction, window-neutrality, and registry numerics. Definition-and-bounds module: closed-form w₈ plus positivity and hypothesis-shaped interval claims.

claimThe module fixes the canonical gap weight $w_8$ as the normalized projection of the recognition gap onto the fundamental eight-tick (period $2^3$) basis, gives a closed parameter-free form with $w_8>0$, and defines the gap load $f_{\mathrm{gap}}$ together with lower/upper bound hypotheses used in the $\alpha^{-1}$ dressing.

background

Recognition Science forces an eight-tick octave (T7: period $2^3$) as the minimal neutral ledger window. The gap that remains after exact eight-tick neutrality must be projected onto that basis; the resulting scalar weight is $w_8$. The module doc states it is parameter-free and closed-form, with numerical value approximately $2.49056927545\ldots$.

Upstream, Constants supplies the RS-native tick $\tau_0=1$. Downstream measurement work (WindowNeutrality) records that window-8 neutrality constraints uniquely determine this same $w_8$ appearing in the $\alpha^{-1}$ derivation. The sibling surface exposes $w_8$ from the eight-tick construction, positivity, the gap function $f_{\mathrm{gap}}$, and a bounds hypothesis interface.

In the alpha pipeline the seed is dressed by a factor involving $f_{\mathrm{gap}}$; the exponential form module writes the canonical display $\alpha^{-1}=\alpha_{\mathrm{seed}}\cdot\exp(-f_{\mathrm{gap}}/\alpha_{\mathrm{seed}})$. Thus $w_8$ and $f_{\mathrm{gap}}$ are the concrete bridge from eight-tick geometry to the fine-structure dressing.

proof idea

This is a constants definition module, not a deep proof development. It introduces the closed-form gap weight from the eight-tick basis, records positivity, defines $f_{\mathrm{gap}}$, and packages lower/upper bound claims as a hypothesis interface (with a separate numerics scaffold module for certificate work). No multi-step forcing argument lives here; consumers import the symbols and discharge or assume the bound hypothesis as needed.

why it matters in Recognition Science

Without a fixed $w_8$, the $\alpha^{-1}$ seed-dressing chain has no canonical gap load. Downstream importers include Constants.Alpha, AlphaDerivation (cubic-ledger seed assembly; exact IR $\alpha^{-1}(0)$ still OPEN), AlphaExponentialForm (Gap B: structural analysis of $\exp(-f_{\mathrm{gap}}/\alpha_{\mathrm{seed}})$), and AlphaGenesis.ResummationForcing (theorem that factorizing unit-linear dressing responses are exactly $\varepsilon\mapsto\exp(-\varepsilon)$).

WindowNeutrality ties eight-tick neutrality to ledger exactness and states that those constraints uniquely determine the gap weight used in $\alpha^{-1}$. Numerics consumers (GapWeightNumericsScaffold, Interval.W8Bounds) and Unification.RegistryPredictionsProved pin the floating value and registry claims. Landmark contact: T7 eight-tick octave and the RS alpha band target near $137.03$–$137.04$.

scope and limits

used by (10)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)