w_resonant
plain-language theorem explainer
The resonance-aware ILG weight kernel is defined by w(r) = 1 + C_lag times the fractional distance of r to the nearest integer. Researchers modeling discrete gravity and resonant mass reduction would cite this kernel when deriving effective weights in eight-tick systems. The definition is a direct algebraic combination of the pre-defined lag constant and interpolation cost function.
Claim. The resonant weight function is $w(r) = 1 + C_{lag} · d(r)$, where $C_{lag} = φ^{-5}$ and $d(r) = min({r}, 1-{r})$ with {r} the fractional part of r.
background
In the EightTickResonance module the weight kernel incorporates lag effects from the Recognition Science framework. C_lag is defined as phi^{-5} approximately 0.09 and represents the RS-derived lag coupling. The interpolation_cost function measures desynchronization as the distance to the nearest integer: min(fract r, 1 - fract r), vanishing at integers and reaching one-half at half-integers.
proof idea
The definition is a direct algebraic expression that adds one to the product of C_lag and interpolation_cost r. It is a one-line wrapper with no tactics beyond unfolding the referenced constants.
why it matters
This definition supplies the core weight kernel for the EightTickResonanceCert structure and the eight_tick_resonance_certified theorem. It realizes the eight-tick octave by modulating weights according to synchronization with the ledger clock and feeds into gravity models where resonant frequencies produce lower effective weight. The construction connects to the ILG time-kernel expressed as a power law in dynamical timescale ratios.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.