Documentation

Lean 4 Proof

structure SettlementEconomy where
  /-- |∂f_φ/∂S| > 0: settlement infrastructure attracts mesh adoption.
      From eq. (5): ∂f_φ/∂S = γ_φ · φ(1-φ) · ∂μ_φ/∂S. -/
  cross_phi_S : ℝ
  h_cross_phi_S : 0 < cross_phi_S
  /-- |∂f_S/∂φ| > 0: mesh participation generates settlement demand.
      From eq. (6): ∂f_S/∂φ = γ_S · S · g'_mesh(φ). -/
  cross_S_phi : ℝ
  h_cross_S_phi : 0 < cross_S_phi
  /-- |∂f_φ/∂φ| > 0: logistic self-damping of mesh adoption.
      Negative eigenvalue contribution at stable equilibrium. -/
  self_phi : ℝ
  h_self_phi : 0 < self_phi
  /-- |∂f_S/∂S| > 0: stablecoin depreciation and attrition (δ_S).
      Negative eigenvalue contribution at stable equilibrium. -/
  self_S : ℝ
  h_self_S : 0 < self_S

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/SettlementFeedback.lean:60

Module Section

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

In the same file