Documentation

Lean 4 Proof

theorem ramsey_goldenRule_wedge {τ_K ρ_time δ : ℝ} :
    eulerSteadyStateMPK τ_K ρ_time δ - δ = eulerSteadyStateReturn τ_K ρ_time := by
  simp only [eulerSteadyStateMPK, eulerSteadyStateReturn]; ring

Dependency Graph

Location

thesis/CESProofs/Macro/Accumulation.lean:314

Module Section

Accumulation Dynamics (Layer 2 of Macro Extension)

In the same file