Deterministic annual cash cost shifts entropic stage value equally
ProvedActuarialValuation.finiteEntropicStageCost_cash_addAdding a deterministic immediate cost k to every next-state outcome under the selected action multiplies the conditional exponential moment by exp(gammak), whose logarithm shifts by gammak. Division by nonzero gamma yields a shift of k in the stage value. Normalised nonnegative transition weights guarantee positive log arguments.
Mathematical statement
import Mathlib import Definitions.Def_actuarial_finiteEntropicStageCost
namespace ActuarialValuation
theorem finiteEntropicStageCost_cash_add {S A : Type*} [Fintype S]
(P : S → A → S → ℝ) (cost : S → A → S → ℝ)
(beta gamma : ℝ) (next : S → ℝ) (s : S) (a : A) (k : ℝ)
(hP : ∀ t, 0 ≤ P s a t)
(hsum : (∑ t : S, P s a t) = 1)
(hgamma : gamma ≠ 0) :
finiteEntropicStageCost P (fun x b t => cost x b t + k)
beta gamma next s a =
finiteEntropicStageCost P cost beta gamma next s a + k := by sorry
end ActuarialValuationRead-back
What the Lean code literally says, in plain math · gpt-6
Independent mathematical reading. The first stage valuation replaces every immediate annual transition cost throughout the model by the cost plus one fixed deterministic constant k. At the chosen state and action all exponentials therefore gain the same factor exp(gammak), so the log moment increases by gammak. With gamma nonzero and a nonnegative normalised row, the entropic stage value rises by precisely k. It is an annual cashflow shift, not a scaling of next-year risk.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.