Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Proposition 6, pp. 18–19 — under the W_it-policy, robust generation and ramping limits reduce to the extreme total-load scenarios

Proved
MultistageRUC.WitPolicy.proposition_6

by mikedeng1 · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

affine-policybudget-uncertaintyp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1robust-optimizationunit-commitment

Consider the affine multistage robust unit commitment model under the WitW_{it}Wit​-policy pit(d)=wit+Wit∑j∈Nddjtp^t_i(\mathbf d)=w^t_i+W_{it}\sum_{j\in\mathcal N_d}d^t_jpit​(d)=wit​+Wit​∑j∈Nd​​djt​, with arbitrary output limits pimin⁡,pimax⁡p^{\min}_i,p^{\max}_ipimin​,pimax​, ramp rates RDit,RUit,SDit,SUitRD^t_i,RU^t_i,SD^t_i,SU^t_iRDit​,RUit​,SDit​,SUit​, commitments xit,uit,vitx^t_i,u^t_i,v^t_ixit​,uit​,vit​, initial state xi0,pi0x^0_i,p^0_ixi0​,pi0​, and policy coefficients wit,Witw^t_i,W_{it}wit​,Wit​. Let D=∏tDt\mathcal D=\prod_t\mathcal D^tD=∏t​Dt be the budget uncertainty set (3), and let dmax⁡,dmin⁡∈D\mathbf d_{\max},\mathbf d_{\min}\in\mathcal Ddmax​,dmin​∈D be trajectories whose total load is maximal, respectively minimal, over D\mathcal DD in every period ((19), (20)). Let dminmax(t)\mathbf d_{minmax}(t)dminmax​(t) and dmaxmin(t)\mathbf d_{maxmin}(t)dmaxmin​(t) be the scenarios (21), (22).

Then for every generator iii and every period ttt:

  1. the robust generation limits (8c) over D\mathcal DD are equivalent to the same constraints over the finite set {dmin⁡,dmax⁡}\{\mathbf d_{\min},\mathbf d_{\max}\}{dmin​,dmax​};
  2. the robust ramping-down limits (8d) at ttt over D\mathcal DD are equivalent to the same constraints over {dmin⁡,dmax⁡,dminmax(t),dmaxmin(t)}\{\mathbf d_{\min},\mathbf d_{\max},\mathbf d_{minmax}(t),\mathbf d_{maxmin}(t)\}{dmin​,dmax​,dminmax​(t),dmaxmin​(t)}, and so are the robust ramping-up limits (8e).

In symbols, for (8c),

pimin⁡xit≤pit(d)≤pimax⁡xit  ∀d∈D  ⟺  pimin⁡xit≤pit(d)≤pimax⁡xit  ∀d∈{dmin⁡,dmax⁡}.p^{\min}_i x^t_i\le p^t_i(\mathbf d)\le p^{\max}_i x^t_i\ \ \forall\mathbf d\in\mathcal D\iff p^{\min}_i x^t_i\le p^t_i(\mathbf d)\le p^{\max}_i x^t_i\ \ \forall\mathbf d\in\{\mathbf d_{\min},\mathbf d_{\max}\}.pimin​xit​≤pit​(d)≤pimax​xit​  ∀d∈D⟺pimin​xit​≤pit​(d)≤pimax​xit​  ∀d∈{dmin​,dmax​}.

This is Proposition 6 of the paper. It means that, under the WitW_{it}Wit​-policy, the generation and ramping constraints can be imposed in advance through finitely many scenarios, so that only the worst-case cost constraint and the transmission constraints need constraint generation.

Formalization Note. The statement is for the WitW_{it}Wit​-policy; the WiW_iWi​-policy (9) ("any simpler policy") is the instance Wit=WiW_{it}=W_iWit​=Wi​. Lean periods are 0-based. At the first period the ramping constraints compare with the initial dispatch pi0p^0_ipi0​ and use xi0x^0_ixi0​ in place of xit−1x^{t-1}_ixit−1​. The commitments are arbitrary reals (the paper's {0,1}\{0,1\}{0,1} restriction is not needed). The scenarios dmax⁡,dmin⁡\mathbf d_{\max},\mathbf d_{\min}dmax​,dmin​ are hypotheses: any members of D\mathcal DD that maximize, respectively minimize, the total load of every period. The standing assumptions Γ≥0\Gamma\ge0Γ≥0, d^jt>0\hat d^t_j>0d^jt​>0 of (3) are not needed once dmax⁡,dmin⁡∈D\mathbf d_{\max},\mathbf d_{\min}\in\mathcal Ddmax​,dmin​∈D is assumed, and are omitted.

Preamble
import Mathlib
import Definitions.Def_MultistageRUC_WitPolicy_Setting
Formal statement
namespace MultistageRUC.WitPolicy

theorem proposition_6 {Ng Nd T : ℕ}
    (pmin pmax : Fin Ng → ℝ) (RD RU SD SU : Fin Ng → Fin T → ℝ)
    (x0 p0 : Fin Ng → ℝ) (x u v : Fin Ng → Fin T → ℝ) (w W : Fin Ng → Fin T → ℝ)
    (dbar dhat : Fin T → Fin Nd → ℝ) (Γ : ℝ)
    (dmax dmin : Fin T → Fin Nd → ℝ)
    (hmax : IsMaxLoad (MultistageRUC.Equiv.uncSet dbar dhat Γ) dmax)
    (hmin : IsMinLoad (MultistageRUC.Equiv.uncSet dbar dhat Γ) dmin) :
    ∀ i t,
      (GenLimits pmin pmax x w W (MultistageRUC.Equiv.uncSet dbar dhat Γ) i t ↔
        GenLimits pmin pmax x w W {dmin, dmax} i t) ∧
      ((RampDown RD SD x v p0 w W (MultistageRUC.Equiv.uncSet dbar dhat Γ) i t ↔
          RampDown RD SD x v p0 w W {dmin, dmax, dminmax dmin dmax t, dmaxmin dmin dmax t} i t) ∧
        (RampUp RU SU x0 x u p0 w W (MultistageRUC.Equiv.uncSet dbar dhat Γ) i t ↔
          RampUp RU SU x0 x u p0 w W {dmin, dmax, dminmax dmin dmax t, dmaxmin dmin dmax t} i t)) := by sorry

end MultistageRUC.WitPolicy
Source
Lorca, Sun, Litvinov, Zheng, Multistage adaptive robust optimization for the unit commitment problem, Oper. Res. (2016), doi:10.1287/opre.2015.1456, manuscript of Sept. 29, 2014, pp. 18–19, Proposition 6
Human review
  • Endorsed by Shuze Chen · Oct 9, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 9, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me