Gravity Eight Tick Resonance Interpolation Cost Le Half

A bounded measure of mismatch

The interpolation cost is a number between 0 and 1/2 that measures how far a frequency ratio is from an integer. For any real number r, the cost is the distance to the nearest integer, computed as the smaller of r's fractional part and one minus that fractional part. At an integer, the cost is exactly 0. At a half-integer like 1.5 or 2.5, the cost reaches its maximum of 1/2. The theorem interpolation_cost_le_half proves that this maximum is never exceeded: for every real number r, the cost is always less than or equal to 1/2.

In the Recognition Science framework, this bound matters because the cost feeds directly into a quantity called the resonant weight. The resonant weight is defined as 1 plus a small positive constant times the interpolation cost. When the cost is 0, the weight is exactly 1. When the cost is at its maximum of 1/2, the weight is at most 1 plus half that constant. A separate theorem, w_resonant_bounded_above, uses the half bound to place a ceiling on the resonant weight. This ceiling is what keeps the framework's account of gravity from producing unbounded effects as frequencies drift away from integer ratios.

The declaration itself is a modest piece of mathematics: a proof that a particular function has a maximum value. It does not claim that gravity is caused by this cost, nor that the cost is the fundamental quantity of the framework. It does not assert that the bound is tight, only that it holds. The theorem is a supporting lemma in a larger chain, not a standalone physical law. Its role is to guarantee that a key quantity stays finite and controlled, which the framework's library of formal theorems can then build upon.

What the bound changes is the shape of the framework's resonance story. Because the interpolation cost cannot exceed 1/2, the resonant weight cannot grow without limit. This means that the framework can describe a spectrum of weights that are all bounded above, with the maximum occurring at the point of greatest desynchronization. The half bound is what makes that description possible, and it is a fact that the machine-checked library of formal theorems has verified for every real number, not just for a sample of cases.

theorem interpolation_cost_le_half (r : ℝ) : interpolation_cost r ≤ 1/2 := by
  unfold interpolation_cost
  rcases le_or_gt (Int.fract r) (1/2) with h | h
  · exact min_le_of_left_le h
  · exact min_le_of_right_le (by linarith [Int.fract_lt_one r])

/-- At integer ratios, interpolation cost is zero — perfect synchronization. -/
theorem interpolation_cost_zero_at_integer (n : ℤ) :
    interpolation_cost (n : ℝ) = 0 := by
  unfold interpolation_cost
  simp [Int.fract_intCast]

/-- The resonance-aware ILG weight kernel.
    w(r) = 1 + C_lag · interpolation_cost(r)
    At resonance (integer r): w = 1 (minimum).
    Off resonance: w > 1. -/
def w_resonant (r : ℝ) : ℝ :=
  1 + C_lag * interpolation_cost r

/-- The resonance weight is bounded above by 1 + C_lag/2 (since
    interpolation cost ≤ 1/2). -/
theorem w_resonant_bounded_above (r : ℝ) :
    w_resonant r ≤ 1 + C_lag / 2 := by
  unfold w_resonant
  have hic := interpolation_cost_le_half r
  have hcl := le_of_lt C_lag_pos
  nlinarith [mul_le_mul_of_nonneg_left hic hcl]

What this page does not claim

The interpolation cost is not the cause of gravity. The bound of 1/2 is not claimed to be achieved by any particular frequency ratio. The theorem does not state that the resonant weight is bounded by a specific numeric value, only by an expression involving a constant.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/EightTickResonance.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: