interpolation_cost
plain-language theorem explainer
The interpolation cost assigns to each real frequency ratio r the value min(fract(r), 1-fract(r)), vanishing at integers and reaching 1/2 at half-integers. Gravity modelers constructing resonance-aware ILG weight kernels cite this definition when building the function w(r) = 1 + C_lag · interpolation_cost(r). The definition is a direct one-line expression using the fractional part.
Claim. For a real number $r$, the interpolation cost is defined by $c(r) := min({r}, 1 - {r})$, where ${r}$ denotes the fractional part of $r$.
background
In the EightTickResonance module the 8-tick period is fixed at exactly 8, linking to the self-similar fixed point phi from the forcing chain. The interpolation cost quantifies how far a frequency ratio deviates from integer synchronization, which corresponds to perfect ledger-clock alignment. It is the building block for the resonance-aware weight kernel w(r) = 1 + C_lag · interpolation_cost(r), with C_lag = phi^{-5}.
proof idea
The definition is a direct one-line expression that applies the min function to the fractional part of r and its complement to one.
why it matters
This definition supplies the distance-to-integer metric that enters the resonance certificate EightTickResonanceCert and the weight-reduction theorems weight_reduction_at_resonance and w_off_resonance. It realizes the eight-tick octave by penalizing desynchronization inside the gravity kernel, feeding the ILG time-kernel construction that connects to the phi-ladder. No open questions attach to this basic definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.