interpolation_cost_le_half
plain-language theorem explainer
The interpolation cost of any real frequency ratio r is at most one half. Researchers working on resonant weights in the eight-tick gravity model cite this bound to control the growth of w_resonant. The proof proceeds by case analysis on the fractional part of r and direct application of the min-lemmas for the two branches.
Claim. For all real numbers $r$, the interpolation cost defined by $min(fract r, 1 - fract r)$ satisfies $min(fract r, 1 - fract r) ≤ 1/2$.
background
The EightTickResonance module defines the interpolation cost to measure deviation of a frequency ratio from integer synchronization with the ledger. It equals the minimum of the fractional part of r and its complement to one, reaching zero at integers and one half at half-integers. This construction draws from the J-cost in ObserverForcing and the derived cost in MultiplicativeRecognizerL4, specialized here to fractional arithmetic for resonance analysis.
proof idea
The proof unfolds the definition of interpolation_cost to expose the min expression. It then splits into cases according to whether the fractional part is at most one half. The left branch applies the left-min lemma directly; the right branch invokes the right-min lemma after a linear arithmetic step establishing that the complement is at most one half.
why it matters
This lemma supplies the key estimate for the upper bound on the resonance weight w_resonant, which is shown to be at most one plus C_lag over two. It supports the resonant frequency calculations within the eight-tick resonance framework, ensuring controlled penalties in the gravity sector of the Recognition Science forcing chain. The result closes a local estimate without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.