A zero-year Markov policy has its terminal cost
ProvedActuarialValuation.finiteEntropicPolicyValue_zeroFor a horizon of zero policy years there is no action, no transition and no covered future cashflow. The fixed policy's recursively valued insurance cost equals the supplied terminal valuation for the current state. The result holds for arbitrary risk and discount parameters because the stage operator is never invoked.
Mathematical statement
import Mathlib import Definitions.Def_actuarial_finiteEntropicPolicyValue
namespace ActuarialValuation
theorem finiteEntropicPolicyValue_zero {S A : Type*}
[Fintype S] (P : S → A → S → ℝ)
(cost : S → A → S → ℝ) (beta gamma : ℝ)
(terminal : S → ℝ) (policy : ℕ → S → A) (s : S) :
finiteEntropicPolicyValue P cost beta gamma terminal policy 0 s =
terminal s := by sorry
end ActuarialValuationRead-back
What the Lean code literally says, in plain math · gpt-6
Independent mathematical reading. Evaluating the recursively defined cost for a fixed Markov policy at horizon zero returns the terminal function exactly at the chosen state. There is no state transition or stage cost in that branch. The equality does not depend on whether transition weights are stochastic or the cost-risk aversion gamma is positive, because the entropic stage operator is not called at this horizon.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.