Reference · Finite types, distributions and Markov chains

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

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

A posteriori residual certificates for signed Bellman optimality. A generic finite-function theorem combines the signed sup metric, scalar triangle inequality, and a two-sided additive contraction to establish d(v,v*) <= d(v,Tv) + rate*d(v,v*). The checked signed inverse-gap theorem then isolates the unknown fixed-point distance. Bellman capstones instantiate the generic result with ordinary normalized nnrat transition kernels, arbitrary signed rewards and values, and the runtime finite-action maximum. This verifies mathematical certificates, not an executable solver. State coverage and fixed-point existence remain explicit premises. Native, kernel-checked, and axiom-free on D63.

Depends onmath.finite.signed-sup-distancemath.finite.bellman-signed-value-iteration-general-converges

metric/finite-signed-sup-distance-self-bound-of-additive-contraction.{u} :
  (S : Type u) (states : Finset S)
  (state-covered : ∀ (state : S), state ∈ states)
  (operator : (S → ℚ) → S → ℚ) (rate : ℚ)
  (rate-nonnegative : 0 ≤ rate)
  (contractive : ∀ (left-value : S → ℚ), ∀ (right-value : S → ℚ), ∀ (epsilon : ℚ), ∀ (left-pointwise : ∀ (state : S), left-value state ≤ right-value state + epsilon), ∀ (right-pointwise : ∀ (state : S), right-value state ≤ left-value state + epsilon), ∀ (state : S), proposition/conjunction (operator left-value state ≤ operator right-value state + rate · epsilon) (operator right-value state ≤ operator left-value state + rate · epsilon))
  (fixed-value : S → ℚ)
  (fixed-point : ∀ (state : S), operator fixed-value state = fixed-value state)
  (candidate : S → ℚ)
  → distance ≤ metric/finite-signed-sup-distance S states candidate (operator candidate) + rate · distance
  where distance := metric/finite-signed-sup-distance S states candidate fixed-value

value/nnrat-transition-signed-optimality-fixed-point-sup-distance-self-bound.{u, v} :
  (S : Type u) (A : Type v) (states : Finset S)
  (state-covered : ∀ (state : S), state ∈ states)
  (actions : Finset A) (transition : S → A → S → ℚ≥0) (reward : S → A → ℚ)
  (discount : ℚ≥0) (fallback : S → A)
  (fallback-admissible : ∀ (state : S), fallback state ∈ actions)
  (normalized : ∀ (state : S), ∀ (action : A), probability/nnrat-total-mass S states (transition state action) = 1)
  (fixed-value : S → ℚ)
  (fixed-point : ∀ (state : S), value/signed-optimality-step S A actions fallback (fun value => fun state₁ => fun action => backup value state₁ action) fixed-value state = fixed-value state)
  (candidate : S → ℚ)
  → distance ≤ metric/finite-signed-sup-distance S states candidate ((fun value => fun state => step value state) candidate) + signed/from-nnrat discount · distance
  where backup := bellman/signed-action-backup S A states (fun state₂ => fun action₁ => fun next-state => signed/from-nnrat (transition state₂ action₁ next-state)) reward (signed/from-nnrat discount)
  where distance := metric/finite-signed-sup-distance S states candidate fixed-value
  where step := value/signed-optimality-step S A actions fallback (fun value₁ => fun state₁ => fun action => bellman/signed-action-backup S A states (fun state₂ => fun action₁ => fun next-state => …⟨1⟩ …⟨7⟩) reward (signed/from-nnrat discount) value₁ state₁ action)

value/nnrat-transition-signed-optimality-fixed-point-residual-bound.{u, v} :
  (S : Type u) (A : Type v) (states : Finset S)
  (state-covered : ∀ (state : S), state ∈ states)
  (actions : Finset A) (transition : S → A → S → ℚ≥0) (reward : S → A → ℚ)
  (discount : ℚ≥0) (fallback : S → A)
  (fallback-admissible : ∀ (state : S), fallback state ∈ actions)
  (normalized : ∀ (state : S), ∀ (action : A), probability/nnrat-total-mass S states (transition state action) = 1)
  (fixed-value : S → ℚ)
  (fixed-point : ∀ (state : S), value/signed-optimality-step S A actions fallback (fun value => fun state₁ => fun action => backup value state₁ action) fixed-value state = fixed-value state)
  (candidate : S → ℚ) (gap inverse : ℚ)
  (inverse-nonnegative : 0 ≤ inverse)
  (discount-plus-gap-one : signed/from-nnrat discount + gap = 1)
  (inverse-times-gap-one : inverse · gap = 1)
  → distance fixed-value ≤ inverse · distance ((fun value => fun state => step value state) candidate)
  where backup := bellman/signed-action-backup S A states (fun state₂ => fun action₁ => fun next-state => signed/from-nnrat (transition state₂ action₁ next-state)) reward (signed/from-nnrat discount)
  where distance := metric/finite-signed-sup-distance S states candidate
  where step := value/signed-optimality-step S A actions fallback (fun value₁ => fun state₁ => fun action => bellman/signed-action-backup S A states (fun state₂ => fun action₁ => fun next-state => …⟨1⟩ …⟨7⟩) reward (signed/from-nnrat discount) value₁ state₁ action)

value/nnrat-transition-signed-optimality-fixed-point-stopping-certificate.{u, v} :
  (S : Type u) (A : Type v) (states : Finset S)
  (state-covered : ∀ (state : S), state ∈ states)
  (actions : Finset A) (transition : S → A → S → ℚ≥0) (reward : S → A → ℚ)
  (discount : ℚ≥0) (fallback : S → A)
  (fallback-admissible : ∀ (state : S), fallback state ∈ actions)
  (normalized : ∀ (state : S), ∀ (action : A), probability/nnrat-total-mass S states (transition state action) = 1)
  (fixed-value : S → ℚ)
  (fixed-point : ∀ (state : S), value/signed-optimality-step S A actions fallback (fun value => fun state₁ => fun action => backup value state₁ action) fixed-value state = fixed-value state)
  (candidate : S → ℚ) (gap inverse : ℚ)
  (inverse-nonnegative : 0 ≤ inverse)
  (discount-plus-gap-one : signed/from-nnrat discount + gap = 1)
  (inverse-times-gap-one : inverse · gap = 1)
  (threshold : ℚ)
  (residual-at-most-threshold : distance ((fun value => fun state => step value state) candidate) ≤ threshold)
  → distance fixed-value ≤ inverse · threshold
  where backup := bellman/signed-action-backup S A states (fun state₂ => fun action₁ => fun next-state => signed/from-nnrat (transition state₂ action₁ next-state)) reward (signed/from-nnrat discount)
  where distance := metric/finite-signed-sup-distance S states candidate
  where step := value/signed-optimality-step S A actions fallback (fun value₁ => fun state₁ => fun action => bellman/signed-action-backup S A states (fun state₂ => fun action₁ => fun next-state => signed/from-nnrat (…⟨1⟩ …⟨1⟩ …⟨1⟩ …⟨1⟩)) reward (signed/from-nnrat discount) value₁ state₁ action)