Basic unilateral CVA = (1−R)·∫₀ᵀ EE(u)·e^(−ru)·h(u)·S(u) du

[raphaelrrcoelho]

Context

The (unilateral) credit valuation adjustment prices counterparty default risk as expected
exposure integrated against the risk-neutral default-time density. It is the natural downstream
consumer of the deterministic hazard curve S(u) = exp(−∫₀^u h) in FixedIncome/HazardCurve.lean,
whose default density is h(u)·S(u) — the same credit-triangle marginal as cdsFairSpread.

Task

Define cva for a deterministic expected-exposure profile EE : ℝ → ℝ and prove
CVA = (1−R)·∫₀^T EE(u)·e^{−r u}·h(u)·S(u) du. Specialise to constant exposure EE ≡ E₀ and
constant hazard h to get the closed form CVA = (1−R)·E₀·(h/(r+h))·(1 − e^{−(r+h)T}).

Acceptance criteria

• A full (or library_wrapper) benchmark entry deriving the result; axioms-clean.
• Coverage row + AxiomAudit + ledger updated.

Pointers

• MathFin/FixedIncome/HazardCurve.lean (cumHazard, hazardSurvival),
  MathFin/FixedIncome/Credit.lean (survivalProbability, cdsFairSpread),
  MathFin/FixedIncome/CDSTimeVarying.lean (annuity/losses integral pattern).