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, with closed form and numerical value ~2.49057. Also introduces the derived gap function f_gap and its bound hypotheses used in the α⁻¹ dressing. Cited by every Alpha construction path and by eight-tick window neutrality. The module is definitional plus positivity and bound scaffolding.

claimThe gap weight $w_8$ is the normalized projection weight of the recognition gap onto the fundamental 8-tick basis (closed form, parameter-free), with $w_8 \approx 2.49056927545$. The module also defines the gap function $f_{\mathrm{gap}}$ built from $w_8$, positivity $w_8 > 0$, and lower/upper bound hypotheses on $f_{\mathrm{gap}}$.

background

Recognition Science forces an eight-tick octave (T7: period $2^3$) as the fundamental discrete time window. The gap that appears when projecting continuous recognition cost onto this basis carries a unique normalized weight $w_8$, independent of free parameters.

This module sits under Constants (where the RS time quantum is $\tau_0 = 1$ tick) and packages that weight together with the derived gap load $f_{\mathrm{gap}}$ used in the fine-structure dressing. Downstream Alpha modules write the canonical formula $\alpha^{-1} = \alpha_{\mathrm{seed}} \cdot \exp(-f_{\mathrm{gap}}/\alpha_{\mathrm{seed}})$; the seed itself comes from cubic-ledger combinatorics, while $f_{\mathrm{gap}}$ is the infrared gap content controlled by $w_8$.

Window neutrality (Measurement) axiomatizes that eight-tick neutrality plus ledger exactness uniquely fix this same $w_8$, so the constant here is the shared interface between the geometric seed and the exponential dressing.

proof idea

Definition module. It introduces the closed-form constant $w_8$ (via an eight-tick construction), proves positivity, and defines $f_{\mathrm{gap}}$ together with named lower/upper bound hypotheses. No deep derivation is proved here; numeric match and bound discharge live in sibling scaffolds (GapWeightNumericsScaffold, W8Bounds). The argument structure is: define $w_8$ from the 8-tick basis, record $w_8 > 0$, package $f_{\mathrm{gap}}$ and its bound interface for Alpha consumers.

why it matters in Recognition Science

Every Alpha path imports this module: Constants.Alpha, AlphaDerivation (seed assembly from the cubic ledger), AlphaExponentialForm (structural analysis of $\alpha^{-1} = \alpha_{\mathrm{seed}}\exp(-f_{\mathrm{gap}}/\alpha_{\mathrm{seed}})$), and AlphaGenesis.ResummationForcing (the theorem that any factorizing unit-linear dressing is exactly $\varepsilon \mapsto \exp(-\varepsilon)$). Measurement.WindowNeutrality cites $w_8$ as the unique weight fixed by eight-tick neutrality. Numerics (W8Bounds, GapWeightNumericsScaffold) and Unification.RegistryPredictionsProved consume the same constant. Without a single canonical $w_8$, the $\alpha$ band and gap-dressed predictions would not share a common interface. Ties directly to T7 (eight-tick octave) and the open exact $\alpha^{-1}(0)$ boundary condition.

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)