Documentation

Lean 4 Proof

theorem cbdc_triggers_bifurcation (e : SettlementEconomy) {lambda_B : ℝ}
    (_hlambda_pos : 0 < lambda_B) (_hlambda_lt : lambda_B < 1)
    (h_sub : settlementR0Friction e lambda_B < 1)
    (h_super : 1 < settlementR0 e) :
    settlementR0Friction e lambda_B < 1 ∧
    1 < settlementR0Friction e 1 := by
  constructor
  · exact h_sub
  · rwa [settlementR0Friction_one]

Dependency Graph

Location

thesis/CESProofs/Applications/SettlementFeedback.lean:195

Module Section

Paper 7: Settlement Feedback and Monetary Policy in a Mesh Economy

In the same file