Entry age, attained age and liability allocation: pfEntryLiability_zero_payroll
ProvedActuarialValuation.pfEntryLiability_zero_payrollactuarial-sciencedb-funding-experienceformal-verification
With no future payroll all remaining expected benefits form the funding liability. This original derived actuarial relation uses the parameter restrictions, endpoints and units stated in the separate formal theorem or definition.
Mathematical relation:
Preamble
import Mathlib.Data.Real.Basic import Mathlib.Algebra.BigOperators.Group.Finset.Basic import Definitions.Def_actuarial_pfEntryLiability
Formal statement
namespace ActuarialValuation theorem pfEntryLiability_zero_payroll (benefit rate : ℝ) : pfEntryLiability benefit 0 rate=benefit := by sorry end ActuarialValuation
Source
Original derived actuarial mathematics, published source page 7. Institute and Faculty of Actuaries, GN26 Pension Fund Terminology, §§4.5–4.9, https://www.actuaries.org.uk/system/files/documents/pdf/gn26v2-0.pdf; OECD Working Paper, Funding Rules and Actuarial Methods, §§74–76, https://www.oecd.org/content/dam/oecd/en/publications/reports/2006/10/funding-rules-and-actuarial-methods_g17a1941/274307371724.pdf; Actuarial Standards Board ASOP No.4, https://www.actuarialstandardsboard.org/asops/measuring-pension-obligations-determining-pension-plan-costs-contributions/. Parent topic: Entry age and attained age normal costs, aggregate and modified contributions, deficit amortisation and exact funding-surplus rollforward. The particular Lean formula is a new finite/real-algebraic formalisation and remains an unproved theorem target if labelled theorem. Relevant published actuarial derivation: https://www.actuaries.org.uk/system/files/documents/pdf/gn26v2-0.pdf
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.