pith. sign in
module module high

IndisputableMonolith.Constants.GapWeight

show as:
view Lean formalization →

The GapWeight module supplies the canonical gap weight w8 as a parameter-free closed form from the eight-tick basis. Alpha derivation modules cite this normalized projection weight when constructing the exponential form of alpha inverse. The module consists entirely of definitions and supporting bounds with no internal proofs.

claimThe gap weight is the normalized projection of the gap onto the fundamental 8-tick basis, given explicitly by the closed form $w_8 = (348 + 210\sqrt{2} - (204 + 130\sqrt{2})\phi)/7$ where $\phi$ denotes the golden ratio.

background

This module belongs to the Constants domain and imports the base Constants module whose sole content is the definition of the fundamental RS time quantum $\tau_0 = 1$ tick. Recognition Science places the eight-tick octave at T7 of the forcing chain; the gap weight w8 is the normalized projection of the gap onto that basis. The module also introduces the auxiliary objects w8_pos, f_gap, and the hypothesis f_gap_bounds_hypothesis that later bound the gap function appearing in the alpha exponential form.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the alpha derivation in Constants.Alpha and Constants.AlphaDerivation, the exponential-form analysis in AlphaExponentialForm, and the eight-tick neutrality axioms in Measurement.WindowNeutrality. It supplies the explicit weight required by the T7 eight-tick octave landmark and by the gap term in the alpha inverse formula. Downstream numerics modules such as W8Bounds and GapWeightNumericsScaffold rely on the closed form for interval bounds and match certificates.

scope and limits

used by (8)

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 (6)