Sections / Section 12: Two-World Economy and Indicators / TwoWorldEconomy

Two World Economy

structureprovedDynamics & Crises

Documentation

Lean 4 Proof

structure TwoWorldEconomy (N : ℕ) extends NSectorEconomy N where
  v_price : Fin N → ℝ
  hv : ∀ n, 0 < v_price n
  hfast : ∀ n, ℓ n < v_price n

Dependency Graph

Used by

priceRelaxTime_pos indicator_classification_foundations slow_manifold_reduction priceRelaxTime crisis_asymmetry_ratio composed_ordering quantityRelaxTime_pos early_warning_same_criticality timescaleGap quantityRelaxTime price_leads_quantity timescaleGap_gt_one two_world_inherits_paper3 epsPQ_lt_one epsPQ_pos temporal_rules_summary epsPQ price_faster_than_quantity shared_effective_curvature curvature_conservation_lag

Location

thesis/CESProofs/Dynamics/TwoWorldDefs.lean:41

Module Section

Two-World Economy: Price vs. Production Timescale Separation

In the same file

epsPQ epsPQ_pos epsPQ_lt_one priceRelaxTime quantityRelaxTime priceRelaxTime_pos quantityRelaxTime_pos price_faster_than_quantity slow_manifold_reduction two_world_inherits_paper3 timescaleGap timescaleGap_gt_one timescaleGap_monotone_in_relaxRate