Reference · Finite types, distributions and Markov chains

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

Finite types, distributions and Markov chains src/rainbow/math/finite/bellman_signed_fixed_point_uniqueness.clj0 definitions, 1 theorems

Uniqueness of signed Bellman optimality fixed points. Treat the first fixed point as a residual-certified candidate relative to the second. Its Bellman residual has zero finite signed sup distance, so the exact inverse-gap certificate forces the distance between the fixed points to zero. Finite signed metric separation then yields pointwise quotient equivalence over the entire carrier, using the explicit coverage witness. This proves uniqueness, not existence. Native, kernel-checked, and axiom-free on D63.

Depends onmath.finite.bellman-signed-greedy-policy

value/nnrat-transition-signed-optimality-fixed-points-unique

TheoremFor all inputsNo axiomsSource, line 136

value/nnrat-transition-signed-optimality-fixed-points-unique.{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)
  (left : S → ℚ)
  (left-fixed : ∀ (state : S), (fun value => fun state₁ => step value state₁) left state = left state)
  (right : S → ℚ)
  (right-fixed : ∀ (state : S), (fun value => fun state₁ => step value state₁) right state = right state)
  (gap inverse : ℚ)
  (inverse-nonnegative : 0 ≤ inverse)
  (discount-plus-gap-one : signed/from-nnrat discount + gap = 1)
  (inverse-times-gap-one : inverse · gap = 1)
  (state : S)
  → left state = right state
  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)

+ = signed/add0 = signed/zero1 = signed/one= = signed/equivalent: equality of rational valuesFinset = finset-data/Finset· = signed/multiplyℚ = signed/SignedRationalℚ≥0 = nnrat/NonnegativeRational∈ = finset-data/to-set: membership in a finite set≤ = signed/at-most