State-Cost CVaR — the Inf-Form Instantiated at the Guidance State Cost

At a glance

Phase B of the risk-aware program applies the same tail-risk measure as Phase A, but to a state cost rather than a view score (obligation B3). This module is the wiring that makes that reuse rigorous: it instantiates the sealed Rockafellar–Uryasev inf-form at the state-cost loss and transfers all three of its structural facts — convexity, minimizer-at-a-sample, and the closed-form value — with no new mathematics. Because every theorem in the sealed engine is stated for an arbitrary sample with no distinctness hypothesis, the transfer is a direct application, and the atom-safety that made the view-score form trustworthy carries over verbatim. Lean’s kernel has checked all three public results on the three standard axioms [propext, Classical.choice, Quot.sound], with no sorry.

Links: module index · the sealed inf-form (Phase A) · assumptions ledger · sources rockafellar2000optimization, rockafellar2002conditional. Numeric behaviour is identical to the sealed engine and is covered by its cross-check (~/Code/tasks/streams/ctrllib/scratch/pin_cvar_saa.py); this module adds no arithmetic and needs no pin of its own.

Motivation

The Phase-A module cvar_inf_form seals the discrete Rockafellar–Uryasev form of Conditional Value-at-Risk for a finite equal-weight sample of a view score — the loss a camera-placement planner risks. Phase B asks the risk-aware guidance layer to bound a different loss: a state cost on the estimated state (the tracking / standoff / confidence cost the guidance policy incurs), evaluated across a batch of scenario states. The obligations map records the reduction plainly (proof_obligations_risk_phases.md row B3): “the risk functional is identical, only the loss $Z$ changes (state-cost instead of view-score).”

That single sentence is the whole content of B3, and it is a wiring corollary rather than a theorem, because the sealed engine was written to be loss-agnostic from the start. This page records the instantiation and — the one thing worth checking — confirms that the atom-safety argument, which is what made the discrete form trustworthy in the first place, depends on nothing specific to the view score and so transfers unchanged.

The objects

The state cost is left abstract: a function $J:S\to \mathbb{R}$ on an arbitrary state space $S$. The corpus fixes no formula for it (proof_obligations_risk_phases.md:78 specifies only “state cost”, never a quadratic form, a norm, or a tracking error), and keeping it general is not a shortcut — it is exactly the faithful statement, since the reduction claim is that any choice of loss inherits the CVaR algebra.

A scenario batch is a family of $q$ sampled states $x:\text{Fin }q\to S$. The state-cost loss sample (stateLoss) is the cost evaluated at each scenario,

$\text{stateLoss}Jx=(k\mapsto J(x_k)):\text{Fin }q\to \mathbb{R},$

which is the Phase-B loss $Z$ — identical in role to the Phase-A view score, differing only in what it measures. The state-cost CVaR (cvarState) is then the sealed inf-form evaluated at this loss,

$\text{cvarState}\alpha Jx=\text{cvarSAA}\alpha (\text{stateLoss}Jx)={\inf }_{\tau \in \mathbb{R}}\text{cvarObj}\alpha (\text{stateLoss}Jx)\tau ,$

with cvarObj, cvarSAA imported verbatim from cvar_inf_form — no redefinition. The confidence level is $\alpha \in [0,1)$ and $\tau$ the auxiliary minimization variable, in the 2002 Rockafellar–Uryasev naming the sealed module already uses.

The three instantiations

Each theorem is a one-line application of its Phase-A counterpart at $Z:=\text{stateLoss}Jx$. Nothing is re-proved; the proofs are the sealed terms themselves.

Convexity of the state-cost objective (cvarState_obj_convexOn)

$0<q,\alpha <1\Rightarrow \text{ConvexOn}\mathbb{R}\text{univ}(\text{cvarObj}\alpha (\text{stateLoss}Jx))$

Directly cvarObj_convexOn at the state-cost loss. The objective is convex in the auxiliary variable $\tau$, so the sampled state-cost CVaR constraint is a convex program — an LP after the standard epigraph split — exactly as for the view score. (This is convexity in $\tau$, the property that licenses the LP reduction; it does not assert convexity of the CVaR in the guidance decision variables, which would need $J$ itself convex in those variables and is a modelling matter, not proved here.)

The minimizer is a scenario’s state cost (cvarState_min_at_scenario)

$0<q,0\le \alpha <1\Rightarrow \exists k,\forall \tau ,\text{cvarObj}\alpha (\text{stateLoss}Jx)(J(x_k))\le \text{cvarObj}\alpha (\text{stateLoss}Jx)\tau$

Directly cvarObj_min_at_sample. The global minimum over $\tau \in \mathbb{R}$ is attained at $J(x_k)$ — the state cost of one scenario, the Value-at-Risk breakpoint (Rockafellar–Uryasev 2002, Proposition 8). Because stateLoss J x applied to $k$ is $J(x_k)$ definitionally, the sealed sample-point statement reads off directly as a statement about scenarios’ state costs.

The state-cost CVaR is attained at a scenario (cvarState_eq_obj_scenario)

$0<q,0\le \alpha <1\Rightarrow \exists k,\text{cvarState}\alpha Jx=\text{cvarObj}\alpha (\text{stateLoss}Jx)(J(x_k))$

Directly cvarSAA_eq_obj_sample. The defined state-cost CVaR equals the objective evaluated at a scenario’s state cost — a finite, computable value (the 2002 Proposition 8 closed-form shape), not a continuum infimum. A guidance policy recovers both the state-cost CVaR and its VaR by scanning a finite list of scenario costs.

Atom-safety transfers verbatim

The reason the discrete inf-form is trustworthy is that it carries no distinctness hypothesis, so a probability mass sitting exactly at the VaR quantile is handled by construction — the inf-form never forms the ambiguous conditional expectation that a naive tail average would (see cvar_inf_form > When a probability mass sits at the quantile). For the view score, the atom was the visibility flip depositing a mass at the failure loss.

For the state cost the atom is different in origin but identical in structure: two scenarios can share a state cost — a mass at a saturated actuator cost, at a constraint-violation ceiling, or wherever the state cost clips. Since stateLoss J x is an arbitrary $\text{Fin }q\to \mathbb{R}$ with no imposed injectivity, the sealed theorems apply to it unchanged, ties and all. Crucially, nothing in the atom argument used that the loss was a view score — it used only that the sample is an arbitrary real family — so it transfers verbatim. That is the one confirmation obligation B3 actually asks for, and it is discharged by the generality of the sealed statements, not by any new proof.

Scope and limitations

• Definition-first, inherited. cvarState is defined through the sealed inf-form, so it inherits the Phase-A scope exactly: CVaR is the Rockafellar–Uryasev operative definition, the sorted $\alpha$-tail-average equality is deferred (it needs order statistics and is pinned numerically), and nothing here addresses a continuous state-cost distribution — only the finite equal-weight batch a scenario planner produces.
• State cost abstract by design. $J:S\to \mathbb{R}$ is arbitrary. The instantiation makes no assumption about its form because the reduction claim is precisely that none is needed; a concrete $J$ (once the guidance stream fixes one) is a drop-in, changing no theorem.
• Convexity is in $\tau$, not in the decision. As noted above, cvarState_obj_convexOn gives convexity of the auxiliary objective, the LP-enabling fact. Whether the state-cost CVaR is convex in the guidance decision variables is a separate modelling question about $J$ and is out of scope here.
• No new numerics. The CVaR algebra is bit-for-bit the sealed engine’s, so the cvar_inf_form cross-check (pin_cvar_saa.py, including the atom case $Z=[1,2,3,3,10]$) covers this module; it introduces no arithmetic of its own and therefore carries no separate pin.

Provenance

• The auxiliary-function (inf-form) representation of CVaR, its convexity, and the LP reduction are due to Rockafellar & Uryasev (2000), Optimization of Conditional Value-at-Risk, Theorem 1 and eq. 9 — rockafellar2000optimization.
• The general-loss treatment (distributions with atoms), the atom-splitting, the sample form, and the minimizer characterization (Proposition 8) are from Rockafellar & Uryasev (2002), Conditional Value-at-Risk for General Loss Distributions — rockafellar2002conditional.
• The reduction that B3 reuses the Phase-A algebra with only the loss changed is recorded in the risk obligations map, row B3 (~/Code/tasks/streams/risk_aware_planning/proof_obligations_risk_phases.md).

Machine verification (#print axioms)

Built as part of the full Ctrllib library (lake build, 8597 jobs green), with no sorry and no assumption taken as given. Lean’s kernel reports the axiom dependency of each of the three public theorems; nothing beyond [propext, Classical.choice, Quot.sound] appears on any of them, and there is no sorryAx:

'Ctrllib.cvarState_obj_convexOn' depends on axioms: [propext, Classical.choice, Quot.sound]
'Ctrllib.cvarState_min_at_scenario' depends on axioms: [propext, Classical.choice, Quot.sound]
'Ctrllib.cvarState_eq_obj_scenario' depends on axioms: [propext, Classical.choice, Quot.sound]

The empty assumptions ledger (interfaces_assumed: [], interfaces_discharged: []) records that this module, like the engine it instantiates, assumes nothing beyond Mathlib and the sealed cvar_inf_form. The machine-checked source is [(~/Code/vault/lean/CvarStateCost.lean)].