module module high

`IndisputableMonolith.Gravity.EightTickResonance`

This module defines the interpolation cost for frequency ratios and associated resonant weights in the eight-tick gravity setting. Modelers of acoustic levitation or ledger-synchronized resonances cite these objects to quantify synchronization penalties. It consists entirely of definitions and elementary properties of the cost function.

claimThe interpolation cost is $C(r) = \min(\{r\}, 1-\{r\})$ for frequency ratio $r$, equaling zero at integers and $1/2$ at half-integers. Resonant weight functions $w$ satisfy $w \ge 1$ exactly when $C(r) = 0$.

background

The module sits inside the gravity domain and imports the RS time quantum $\tau_0 = 1$ tick from Constants. Its central object is the interpolation cost, which measures distance of a frequency ratio to the nearest integer and therefore to ledger-clock synchronization. Sibling definitions introduce non-negative cost bounds, zero cost at integers, positive resonant weights, and a resonant-frequency predicate.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the resonance primitives consumed by AcousticPhaseLevitation. It implements the eight-tick octave (T7) component of the forcing chain by furnishing the cost and weight machinery needed for phase-locked gravitational effects.

scope and limits

Does not derive equations of motion or field equations.
Does not compute numerical spectra or coupling constants.
Does not address spatial dimension D=3 or the phi-ladder.
Does not contain any theorem with a sorry or external hypothesis.

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