var_subadditivity

A2 — VaR fails subadditivity: the coherence counterexample

Seal

Rung A2 (risk phase A) · Status sealed — all four theorems axiom-clean (#print axioms verbatim in 6. The machine seal), depending only on propext, no Classical.choice, no Quot.sound, no sorryAx. No interface hypothesis. This is the smallest risk-layer Lean win: a finite decide computation that refutes the universal subadditivity of Value-at-Risk, the reason the thesis’ risk layer uses CVaR (coherent) rather than VaR. Links: source artzner1999coherent (axioms + the §3.3 counterexample), carriers dixit2023risk / majumdar2017how · derivation cvar_derivation_draft §3.2 · obligations map proof_obligations_risk_phases.md row A2 · pin tasks/streams/ctrllib/scratch/pin_var_subadd.py.

What this seals, in one paragraph

Artzner, Delbaen, Eber & Heath (1999) axiomatize a coherent risk measure by four axioms; Axiom S is subadditivity $\rho (X+Y)\le \rho (X)+\rho (Y)$ — pooling risks should never manufacture risk. They prove Value-at-Risk violates S (their §3.3). This module machine-checks that failure on the paper’s independent i.i.d. loss-pair example: two independent identical defaultable bonds, each alone with VaR $0$, whose sum has VaR $100>0$. The module is (~/Code/vault/lean/VaRSubadditivity.lean), build copy ~/lean/ctrllib/Ctrllib/VaRSubadditivity.lean. Numbers pinned first in exact rationals by pin_var_subadd.py, then re-derived in the kernel.

1. The definitions (honest, and why integers)

A finite loss law is a list of (value, integer count) atoms; the probability of an atom is count / totalMass. Two deliberate choices, both load-bearing:

• A list (multiset), not a Finset. The independent sum below is a convolution that produces two distinct joint outcomes with the same total loss ($100$: bond-1 defaults, or bond-2 defaults). Their masses must add. A Finset of (value, count) pairs would collapse the two identical (100, 24) atoms into one and silently halve that mass. The list keeps them; the CDF sums over them.
• Integer counts, not rational probabilities. VaR is defined via the test $F(z)\ge \alpha$. With $\alpha ={\alpha }_{\text{num}}/{\alpha }_{\text{den}}$ and $F(z)=m(z)/N$ (count mass $m(z)$ over total $N$), the test clears its denominators exactly: $F(z)\ge \alpha ⟺m(z){\alpha }_{\text{den}}\ge {\alpha }_{\text{num}}N$. Every quantity is then ℤ/ℕ, which the Lean kernel reduces under decide. Rational (ℚ) arithmetic stalls the kernel on the irreducible Rat.blt; native_decide would compile past it but injects the Lean.ofReduceBool axiom, which the house seal forbids. Integers keep the proof kernel-checked and axiom-clean.

VaR is the textbook lower quantile
${\mathrm{VaR}}_{\alpha }(Z)=\inf \{z:F_Z(z)\ge \alpha \}$
(value_at_risk topic; Artzner 1999 §3 audits VaR against the axioms). For a finite law $F_Z$ is a right-continuous step function that jumps only at support atoms and is constant between them, so the infimum is attained at the least atom whose CDF reaches $\alpha$ — exactly what the Lean VaR computes (the [] => 0 branch is unreachable: for $\alpha \le 1$ the top atom has $F=1\ge \alpha$, so the crossing set is never empty).

2. The two-bond setup and the pinned numbers

One bond is a loss of $100$ with probability $\frac{1}{25}=0.04$ and $0$ with probability $\frac{24}{25}=0.96$. Confidence $\alpha =\frac{19}{20}=0.95$, tail probability $\frac{1}{20}=0.05$. In counts over $N=25$: bond = [(0, 24), (100, 1)].

$z$	$F_{\text{bond}}(z)$	$\ge \alpha =0.95$?
$0$	$24/25=0.96$	yes
$100$	$25/25=1$	yes

The least crossing atom is $z=0$, so ${\mathrm{VaR}}_{0.95}(X)=0$ — and likewise for the second bond $Y$. This is theorem var_bond_eq_zero.

3. The independent sum, and where the tail comes from

For independent $X,Y$ the law of $X+Y$ is the convolution: joint outcomes are the product, values add, counts multiply. indepSumLaw bond bond yields four atoms (counts over $N=25^2=625$), which merge to the human-readable law:

$s$	atoms	merged count	$P(S=s)$
$0$	$(0)+(0)$	$24\cdot 24=576$	$576/625=0.9216$
$100$	$(0)+(100)$ and $(100)+(0)$	$24+24=48$	$48/625=0.0768$
$200$	$(100)+(100)$	$1$	$1/625=0.0016$

The two coincident $100$-atoms are exactly the mass the Finset collapse (§1) would have lost. Their CDF:

$z$	$F_S(z)$	$\ge \alpha =0.95$?
$0$	$576/625=0.9216$	no
$100$	$624/625=0.9984$	yes
$200$	$625/625=1$	yes

$F_S(0)=0.9216<0.95$: the mass at the best outcome no longer covers the confidence level, because there are now two ways to take a loss. The least crossing atom is $z=100$, so ${\mathrm{VaR}}_{0.95}(X+Y)=100$. This is theorem var_indepSum_eq_hundred.

4. The failure

${\mathrm{VaR}}_{0.95}(X+Y)=100>0=\underset{0}{\underbrace{{\mathrm{VaR}}_{0.95}(X)}}+\underset{0}{\underbrace{{\mathrm{VaR}}_{0.95}(Y)}}$

Pooling two independent risks raised the measured risk — the “diversification penalty” that makes VaR unsound as a risk objective. Sealed two ways: var_subadditivity_fails (a concrete existential witness) and var_not_subadditive (the negation of the universal axiom S).

5. Why VaR fails and CVaR does not

VaR reads a single point off the distribution — where the tail begins — and is blind to how the mass is arranged on either side of it. Subadditivity can break at that seam, as above. Artzner 1999’s representation theorem (§4.1) is the structural reason a coherent measure cannot: every coherent $\rho$ is a supremum of expectations over a convex set $\mathcal{Q}$ of scenario measures, $\rho (X)={\sup }_{Q\in \mathcal{Q}}{\mathbb{E}}_Q[X]$, and the supremum of a sum never exceeds the sum of suprema — subadditivity is one line. CVaR is exactly such a measure: its scenario set is the tail-reweighting envelope ${\mathcal{Q}}_{\alpha }=\{Q:dQ/dP\le \frac{1}{1-\alpha }\}$ (cvar_derivation_draft §3.3). So ${\mathrm{CVaR}}_{\alpha }(X+Y)\le {\mathrm{CVaR}}_{\alpha }(X)+{\mathrm{CVaR}}_{\alpha }(Y)$ always — it cannot manufacture the diversification penalty this module exhibits for VaR. That is why the thesis’ risk layer scores views with CVaR, not VaR.

6. Honest scope

This is a concrete counterexample on one finite discrete law, not a theory of risk measures. It refutes the universal subadditivity of VaR; it does not define VaR or CVaR in general, nor prove CVaR coherent in Lean (Mathlib has neither VaR nor CVaR — obligations row A2; §5 argues CVaR’s coherence on paper, from the cited sources, not by machine). The independence used to build $X+Y$ is a modelling choice matching Artzner’s i.i.d. example; the failure is, if anything, sharper for it (diversification of independent risks is where subadditivity is expected to help most). The sympy_pin fixes the same numbers in exact rationals as an independent cross-check of the integer-count kernel computation.

7. The machine seal

Elaborated standalone (lake env lean, not a full lake build — the orchestrator integrates the module into the root import list serially); axiom prints verbatim:

'Ctrllib.var_bond_eq_zero' depends on axioms: [propext]
'Ctrllib.var_indepSum_eq_hundred' depends on axioms: [propext]
'Ctrllib.var_subadditivity_fails' depends on axioms: [propext]
'Ctrllib.var_not_subadditive' depends on axioms: [propext]

No sorryAx, no Classical.choice, no Quot.sound, no interface hypotheses — interfaces_assumed: []. The seal rests on propext alone.