local_cache_benefit

formal source

  43  (A1) Non-uniformity: freq(v*) · dist(v*) is the dominant cost term
  44  (A2) Distance spread: dist(v*) > ε
  45  (A3) Positive maintenance: 0 < α < freq(v*) · (dist(v*) - ε) -/
  46theorem local_cache_benefit
  47    (freq_star dist_star ε α : ℝ)
  48    (_hε_pos : 0 < ε)
  49    (_hdist : ε < dist_star)
  50    (_hα_pos : 0 < α)
  51    (hα_lt : α < freq_star * (dist_star - ε))
  52    (_hfreq_pos : 0 < freq_star) :
  53    -- The cost reduction from caching v* is strictly positive
  54    freq_star * dist_star - (freq_star * ε + α) > 0 := by
  55  have h1 : freq_star * dist_star - freq_star * ε = freq_star * (dist_star - ε) := by ring
  56  linarith [hα_lt]
  57
  58/-! ## §2  Fibonacci Partition Forces φ (Theorem 4.2, rigorous) -/
  59
  60/-- The Fibonacci partition recurrence: each level's capacity equals the sum
  61    of the next two smaller levels. This arises from J-cost-optimal partitioning
  62    (see paper §4 for the derivation). -/
  63def fibonacci_recurrence (K : ℕ → ℝ) : Prop :=
  64  ∀ ℓ : ℕ, K (ℓ + 2) = K (ℓ + 1) + K ℓ
  65
  66/-- The constant-ratio property: K_{ℓ+1}/K_ℓ = r for all ℓ. -/
  67def constant_ratio (K : ℕ → ℝ) (r : ℝ) : Prop :=
  68  ∀ ℓ : ℕ, K (ℓ + 1) = r * K ℓ
  69
  70/-- **KEY LEMMA**: Fibonacci recurrence + constant positive ratio → r² = r + 1.
  71
  72This is the rigorous replacement for the hand-wavy "self-similar cost" argument. -/
  73theorem fibonacci_ratio_forces_golden (K : ℕ → ℝ) (r : ℝ)
  74    (_hr_pos : 0 < r)
  75    (hK_pos : ∀ ℓ, 0 < K ℓ)
  76    (hfib : fibonacci_recurrence K)