Positive probability weights give nonnegative quantile excess premium
ProvedActuarialValuation.tailRiskStopLoss_nonnegactuarial-scienceaggregate-claimsformal-verification
Natural-number excess payments are never negative. Weighting them by nonnegative claim probabilities preserves nonnegativity term by term in the finite stop-loss sum.
Mathematical statement
Preamble
import Mathlib import Definitions.Def_actuarial_tailRiskStopLoss
Formal statement
namespace ActuarialValuation theorem tailRiskStopLoss_nonneg (w : ℕ → ℝ) (bound q : ℕ) (hw : ∀ s, 0 ≤ w s) : 0 ≤ tailRiskStopLoss w bound q := by sorry end ActuarialValuation
Source
S David Promislow (2015), Fundamentals of Actuarial Mathematics (3rd ed), sec 22.5.3 Definition 22.5 and eq (22.9), library PDF pages 439-442; finite discrete stop-loss representation and VaR atom allocation
Read-back
What the Lean code literally says, in plain math · gpt-6
Independent mathematical reading. Each claim excess is computed using saturating subtraction in the natural numbers and then converted to a real nonnegative amount. Multiplication by the separately assumed nonnegative claim coefficient preserves its sign, so the bounded stop-loss premium is nonnegative.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.