Prove2Me

Ceded claim amount is nonnegative

Proved
ActuarialValuation.cededExcessLoss_nonnegative

by WillR · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

dynamic-programmingfinite-horizonreinsurance

The ceded claim equals z minus a number no larger than z, so is nonnegative for every real inputs.

Mathematical statement

c(z,a)≥0c(z,a)\ge0
Preamble
import Mathlib
import Definitions.Def_actuarial_cededExcessLoss
open MeasureTheory
Formal statement
namespace ActuarialValuation

theorem cededExcessLoss_nonnegative (z a : ℝ)
  :
  0 ≤ cededExcessLoss z a := by sorry

end ActuarialValuation
Source
Brachetta and Ceci (2019), Optimal Excess-of-Loss Reinsurance for Stochastic Factor Risk Models, Risks 7(2) 48, DOI https://doi.org/10.3390/risks7020048, §2 retained loss min(z,alpha), §3 HJB optimisation; Puterman (1994), Markov Decision Processes: Discrete Stochastic Dynamic Programming, Chapter 4 finite-horizon Bellman/backward induction, https://doi.org/10.1002/9780470316887.ch4
Read-back

What the Lean code literally says, in plain math · gpt-6

Independent mathematical reading. The gross claim minus the minimum of gross claim and retention is nonnegative for every real z and a, because the minimum is no greater than z. The theorem is algebraic and does not require both inputs to be nonnegative.

Human review

  • Endorsed by Shuze Chen · Oct 9, 2026

    Confirmed by the moderator at approval.

  • Endorsed by WillR · Oct 9, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph