Documentation

Lean 4 Proof

theorem dual_side_integration_boundary
    (J : ℕ) (ρ : ℝ) (a : Fin J → ℝ) (T c w : ℝ) :
    -- The production-side integration boundary (K_eff > threshold)
    -- and the cost-side boundary (1/K_eff_dual > threshold)
    -- are linked by the conservation law.
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Potential/PrimalDual.lean:45

Module Section

## Corollary 2b.5: Dual-Side Integration Boundary

In the same file