Prove2Me

Three-state rating migration and recoverable default claims: crRatingExpectedPay_zero

Proved
ActuarialValuation.crRatingExpectedPay_zero

by WillR · Oct 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

actuarial-credit-default-migrationactuarial-scienceformal-verification

A bond with zero state-contingent benefit has no payout. This original derived actuarial relation uses the parameter restrictions, endpoints and units stated in the separate formal theorem or definition.

Mathematical relation:

∑jPij=1,Pdefault,default=1\sum_j P_{ij}=1,\quad P_{\text{default,default}}=1
Preamble
import Mathlib.Data.Real.Basic
import Mathlib.Algebra.Order.Group.MinMax
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Mathlib.Data.Fintype.Basic
import Mathlib.Analysis.SpecialFunctions.Log.Deriv
import Definitions.Def_actuarial_crRatingExpectedPay
Formal statement
namespace ActuarialValuation

theorem crRatingExpectedPay_zero (P : Fin 3 → Fin 3 → ℝ) (i : Fin 3) : crRatingExpectedPay P i (fun _ => 0)=0 := by sorry

end ActuarialValuation
Source
Original derived actuarial mathematics, published source page 451. Robert C. Merton (1974), On the Pricing of Corporate Debt, Journal of Finance 29(2), 449–470, https://doi.org/10.1111/j.1540-6261.1974.tb03058.x; Jarrow, Lando and Turnbull (1997), Markov Model for the Term Structure of Credit Risk Spreads, https://doi.org/10.1093/rfs/10.2.481. Parent topic: Merton-style terminal firm assets, debt/equity limited liability, credit spread and absorbing finite-state rating transition and default-recovery bond cashflows. 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://doi.org/10.1111/j.1540-6261.1974.tb03058.x
Human review

  • Endorsed by Shuze Chen · Oct 11, 2026

    Confirmed by the moderator at approval.

  • Endorsed by WillR · Oct 11, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph