Zero-year optimal entropic valuation equals terminal cost
ProvedActuarialValuation.finiteEntropicBellmanValue_zeroAt a zero-horizon valuation date, the optimiser cannot improve or worsen an immediate given terminal reserve or terminal insurance loss. The Bellman value is exactly that terminal amount, even if the state type is empty or the discount factor is zero.
Mathematical statement
import Mathlib import Definitions.Def_actuarial_finiteEntropicBellmanValue
namespace ActuarialValuation
theorem finiteEntropicBellmanValue_zero {S A : Type*}
[Fintype S] [Fintype A] [Nonempty A]
(P : S → A → S → ℝ)
(cost : S → A → S → ℝ) (beta gamma : ℝ)
(terminal : S → ℝ) (s : S) :
finiteEntropicBellmanValue P cost beta gamma terminal 0 s =
terminal s := by sorry
end ActuarialValuationRead-back
What the Lean code literally says, in plain math · gpt-6
Independent mathematical reading. The cost-minimising Bellman recursion makes no decision at zero remaining policy years and consequently returns the given terminal value for every state. A finite nonempty action type is part of the general Bellman definition's signature but is not used to choose any action at zero years. This base case is independent of probability normalisation and risk or discount restrictions.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.