pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Constants.GapWeight

show as:
view Lean formalization →

GapWeight supplies the closed-form expression for the canonical gap weight w₈ as the normalized projection onto the fundamental eight-tick basis in Recognition Science. Researchers deriving the fine-structure constant or validating eight-tick neutrality bounds cite this module. The module contains only definitions and explicit bounds with no proofs or derivations.

claim$w_8 = (348 + 210√2 - (204 + 130√2)φ)/7$, where φ denotes the golden ratio. The module also defines the auxiliary gap function $f_{gap}$ together with its lower and upper bounds.

background

The module resides in the Constants domain and imports the parent Constants module, which fixes the fundamental RS time quantum τ₀ = 1 tick. It introduces w₈ as the parameter-free projection weight of the recognition gap onto the eight-tick octave (period 2³) and supplies the closed-form expression together with positivity and bound statements for the related function f_gap.

proof idea

This is a definition module, no proofs. It consists of direct closed-form definitions for w8_from_eight_tick, w8_pos, f_gap, fGapLowerBound, fGapUpperBound and the hypothesis interface f_gap_bounds_hypothesis.

why it matters in Recognition Science

GapWeight supplies the exact w₈ required by the α⁻¹ derivation in Alpha and AlphaDerivation, the exponential form in AlphaExponentialForm, and the eight-tick neutrality connection in WindowNeutrality. It also supports the numerical bounds certificate in GapWeightNumericsScaffold and the W8 interval bounds. The module closes the structural step that feeds the unification predictions in ConstantsPredictionsProved and RegistryPredictionsProved.

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)