Gravity Eight Tick Resonance Interpolation Cost Nonneg

The interpolation cost

The interpolation cost is a number that measures how far a frequency ratio is from being an integer. For any real number r, it is defined as the distance to the nearest integer: the smaller of the fractional part of r and one minus that fractional part. If r is exactly an integer, the cost is 0. If r is exactly halfway between two integers, the cost reaches its maximum value of 1/2. This is a plain mathematical definition, independent of any physical theory.

The definition has a natural use in the Recognition Science framework, where a ledger (a discrete record of events) sets a clock. In that framework, the interpolation cost measures how far a frequency ratio is from being synchronized with that clock. A ratio of exactly 8, for instance, has cost 0, meaning it is perfectly in step. A ratio of 8.5 has cost 1/2, meaning it is as out of step as possible. The framework uses this cost to build a resonant frequency, where the cost is added to a base value, so that being off the integer costs more.

The declaration interpolation_cost_nonneg is a machine-checked theorem in the framework's library of formal theorems. It states that for every real number r, the interpolation cost is greater than or equal to zero. The proof is short and relies on two standard facts about the fractional part function: it is never negative, and it is always less than one. From those two facts, the minimum of the two candidate values is also never negative. The theorem is a formal guarantee of a property that is visually obvious from the definition, but the value of the machine check is that it rules out any hidden edge case in the logic.

The theorem does not claim that the interpolation cost is the only possible measure of desynchronization, nor that it has any physical meaning on its own. It does not claim that a frequency ratio of 8 is physically preferred over 8.1; that would require additional physical assumptions about the ledger and its clock. The theorem only certifies that the cost function, as defined, never outputs a negative number. It is a small but necessary piece of the larger framework, ensuring that the cost function behaves as a genuine distance-like quantity.

/-- The interpolation cost measures how far a frequency ratio is from an integer.
    At integers (synchronized with ledger clock): cost = 0.
    At half-integers (maximally desynchronized): cost = 1/2.
    We use distance to nearest integer: min(fract r, 1 - fract r). -/
def interpolation_cost (r : ℝ) : ℝ :=
  min (Int.fract r) (1 - Int.fract r)

theorem interpolation_cost_nonneg (r : ℝ) : 0 ≤ interpolation_cost r := by
  unfold interpolation_cost
  exact le_min (Int.fract_nonneg r) (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]

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])

What this page does not claim

The theorem does not claim that the interpolation cost is the only possible measure of desynchronization. The theorem does not claim that integer frequency ratios are physically preferred without additional assumptions. The theorem does not claim that the interpolation cost has any direct physical meaning on its own.

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: