Documentation

Lean 4 Proof

theorem dynamic_knockout_propagation
    (N : ℕ) (e : WeightedNSectorEconomy N) (n : Fin N)
    (j : Fin (e.J n)) :
    -- Recovery path depends on a_{n,j}: high-weight knockout → larger transient
    -- Recovery time depends on ρ_n: Leontief (ρ ≤ 0) → no recovery
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Dynamics/Relaxation.lean:449

Module Section

## Theorem 3b.5: Dynamic Knockout Propagation

In the same file