Documentation

Lean 4 Proof

theorem knockout_triggered_regime_shift
    (N : ℕ) (e : WeightedNSectorEconomy N) (n : Fin N)
    (j : Fin (e.J n)) :
    -- If a_{n,j} > a_crit(ρ_n, T_n), knockout of input j causes regime shift
    -- Regime shift is permanent: system cannot return to complementary equilibrium
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Dynamics/Relaxation.lean:469

Module Section

## Proposition 3b.6: Knockout-Triggered Regime Shift

In the same file