Nonnegative cause masses yield a nonnegative annual death mass
ProvedActuarialValuation.decrementYearMass_nonnegactuarial-scienceformal-mathematicsmortality-risk
All cause incidence masses are nonnegative by assumption. Adding finitely many such masses gives a nonnegative aggregate termination probability in the year, including the possibility that every cause has probability zero.
Mathematical statement
Preamble
import Mathlib import Definitions.Def_actuarial_decrementYearMass
Formal statement
namespace ActuarialValuation
theorem decrementYearMass_nonneg {C : Type*} [Fintype C]
(w : ℕ → C → ℝ) (t : ℕ) (hw : ∀ c, 0 ≤ w t c) :
0 ≤ decrementYearMass w t := by sorry
end ActuarialValuationSource
Shiu and Xiong (2021), DOI https://doi.org/10.1007/s13385-020-00256-9; original multiple-decrement and cause-covariance extension in this mission
Read-back
What the Lean code literally says, in plain math · gpt-6
Independent mathematical reading. The source assumes each individual time-t cause mass is nonnegative. Its conclusion is only that the aggregate finite cause sum cannot be negative. It does not require a normalised distribution over time or any in-force survival-tail assumption, and remains valid when no cause can occur in the chosen year.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.