Finite discounted death–annuity summation identity
Provedactuarial_c_discounted_survival_annuity_conservationactuarial-scienceinsurancelife-contingency
For any real survival sequence, discount v and number of years n, prove the weighted year-to-year survival decrements plus effective-discounted annuity due cashflows plus terminal survival value equal initial survival mass. This is the exact discrete-time identity that underlies the conventional finite insurance–annuity relationship, including the zero-horizon boundary.
The original mathematical identity is an open formal mission target. Its type has been copied exactly from a successful private remote Lean proof, which does not establish acceptance of this individual Prove2Me target.
Preamble
import Mathlib.Data.Real.Basic import Mathlib.Algebra.BigOperators.Group.Finset.Basic
Formal statement
theorem actuarial_c_discounted_survival_annuity_conservation (s : ℕ → ℝ)
(v : ℝ) (n : ℕ) :
(∑ j ∈ Finset.range n,
v^(j+1) * (s j - s (j+1))) +
(1-v)*(∑ j ∈ Finset.range n, v^j * s j) +
v^n * s n = s 0 := by sorry
Source
Original actuarial formalisation informed by S. David Promislow (2015), Fundamentals of Actuarial Mathematics, third edition, Chapters 3 and 5. Where the result is pure finite-sum algebra, it is an independently derived supporting identity, not claimed as a verbatim textbook theorem.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.