Documentation

Lean 4 Proof

theorem crisis_asymmetry_ratio (e : TwoWorldEconomy N) (n : Fin N)
    (hr : 0 < sectorRelaxRate e.toNSectorEconomy n)
    (hbound : sectorRelaxRate e.toNSectorEconomy n < e.v_price n) :
    -- Recovery/onset time ratio exceeds 1
    1 < timescaleGap e n hr :=
  timescaleGap_gt_one e n hr hbound

Dependency Graph

Location

thesis/CESProofs/Dynamics/TemporalOrdering.lean:149

Module Section

Temporal Ordering Rules from Two-World Timescale Separation

In the same file