Documentation

Lean 4 Proof

theorem smirl_tradeoff_vs_romer_escape (J : ℝ) (hJ : 1 < J)
    {ρ : ℝ} (_hρ : ρ < 1) {c d_sq : ℝ} (_hc : 0 < c) (_hd : 0 < d_sq) :
    -- ρ direction: K up when ρ down (tradeoff with T*)
    (∀ ρ₁ ρ₂, ρ₁ < ρ₂ → ρ₂ < 1 →
      curvatureKReal J ρ₂ < curvatureKReal J ρ₁) ∧
    -- J direction: K up AND T* up (no tradeoff)
    (∀ J₁ J₂, 1 < J₁ → J₁ < J₂ →
      curvatureKReal J₁ ρ < curvatureKReal J₂ ρ ∧
      criticalFrictionReal J₁ ρ c d_sq < criticalFrictionReal J₂ ρ c d_sq) := by
  constructor
  · -- ρ direction: K decreasing in ρ
    intro ρ₁ ρ₂ hρ₁₂ hρ₂
    simp only [curvatureKReal]
    have hJpos : 0 < J := by linarith
    have hJm1 : 0 < J - 1 := by linarith
    rw [div_lt_div_iff₀ hJpos hJpos]
    have : 0 < (J - 1) * J := mul_pos hJm1 hJpos
    nlinarith [mul_pos hJm1 hJpos]
  · -- J direction: K and T* both increasing in J
    intro J₁ J₂ hJ₁ hJ₁₂
    exact ⟨curvatureKReal_increasing (by linarith) J₁ J₂ (by linarith) hJ₁₂,
           criticalFriction_increasing_in_J hJ₁ hJ₁₂ _hρ _hc _hd⟩

Dependency Graph

Location

thesis/CESProofs/EntryExit/CurvatureInJ.lean:133

Module Section

Paper 1c, Section 2: K(J) as the Network Engine

In the same file