interpolation_cost_nonneg
plain-language theorem explainer
The theorem proves that the interpolation cost of any real frequency ratio r is nonnegative. Researchers analyzing resonant weights in the eight-tick gravity model cite it to bound the weight kernel from below. The proof is a term-mode one-liner that unfolds the definition and applies le_min to the nonnegativity of the fractional part together with a linarith step on its complement.
Claim. For every real number $r$, the interpolation cost satisfies $0 ≤ min({r}, 1 - {r})$, where ${r}$ denotes the fractional part of $r$.
background
The interpolation cost is defined as min(Int.fract r, 1 - Int.fract r). It quantifies distance to the nearest integer: zero at synchronized integers and one-half at half-integers. The module Gravity.EightTickResonance develops weight kernels for frequencies in the eight-tick octave of the Recognition Science gravity model. The upstream definition of interpolation_cost supplies the explicit min expression used here.
proof idea
The proof is a term-mode one-liner. It unfolds interpolation_cost and invokes le_min on Int.fract_nonneg r together with a linarith tactic that establishes nonnegativity of 1 - Int.fract r from Int.fract_lt_one r.
why it matters
This result feeds directly into w_resonant_ge_one, which shows the resonant weight is at least one. It supports analysis of resonance within the eight-tick octave (T7) of the gravity sector, ensuring the weight kernel reaches its minimum at synchronized frequencies. No open questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.