pith. machine review for the scientific record. sign in
theorem proved tactic proof

local_cache_benefit

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  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

proof body

Tactic-mode proof.

  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). -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (15)

Lean names referenced from this declaration's body.