Reference · Finite types, distributions and Markov chains

rainbow.math.finite.bellman-fixed-point-uniqueness

Finite types, distributions and Markov chainssrc/rainbow/math/finite/bellman_fixed_point_uniqueness.clj0 definitions, 3 theorems

Constructive uniqueness of exact finite NNRAT Bellman optimality fixed points. A fixed point has zero computable Bellman residual radius. The sharp inverse-gap stopping certificate therefore forces the finite supremum radius between any two fixed points to zero, and NNRAT metric separation turns that into pointwise quotient equivalence. As in the residual certificate, `state-covered` explicitly proves that the exact finite state enumeration exhausts S. This is what upgrades finite-fold bounds to the carrier-wide premise required by Bellman contraction. Native, kernel-checked, and axiom-free on D63.

Depends onmath.finite.bellman-residual-certificatemath.rational.nnrat.metric-separation

value/nnrat-optimality-fixed-point-residual-radius-zero.{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) (candidate : S → ℚ≥0)
  (candidate-fixed-point : ∀ (state : S), step state = candidate state)
  → max state∈states |candidate state - step state| = 0
  where step := value/nnrat-optimality-step S A actions fallback (bellman/nnrat-action-backup S A states transition reward discount) candidate

value/nnrat-optimality-fixed-points-have-zero-sup-radius.{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)
  (left-value : S → ℚ≥0)
  (left-fixed-point : ∀ (state : S), step left-value state = left-value state)
  (right-value : S → ℚ≥0)
  (right-fixed-point : ∀ (state : S), step right-value state = right-value state)
  (gap inverse : ℚ≥0)
  (discount-plus-gap-one : discount + gap = 1)
  (inverse-times-gap-one : inverse · gap = 1)
  → max s∈states |left-value s - right-value s| = 0
  where step := value/nnrat-optimality-step S A actions fallback (bellman/nnrat-action-backup S A states transition reward discount)

value/nnrat-optimality-fixed-points-unique.{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)
  (left-value : S → ℚ≥0)
  (left-fixed-point : ∀ (state : S), step left-value state = left-value state)
  (right-value : S → ℚ≥0)
  (right-fixed-point : ∀ (state : S), step right-value state = right-value state)
  (gap inverse : ℚ≥0)
  (discount-plus-gap-one : discount + gap = 1)
  (inverse-times-gap-one : inverse · gap = 1)
  (state : S)
  → left-value state = right-value state
  where step := value/nnrat-optimality-step S A actions fallback (bellman/nnrat-action-backup S A states transition reward discount)