Documentation

Lean 4 Proof

theorem reshoring_rigidity_corollary
    (K_F_domestic K_C_domestic K_F_gain : ℝ)
    (hKF : 0 < K_F_domestic) (hKC : 0 < K_C_domestic)
    (h_gain : 0 < K_F_gain) :
    -- Any gain in production integration K_F_gain > 0 reduces cost flexibility
    -- Cost rigidity = K_F_gain × (K_C_domestic / K_F_domestic) > 0
    0 < K_F_gain * (K_C_domestic / K_F_domestic) := by
  positivity

Dependency Graph

Location

thesis/CESProofs/Potential/PrimalDual.lean:109

Module Section

## Policy Tradeoff Theorems (Gap 8)

In the same file