In a hydro-dominated grid the marginal value of stored water is the shadow price that sets the whole dispatch — and it obeys a theorem: between the events where the reservoir hits full or empty, the water value is a MARTINGALE, stepping down across full-reservoir events and up across empty ones. On finite scenario trees that statement is proved by LP duality with no constraint qualification, and this page re-proves it at every build: the solver is extracted from the published artifact's own bytes, run on 120 random trees, and every certificate re-checked — duality gap, martingale residual, Hotelling trichotomy.
A pass/fail suite reports one bit. What a reader should want is the margin, and the margin is a distribution: every one of the 120 seeded trees, binned by the relative gap between its primal revenue and its dual certificate. The gate the suite enforces is drawn where it actually sits.
A hydro operator holding stock R releases h against price ϖ under a hard box 0 ≤ R ≤ R̄. The water value w is the multiplier of the stock balance, and optimality is the Hotelling trichotomy: release at full rate where ϖ > w, hold where ϖ < w, and at interior release the price IS the water value. In the deterministic case w is piecewise constant, jumping up across empty-reservoir events and down across full ones — proved here as the KKT system of a finite LP, where no constraint qualification is needed and strong duality is an identity you can print.
On a scenario tree the same proof gives the stochastic statement: at every node whose post-release stock is interior, w equals the conditional expectation of its children's w — the water value is a martingale between stock-binding events, and spilling nodes pin w = 0 (marginal water at a spilling dam is worthless, reappearing as a dual complementarity). That is the exact discrete content of the continuum equation dw = Z dB + dL⁰ − dL̄, with the local times acting only at the barriers.
The scenario-tree solver ships verbatim inside the published water-value artifact, between markers, ending in its own module exports — so this build does not trust a copy: it extracts the solver from the page bytes, checks the extraction's sha256 against the pin, and refuses on a single flipped byte. The extracted source is then run on 120 seeded random trees (depths 3–5, branching 2–3, randomized prices, inflows, stock boxes and salvage), and on every tree four certificate families are re-checked: the KKT residuals (dynamics, boxes, wedge signs, spill duals), the Hotelling trichotomy (zero violations tolerated), the off-binding martingale residual, and the duality gap.
The gap check is one-signed on purpose. This is a maximization LP, so weak duality makes dual − primal non-negative for ANY feasible pair — a negative value cannot be a convergence artifact; it can only mean the assembly is wrong, and the build dies on it as a separate check rather than folding it into a magnitude. The red controls are the lifted unit's own: the adjoint-matched-operator battery must catch both of its planted mutants (it did — 2 CAUGHT this build), and the page-kernel battery re-extracts the browser kernel from the artifact and re-runs its full corner sweep.
The unit tested the theorem's signature against Brazil's hourly spot price (PLD, submarket Sudeste, 2021–2025): between jumps the price should be flat where hydro is marginal. The record shows interior windows with flatness shrinkage up to 75× against a permutation null, and the flattest year is 2021 — the water crisis, when scarcity kept hydro marginal nearly year-round. The naive seasonal reading ("wet years flatter") is REFUTED by the same data: flatness tracks the hydro-marginal regime, not the calendar.
The unit's own adversarial review downgraded this layer from "confirmed" to DESCRIPTIVE CONSISTENCY, and this page keeps the downgrade: PLD is an administered price built from a model that already moves its water value slowly, the permutation null measures persistence rather than pinning, and the window selection is partly circular. These numbers are quoted as history because their data sits behind CCEE's access wall — the recipe to re-run them ships with the unit (docs/pld-data-run.md), and nothing in §2's certificates depends on them.
Every source file behind this page was lifted FILE-LEVEL from the research unit's public set — the eligibility criterion is presence in the source lab's own published tree, checked against the live repository listing — and sits byte-preserved in this repository under legacy/research/stock-constraint/: the two original artifacts, the batteries this build re-ran, the reference implementations, and the model spec with its PROVED/SKETCHED/OPEN labels. The lineage is the price-formation program of the KAUST mean-field-games group (Gomes, Gutierrez, Ribeiro; Bakaryan, Aoun, de Lima Ribeiro, Hovakimyan, Gomes), whose results the source unit reproduces; the certification layer and this page are independent of that group and any error here is ours.