Documentation

Lean 4 Proof

theorem landscape_structure (e : NSectorEconomy N) (n : Fin N)
    (hKeff : 0 < sectorEffectiveCurvature e n) :
    -- The sector-n component of the landscape is strictly convex
    -- on 1⊥ when K_eff_n > 0 (sub-critical regime).
    -- We state the algebraic consequence: the relaxation rate is
    -- strictly positive, ensuring convergence to equilibrium.
    0 < sectorRelaxRate e n := by
  simp only [sectorRelaxRate]
  apply mul_pos
  · apply mul_pos (e.hℓ n) (abs_pos.mpr _)
    simp only [logCesEigenvaluePerp]
    apply div_ne_zero
    · simp only [neg_ne_zero]; linarith [e.hρ n]
    · exact mul_ne_zero (Nat.cast_ne_zero.mpr (by have := e.hJ n; omega))
        (pow_ne_zero 2 (ne_of_gt (e.hc n)))
  · -- (1 - T/T*)⁺ > 0 from K_eff > 0
    simp only [sectorEffectiveCurvature, effectiveCurvatureKeff] at hKeff
    have hK : 0 < curvatureK (e.J n) (e.ρ n) := curvatureK_pos (e.hJ n) (e.hρ n)
    have hmax : 0 < max 0 (1 - e.T n / sectorCriticalFriction e n) := by
      by_contra h; push_neg at h
      have := le_antisymm h (le_max_left 0 _)
      rw [this, mul_zero] at hKeff; linarith
    exact hmax

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/Relaxation.lean:38

Module Section

Results 1-7: Relaxation on the CES Potential Landscape

In the same file