Documentation

Lean 4 Proof

theorem composed_ordering (e : TwoWorldEconomy N) :
    -- Each sector has eps_pq < 1: price faster than quantity at every level
    ∀ n, epsPQ e n < 1 :=
  fun n => epsPQ_lt_one e n

Dependency Graph

Location

thesis/CESProofs/Dynamics/TemporalOrdering.lean:212

Module Section

Temporal Ordering Rules from Two-World Timescale Separation

In the same file