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

caching_is_forced

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)

 100theorem caching_is_forced
 101    (n : ℕ) (freq : Fin n → ℝ) (dist_alloc : Fin n → ℕ)
 102    (hfreq_pos : ∀ i, 0 < freq i)
 103    (hremote : ∃ i, 0 < dist_alloc i) :
 104    (∑ i : Fin n, freq i * Jcost (phi ^ 0)) <
 105    (∑ i : Fin n, freq i * Jcost (phi ^ (dist_alloc i))) := by

proof body

Term-mode proof.

 106  obtain ⟨j, hj⟩ := hremote
 107  apply Finset.sum_lt_sum
 108  · intro i _
 109    apply mul_le_mul_of_nonneg_left _ (le_of_lt (hfreq_pos i))
 110    rw [access_cost_zero_at_origin]
 111    exact Jcost_nonneg (pow_pos phi_pos _)
 112  · exact ⟨j, Finset.mem_univ j, by
 113      apply mul_lt_mul_of_pos_left _ (hfreq_pos j)
 114      exact collocation_minimizes_cost _ hj⟩
 115
 116/-! ## Part 5: φ from Fibonacci -/
 117
 118/-- **φ FROM FIBONACCI**: If r > 0 satisfies r² = r + 1, then r = φ. -/

depends on (8)

Lean names referenced from this declaration's body.