Documentation

Lean 4 Proof

theorem indicator_classification_foundations (e : TwoWorldEconomy N) :
    -- Principle 1: Price world faster than quantity world
    (∀ n, epsPQ e n < 1) ∧
    -- Principle 2: Relative observables detect K; aggregates do not
    (∀ (J : ℕ) (ρ : ℝ), 2 ≤ J → ρ < 1 → 0 < curvatureK J ρ) ∧
    curvatureK 2 1 = 0 ∧
    -- Principle 4: Administered prices slower than market-clearing
    (∀ (v sigma : ℝ), 0 < v → 0 < sigma →
      administeredSpeed v sigma < v) :=
  ⟨fun n => epsPQ_lt_one e n,
   fun _ _ hJ hρ => curvatureK_pos hJ hρ,
   curvatureK_eq_zero_of_rho_one,
   fun _ _ hv hsigma => administered_slower hv hsigma⟩

Dependency Graph

Location

thesis/CESProofs/Dynamics/IndicatorClassification.lean:215

Module Section

Derivation of Leading and Lagging Economic Indicators

In the same file