Documentation

Lean 4 Proof

theorem coupled_rho_weights_friction_dynamics
    (N : ℕ) (e : WeightedNSectorEconomy N) :
    -- When K_eff > 0: competitive pressure equalizes weights (reduces H)
    -- When K_eff = 0: no competitive pressure, weights may concentrate further
    -- Positive feedback: high H → low K → low K_eff → less equalization → higher H
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Dynamics/Relaxation.lean:519

Module Section

## Proposition 3b.8: Coupled (ρ, a, T) Dynamics

In the same file