module module high

`IndisputableMonolith.Gravity.EightTickResonance`

The EightTickResonance module defines the interpolation cost for frequency ratios relative to integer synchronization and builds resonant weights from it. Researchers modeling acoustic levitation or gravity resonances in Recognition Science would cite these objects. The module consists of direct definitions and elementary lemmas on the fractional-part distance, with no complex derivations.

claimThe interpolation cost is $C(r) = min({r}, 1-{r})$, where ${r}$ is the fractional part of the frequency ratio $r$. Resonant weight functions satisfy $w(r) = 1-2C(r)$ at resonance and drop off-resonance, with resonant frequency extracted from the eight-tick period.

background

The module sits inside the gravity domain and imports the RS time quantum from Constants, where the doc-comment states: 'The fundamental RS time quantum (RS-native). τ₀ = 1 tick.' It introduces the interpolation cost as the distance to the nearest integer, zero at synchronized ledger ticks and 1/2 at half-integers. Additional definitions cover C_lag, resonant weights w_resonant, and the resonant frequency, all expressed in RS-native units with c=1.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The definitions feed directly into the AcousticPhaseLevitation module for phase-synchronization calculations. They instantiate the eight-tick octave (T7) of the forcing chain, supplying the cost and weight primitives needed to connect frequency ratios to gravitational resonance without invoking the full J-function or RCL.

scope and limits

Does not derive the eight-tick period from the forcing chain.
Does not compute numerical values for physical resonant frequencies.
Does not relate interpolation cost to the J-cost or mass ladder.
Does not address spatial dimension D=3 or alpha-band constraints.

used by (1)

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

IndisputableMonolith.Gravity.AcousticPhaseLevitation module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (24)

def interpolation_cost L32
theorem interpolation_cost_nonneg L35
theorem interpolation_cost_le_half L39
theorem interpolation_cost_zero_at_integer L46
def C_lag L54
theorem C_lag_pos L56
def w_resonant L64
theorem w_resonant_ge_one L67
theorem w_at_resonance L72
theorem w_off_resonance L77
theorem weight_reduction_at_resonance L84
def resonant_frequency L94
theorem resonant_frequency_pos L97
theorem resonant_frequency_decreasing L104
structure EightTickResonanceCert L121
theorem eight_tick_resonance_certified L127
theorem C_lag_eq_cLagLock_inv L146
theorem w_resonant_bounded_above L151
theorem eight_tick_period L159
def w_total L187
theorem w_total_at_resonance L191
theorem w_total_exceeds_secular L196
theorem resonance_weight_reduction_ratio L205
theorem shared_coupling L214