Reference · Finite types, distributions and Markov chains
rainbow.math.finite.bellman-stationary-policy-optimal
A concrete optimal-policy theorem for exact finite NNRAT Bellman models. Earlier generic policy-iteration theorems isolated optimality-fixed-point uniqueness as an abstract premise. This module discharges that premise with the exact Bellman uniqueness theorem: a policy value that is a fixed point of its policy backup and is greedy-consistent with the optimality operator is pointwise equivalent to any Bellman optimal fixed point. Carrier exhaustiveness and the exact discount gap/inverse identities remain explicit, matching the constructive contraction proof. Native, kernel-checked, and axiom-free on D63.
value/nnrat-stationary-bellman-policy-value-is-optimal
value/nnrat-stationary-bellman-policy-value-is-optimal.{u, v} :
(S : Type u) (A : Type v) (states : Finset S) (actions : Finset A)
(transition : S → A → S → ℚ≥0) (reward : S → A → ℚ≥0) (discount : ℚ≥0)
(fallback : S → A)
(fallback-admissible : ∀ (state : S), fallback state ∈ actions)
(normalized : markov/nnrat-rows-normalized S A states transition)
(state-covered : ∀ (state : S), state ∈ states)
(policy : S → A) (policy-value : S → ℚ≥0)
(policy-value-fixed : ∀ (state : S), policy-value state = backup state (policy state))
(greedy-consistent : ∀ (state : S), backup state (policy state) = step policy-value state)
(optimal-value : S → ℚ≥0)
(optimal-fixed : ∀ (state : S), step optimal-value state = optimal-value state)
(gap inverse : ℚ≥0)
(discount-plus-gap-one : discount + gap = 1)
(inverse-times-gap-one : inverse · gap = 1)
(state : S)
→ policy-value state = optimal-value state
where backup := bellman/nnrat-action-backup S A states transition reward discount policy-value
where step := value/nnrat-optimality-step S A actions fallback (bellman/nnrat-action-backup S A states transition reward discount)+ = nnrat/add1 = nnrat/one= = nnrat/equivalent: equality of rational valuesFinset = finset-data/Finset· = nnrat/multiplyℚ≥0 = nnrat/NonnegativeRational∈ = finset-data/to-set: membership in a finite set