Documentation

Lean 4 Proof

theorem debtSustainable_zero_debt {r_B g d : ℝ} :
    debtSustainable r_B g 0 d ↔ d ≤ 0 := by
  simp only [debtSustainable, debtDynamics]; constructor <;> intro h <;> nlinarith

Dependency Graph

Location

thesis/CESProofs/Macro/TaxStructure.lean:378

Module Section

Government Tax Structure (Layer 3 of Macro Extension)

In the same file