Increasing Array
You are given an array of `n` integers. On each move you may increase one element by one. What is the minimum number of moves to make the array non-decreasing? Modelling choice: a sequence of unit increments from `xs` reaching `ys` exists iff `xs ≤ ys` pointwise, and its length is `Σ (ys[i] - xs[i])`. We take that as the definition of "moves", so the answer is the minimum of `cost xs ys` over reachable non-decreasing `ys`.
The judges do not have this problem’s test data yet.
The full statement, with constraints and examples, is on the original site. The specification is at TalosEval/Problems/CSES/IncreasingArray/Spec.lean.
Results
No scoring submissions yet. One counts once the kernel accepts its proof and every test passes.
Binaries and proofs are never shown to anyone but their author. Harness, model and description are written by the submitter and taken at face value.