Reference · Finite types, distributions and Markov chains

rainbow.math.finite.bellman-policy-residual-certificate

Finite types, distributions and Markov chainssrc/rainbow/math/finite/bellman_policy_residual_certificate.clj0 definitions, 8 theorems

Residual certificates and uniqueness for exact finite fixed-policy Bellman operators. The module first factors the metric argument into a reusable contracted-image theorem. It then instantiates action-backup contraction at `policy state`, obtaining the same sharp inverse-gap residual and stopping certificates as for Bellman optimality. Zero residual plus metric separation yields pointwise uniqueness of fixed-policy values. `state-covered` remains explicit whenever a finite radius must supply a carrier-wide contraction premise. Native, kernel-checked, and axiom-free on D63.

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

metric/finite-nnrat-sup-radius-self-bound-of-contracted-image.{u} :
  (A : Type u) (source : Finset A) (candidate image fixed-value : A → ℚ≥0) (rate : ℚ≥0)
  (contracted-pointwise : ∀ (state : A), ∀ (member : state ∈ source), proposition/conjunction (image state ≤ fixed-value state + rate · (max s∈source |candidate s - fixed-value s|)) (fixed-value state ≤ image state + rate · (max s∈source |candidate s - fixed-value s|)))
  → max s∈source |candidate s - fixed-value s| ≤ max s∈source |candidate s - image s| + rate · (max s∈source |candidate s - fixed-value s|)

bellman/nnrat-policy-step-fixed-point-contraction.{u, v} :
  (S : Type u) (A : Type v) (states : Finset S) (transition : S → A → S → ℚ≥0)
  (reward : S → A → ℚ≥0) (discount : ℚ≥0) (policy : S → A)
  (normalized : markov/nnrat-rows-normalized S A states transition)
  (fixed-value : S → ℚ≥0)
  (fixed-point : ∀ (state : S), bellman/nnrat-action-backup S A states transition reward discount fixed-value state (policy state) = fixed-value state)
  (left-value : S → ℚ≥0) (epsilon : ℚ≥0)
  (left-pointwise : ∀ (state : S), left-value state ≤ fixed-value state + epsilon)
  (right-pointwise : ∀ (state : S), fixed-value state ≤ left-value state + epsilon)
  (state : S)
  → proposition/conjunction (backup ≤ fixed-value state + discount · epsilon) (fixed-value state ≤ backup + discount · epsilon)
  where backup := bellman/nnrat-action-backup S A states transition reward discount left-value state (policy state)

bellman/nnrat-policy-fixed-point-sup-radius-self-bound.{u, v} :
  (S : Type u) (A : Type v) (states : Finset S) (transition : S → A → S → ℚ≥0)
  (reward : S → A → ℚ≥0) (discount : ℚ≥0) (policy : S → A)
  (normalized : markov/nnrat-rows-normalized S A states transition)
  (state-covered : ∀ (state : S), state ∈ states)
  (fixed-value : S → ℚ≥0)
  (fixed-point : ∀ (state : S), backup fixed-value state (policy state) = fixed-value state)
  (candidate : S → ℚ≥0)
  → max s∈states |candidate s - fixed-value s| ≤ max state∈states |candidate state - backup candidate state (policy state)| + discount · (max s∈states |candidate s - fixed-value s|)
  where backup := bellman/nnrat-action-backup S A states transition reward discount

bellman/nnrat-policy-fixed-point-residual-bound.{u, v} :
  (S : Type u) (A : Type v) (states : Finset S) (transition : S → A → S → ℚ≥0)
  (reward : S → A → ℚ≥0) (discount : ℚ≥0) (policy : S → A)
  (normalized : markov/nnrat-rows-normalized S A states transition)
  (state-covered : ∀ (state : S), state ∈ states)
  (fixed-value : S → ℚ≥0)
  (fixed-point : ∀ (state : S), backup fixed-value state (policy 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 - backup candidate state (policy state)|)
  where backup := bellman/nnrat-action-backup S A states transition reward discount

bellman/nnrat-policy-fixed-point-stopping-certificate.{u, v} :
  (S : Type u) (A : Type v) (states : Finset S) (transition : S → A → S → ℚ≥0)
  (reward : S → A → ℚ≥0) (discount : ℚ≥0) (policy : S → A)
  (normalized : markov/nnrat-rows-normalized S A states transition)
  (state-covered : ∀ (state : S), state ∈ states)
  (fixed-value : S → ℚ≥0)
  (fixed-point : ∀ (state : S), backup fixed-value state (policy 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 - backup candidate state (policy state)| ≤ threshold)
  → max s∈states |candidate s - fixed-value s| ≤ inverse · threshold
  where backup := bellman/nnrat-action-backup S A states transition reward discount

bellman/nnrat-policy-fixed-point-residual-radius-zero.{u, v} :
  (S : Type u) (A : Type v) (states : Finset S) (transition : S → A → S → ℚ≥0)
  (reward : S → A → ℚ≥0) (discount : ℚ≥0) (policy : S → A) (value : S → ℚ≥0)
  (fixed-point : ∀ (state : S), backup state (policy state) = value state)
  → max state∈states |value state - backup state (policy state)| = 0
  where backup := bellman/nnrat-action-backup S A states transition reward discount value

bellman/nnrat-policy-fixed-points-have-zero-sup-radius.{u, v} :
  (S : Type u) (A : Type v) (states : Finset S) (transition : S → A → S → ℚ≥0)
  (reward : S → A → ℚ≥0) (discount : ℚ≥0) (policy : S → A)
  (normalized : markov/nnrat-rows-normalized S A states transition)
  (state-covered : ∀ (state : S), state ∈ states)
  (left-value : S → ℚ≥0)
  (left-fixed-point : ∀ (state : S), backup left-value state (policy state) = left-value state)
  (right-value : S → ℚ≥0)
  (right-fixed-point : ∀ (state : S), backup right-value state (policy 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 backup := bellman/nnrat-action-backup S A states transition reward discount

bellman/nnrat-policy-fixed-points-unique.{u, v} :
  (S : Type u) (A : Type v) (states : Finset S) (transition : S → A → S → ℚ≥0)
  (reward : S → A → ℚ≥0) (discount : ℚ≥0) (policy : S → A)
  (normalized : markov/nnrat-rows-normalized S A states transition)
  (state-covered : ∀ (state : S), state ∈ states)
  (left-value : S → ℚ≥0)
  (left-fixed-point : ∀ (state : S), backup left-value state (policy state) = left-value state)
  (right-value : S → ℚ≥0)
  (right-fixed-point : ∀ (state : S), backup right-value state (policy 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 backup := bellman/nnrat-action-backup S A states transition reward discount