Documentation

Lean 4 Proof

theorem mode_dependent_critical_frictions
    (J N : ℕ) (e : WeightedNSectorEconomy N) (n : Fin N) :
    -- Sequential deactivation: T*_1 ≤ T*_2 ≤ ... ≤ T*_{J-1}
    -- The diversity mode (most distributed) deactivates first
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Dynamics/Relaxation.lean:408

Module Section

## Proposition 3b.1: Mode-Dependent Critical Frictions

In the same file