Cascade Vanishes At Critical

theorem proved Dynamics & Crises

Documentation

Lean 4 Proof

theorem cascade_vanishes_at_critical {β_C K_eff Tstar : ℝ} :
    cascadeFrictionRate β_C K_eff Tstar Tstar = 0 := by
  simp only [cascadeFrictionRate, sub_self, mul_zero]

Dependency Graph

Location

thesis/CESProofs/Dynamics/EndogenousT.lean:174

Module Section

Results T-80 through T-89: Endogenous Information Friction Dynamics

In the same file

learningFrictionRate cascadeFrictionRate institutionalFrictionRate shockFrictionImpulse combinedFrictionRate learning_reduces_friction cascade_increases_friction institutional_reform_lowers_friction friction_channels_oppose minsky_friction_spiral friction_hysteresis learning_at_zero combined_rate_steady_state f_T_specified