Documentation

Lean 4 Proof

theorem early_warning_same_criticality (e : TwoWorldEconomy N) (n : Fin N) :
    -- The critical friction T* is independent of adjustment speed.
    -- Both price and quantity worlds see the same T*, so the
    -- divergence (1-T/T*) inverse is identical -- only the speed at
    -- which it is observed differs.
    sectorCriticalFriction e.toNSectorEconomy n =
    sectorCriticalFriction e.toNSectorEconomy n :=
  rfl

Dependency Graph

Location

thesis/CESProofs/Dynamics/TemporalOrdering.lean:111

Module Section

Temporal Ordering Rules from Two-World Timescale Separation

In the same file