interpolation_cost_zero_at_integer
plain-language theorem explainer
The theorem establishes that the interpolation cost vanishes exactly when the frequency ratio is an integer. Workers on resonance in the Recognition Science gravity model cite it to anchor perfect synchronization at integer multiples of the ledger clock. The proof is a direct term reduction that unfolds the cost definition and simplifies the fractional part of an integer cast.
Claim. For every integer $n$, the distance to the nearest integer of the real number $n$ is zero, where this distance (the interpolation cost) is given by $min({r},1-{r})$ and ${r}$ denotes the fractional part of $r$.
background
The Gravity.EightTickResonance module constructs a resonance-aware weight kernel for gravitational source terms. The interpolation cost of a frequency ratio $r$ is the distance to the nearest integer, returning zero at exact integers and a maximum of one-half at half-integers; it is defined via the minimum of the fractional part and its complement. The lag coupling $C_{lag}$ equals $phi^{-5}$ and scales the linear penalty inside the weight function $w_{resonant}$.
proof idea
The proof is a one-line term reduction: it unfolds the interpolation cost definition and applies the simplification rule that the fractional part of an integer cast to the reals is zero.
why it matters
This identity supplies the base case for the downstream theorem w_at_resonance, which asserts that the resonant weight kernel equals one. It realizes the integer synchronization step inside the eight-tick octave (T7), where exact alignment with the ledger clock removes the lag penalty. The result thereby supports the claim that resonance minimizes effective gravitational coupling strength.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.