Settlement R0 Friction

def proved Curvature Roles

Documentation

Lean 4 Proof

def settlementR0Friction (e : SettlementEconomy) (lambda_B : ℝ) : ℝ :=
  (e.cross_phi_S * (lambda_B * e.cross_S_phi)) / (e.self_phi * e.self_S)

Dependency Graph

Used by

settlementR0Friction_eq cbdc_acceleration cbdc_triggers_bifurcation friction_monotone settlementR0Friction_one

Location

thesis/CESProofs/Applications/SettlementFeedback.lean:112

Module Section

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