Documentation

Lean 4 Proof

theorem fragility_at_critical {Tstar1 Tstar2 : ℝ}
    (hTs1 : 0 < Tstar1) (_hTs2 : 0 < Tstar2) (h : Tstar1 < Tstar2) :
    institutionalMargin Tstar1 Tstar1 = 0 ∧
    0 < institutionalMargin Tstar1 Tstar2 := by
  constructor
  · -- At T = T*₁: margin₁ = max(0, 1 - 1) = 0
    simp [institutionalMargin, div_self (ne_of_gt hTs1)]
  · -- At T = T*₁: margin₂ = max(0, 1 - T*₁/T*₂) > 0 since T*₁ < T*₂
    simp only [institutionalMargin]
    apply lt_max_of_lt_right
    have hlt : Tstar1 / Tstar2 < 1 := by
      rw [div_lt_one (by linarith)]
      exact h
    linarith

Dependency Graph

Location

thesis/CESProofs/Hierarchy/InstitutionalReform.lean:201

Module Section

Institutional Reform Equivalence, Adjustment Timescale, and Fragility Ordering

In the same file