interpolation_cost_zero_at_integer

formal source

  43  · exact min_le_of_right_le (by linarith [Int.fract_lt_one r])
  44
  45/-- At integer ratios, interpolation cost is zero — perfect synchronization. -/
  46theorem interpolation_cost_zero_at_integer (n : ℤ) :
  47    interpolation_cost (n : ℝ) = 0 := by
  48  unfold interpolation_cost
  49  simp [Int.fract_intCast]
  50
  51/-! ## 3. Resonance-Aware Weight Kernel -/
  52
  53/-- C_lag = φ⁻⁵ ≈ 0.09 — the RS-derived lag coupling. -/
  54def C_lag : ℝ := phi⁻¹ ^ 5
  55
  56theorem C_lag_pos : 0 < C_lag := by
  57  unfold C_lag
  58  exact pow_pos (inv_pos.mpr phi_pos) 5
  59
  60/-- The resonance-aware ILG weight kernel.
  61    w(r) = 1 + C_lag · interpolation_cost(r)
  62    At resonance (integer r): w = 1 (minimum).
  63    Off resonance: w > 1. -/
  64def w_resonant (r : ℝ) : ℝ :=
  65  1 + C_lag * interpolation_cost r
  66
  67theorem w_resonant_ge_one (r : ℝ) : 1 ≤ w_resonant r := by
  68  unfold w_resonant
  69  linarith [mul_nonneg (le_of_lt C_lag_pos) (interpolation_cost_nonneg r)]
  70
  71/-- At resonance, the weight kernel equals 1 (minimum). -/
  72theorem w_at_resonance (n : ℤ) : w_resonant (n : ℝ) = 1 := by
  73  unfold w_resonant
  74  rw [interpolation_cost_zero_at_integer, mul_zero, add_zero]
  75
  76/-- Off resonance, the weight kernel exceeds 1. -/