Nonnegative claim weights yield a nonnegative strict tail
ProvedActuarialValuation.tailRiskStrictMass_nonnegactuarial-scienceaggregate-claimsformal-verification
Every included tail coefficient is nonnegative, and all coefficients at losses no larger than q are replaced by zero. The finite strict-tail mass therefore cannot be negative.
Mathematical statement
Preamble
import Mathlib import Definitions.Def_actuarial_tailRiskStrictMass
Formal statement
namespace ActuarialValuation theorem tailRiskStrictMass_nonneg (w : ℕ → ℝ) (bound q : ℕ) (hw : ∀ s, 0 ≤ w s) : 0 ≤ tailRiskStrictMass 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. All individual claim coefficients are assumed nonnegative, and the strict-tail indicator either selects a coefficient or supplies zero. Hence each finite summand is nonnegative and the entire tail sum cannot be negative. The lemma does not require total probability one.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.