Documentation

Lean 4 Proof

theorem weighted_curvature_conservation
    (J : ℕ) (ρ : ℝ) (a : Fin J → ℝ) (c w : ℝ) :
    -- |λ_⊥^F(a)| · |λ_⊥^C(a)| = f(H, J, c, w) — ρ-independent
    -- Economic meaning: production curvature × cost curvature determined by
    -- market structure (weights), not technology (complementarity)
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Potential/PrimalDual.lean:21

Module Section

## Theorem 2b.3: Weighted Curvature Conservation

In the same file