Survival probability is nonnegative
ProvedActuarialValuation.annualDecrementLaw_survival_nonnegativeactuarial-sciencemultiple-decrementreserves
The annual decrement law explicitly requires nonnegative survival mass.
Mathematical statement
Preamble
import Mathlib import Definitions.Def_actuarial_isAnnualDecrementLaw open MeasureTheory
Formal statement
namespace ActuarialValuation
theorem annualDecrementLaw_survival_nonnegative {J : Type*} [Fintype J] (p : ℝ) (q : J → ℝ)
(h : isAnnualDecrementLaw p q)
:
0 ≤ p := by sorry
end ActuarialValuationSource
Gerber, Life Insurance Mathematics (1997, third edition), Chapter 7 §7.5, equations (7.5.1)-(7.5.5); Dickson, Hardy and Waters (2009), Actuarial Mathematics for Life Contingent Risks, Chapter 8 §8.8 multiple decrement models, https://doi.org/10.1017/CBO9780511800146.009
Read-back
What the Lean code literally says, in plain math · gpt-6
Independent mathematical reading. The assumption is the locally defined annual decrement-law predicate. Its first conjunct directly states that p, the probability of staying in force through the year, is nonnegative. The theorem merely extracts that requirement and does not constrain the sign of any reserve or benefit amount.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.