pith. sign in
module module high

IndisputableMonolith.Constants.GapWeight

show as:
view Lean formalization →

The GapWeight module supplies the canonical gap weight w₈ as a parameter-free closed-form expression that normalizes the projection of the gap onto the fundamental eight-tick basis. Researchers deriving α⁻¹ from the cubic ledger geometry cite this definition to close the gap term in the exponential formula. The module consists of direct definitions and positivity bounds that follow from the eight-tick neutrality axioms imported from the base Constants module.

claimThe canonical gap weight is $w_8 = (348 + 210√2 - (204 + 130√2)φ)/7$, where φ denotes the self-similar fixed point of the Recognition Composition Law.

background

This module belongs to the Constants domain and imports the base Constants module that defines the fundamental RS time quantum τ₀ = 1 tick. It introduces w₈ as the normalized projection weight of the gap onto the eight-tick basis, with the module documentation stating: 'The canonical gap weight w₈ (parameter-free, closed form). This is the normalized projection weight of the gap onto the fundamental 8-tick basis.' Sibling definitions cover the gap function f_gap together with its lower and upper bounds.

proof idea

This is a definition module, no proofs. It introduces the closed-form expression for w8_from_eight_tick, asserts positivity via w8_pos, and records the gap bounds fGapLowerBound and fGapUpperBound as direct consequences of the eight-tick structure.

why it matters in Recognition Science

The gap weight feeds the alpha derivation modules that construct α⁻¹ from vertex deficits of the cubic ledger. It supports the eight-tick window neutrality result, where 'the window-8 neutrality constraints uniquely determine the gap weight w₈ that appears in the α⁻¹ derivation.' It also supplies the gap term required by the exponential form α⁻¹ = α_seed · exp(-f_gap / α_seed) and the numerical bounds used in W8Bounds.

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)