Documentation

Lean 4 Proof

theorem industrial_policy_rigidity
    (K_F K_C δ : ℝ) (h_KF : 0 < K_F) (h_KC : 0 < K_C) (h_δ : 0 < δ) :
    -- Policy raising K_F by δ necessarily reduces K_C by at least δ · K_C/K_F
    -- (first-order approximation from conservation law)
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Potential/PrimalDual.lean:94

Module Section

## Policy Tradeoff Theorems (Gap 8)

In the same file