Reference · Finite types, distributions and Markov chains

rainbow.math.finite.bellman-residual-certificate

Finite types, distributions and Markov chainssrc/rainbow/math/finite/bellman_residual_certificate.clj0 definitions, 4 theorems

A posteriori certificates for exact finite NNRAT Bellman solvers. For an exhaustive finite state carrier, the exact supremum radius and the Bellman contraction theorem give radius(candidate, fixed) <= radius(candidate, T candidate) + discount * radius(candidate, fixed). The NNRAT inverse-gap theorem then turns the computable Bellman residual into a sharp error certificate. A final stopping theorem accepts a checked residual threshold directly. Exhaustiveness is an explicit premise: `state-covered` proves that every inhabitant of S occurs in `states`; no finite fold is silently treated as covering a larger carrier. Native, kernel-checked, and axiom-free on D63.

Depends onmath.finite.bellman-value-iteration-convergesmath.finite.nnrat-sup-radius

nnrat/additive-upper-triangle :
  (left middle right first-radius second-radius : ℚ≥0)
  (first-bound : left ≤ middle + first-radius)
  (second-bound : middle ≤ right + second-radius)
  → left ≤ right + (first-radius + second-radius)

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

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

value/nnrat-optimality-fixed-point-stopping-certificate.{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)
  (fixed-value : S → ℚ≥0)
  (fixed-point : ∀ (state : S), step fixed-value state = fixed-value state)
  (candidate : S → ℚ≥0) (gap inverse : ℚ≥0)
  (discount-plus-gap-one : discount + gap = 1)
  (inverse-times-gap-one : inverse · gap = 1)
  (threshold : ℚ≥0)
  (residual-at-most-threshold : max state∈states |candidate state - step candidate state| ≤ threshold)
  → max s∈states |candidate s - fixed-value s| ≤ inverse · threshold
  where step := value/nnrat-optimality-step S A actions fallback (bellman/nnrat-action-backup S A states transition reward discount)