Reference · Finite types, distributions and Markov chains

rainbow.math.finite.bellman-signed-policy-dominance

Finite types, distributions and Markov chainssrc/rainbow/math/finite/bellman_signed_policy_dominance.clj0 definitions, 10 theorems

Dominance of admissible signed policy values by Bellman optimality. The concrete signed Bellman operator over normalized nnrat transitions is monotone. A generic induction keeps every post-fixed value below all iterates, while generic rate-limit lemmas turn a convergence certificate and those iterate bounds into pointwise dominance. A named normalized-transition Bellman operator and low-arity iterator keep the concrete policy-value dominance capstone below the kernel reduction budget. The earlier rejected inlined formulations remain documented as negative evidence. The installed lemmas are native, kernel-checked, and axiom-free on D63.

Depends onmath.finite.bellman-signed-policy-optimalmath.rational.signed.rate-ordermath.finite.bellman-signed-operator-fixed-point-convergencemath.finite.bellman-signed-transition-operator

value/nnrat-transition-signed-optimality-step-monotone.{u, v} :
  (S : Type u) (A : Type v) (states : Finset S) (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 right : S → ℚ)
  (ordered : ∀ (state : S), left state ≤ right state)
  (state : S)
  → (fun value => fun state₁ => step value state₁) left state ≤ (fun value => fun state₁ => step value 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 (transition state₃ action₁ next-state)) reward (signed/from-nnrat discount) value₁ state₂ action)

value/signed-abstract-post-fixed-value-below-sequence.{u} :
  (S : Type u) (operator : (S → ℚ) → S → ℚ) (sequence : ℕ → S → ℚ) (value : S → ℚ)
  (below-operator : ∀ (state : S), value state ≤ operator value state)
  (operator-monotone : ∀ (left : S → ℚ), ∀ (right : S → ℚ), ∀ (ordered : ∀ (state : S), left state ≤ right state), ∀ (state : S), operator left state ≤ operator right state)
  (sequence-zero : sequence 0 = value)
  (sequence-successor : ∀ (steps : ℕ), sequence (data/succ steps) = operator (sequence steps))
  (steps : ℕ) (state : S)
  → value state ≤ sequence steps state

value/signed-policy-fixed-point-below-optimality-step.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (backup : (S → ℚ) → S → A → ℚ) (value : S → ℚ) (policy : S → A)
  (policy-admissible : ∀ (state : S), policy state ∈ actions)
  (policy-fixed : ∀ (state : S), backup value state (policy state) = value state)
  (state : S)
  → value state ≤ value/signed-optimality-step S A actions fallback backup value state

value/signed-rate-limit-dominates-below-iterates.{u} :
  (S : Type u) (sequence : ℕ → S → ℚ) (limit-value lower-value : S → ℚ) (error : ℕ → ℚ)
  (modulus : ℕ → ℕ) (error-null : analysis/signed-rate-null error modulus)
  (below-sequence : ∀ (steps : ℕ), ∀ (state : S), lower-value state ≤ sequence steps state)
  (sequence-upper : ∀ (steps : ℕ), ∀ (state : S), sequence steps state ≤ limit-value state + error steps)
  (state : S)
  → lower-value state ≤ limit-value state

value/signed-convergence-certificate-dominates-below-value.{u} :
  (S : Type u) (sequence : ℕ → S → ℚ) (limit-value lower-value : S → ℚ) (error : ℕ → ℚ)
  (modulus : ℕ → ℕ)
  (converged : proposition/conjunction (analysis/signed-rate-null error modulus) (∀ (steps : ℕ), ∀ (state : S), proposition/conjunction (sequence steps state ≤ limit-value state + error steps) (limit-value state ≤ sequence steps state + error steps)))
  (below-sequence : ∀ (steps : ℕ), ∀ (state : S), lower-value state ≤ sequence steps state)
  (state : S)
  → lower-value state ≤ limit-value state

value/signed-post-fixed-value-below-operator-iterate.{u} :
  (S : Type u) (operator : (S → ℚ) → S → ℚ) (value : S → ℚ)
  (below-operator : ∀ (state : S), value state ≤ operator value state)
  (operator-monotone : ∀ (left : S → ℚ), ∀ (right : S → ℚ), ∀ (ordered : ∀ (state : S), left state ≤ right state), ∀ (state : S), operator left state ≤ operator right state)
  (steps : ℕ) (state : S)
  → value state ≤ (fun steps₁ => value/signed-operator-iterate S operator steps₁ value) steps state

value/nnrat-transition-signed-optimality-operator-monotone.{u, v} :
  (discount : ℚ≥0) (S : Type u) (A : Type v) (states : Finset S) (actions : Finset A)
  (transition : S → A → S → ℚ≥0) (reward : S → A → ℚ) (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 right : S → ℚ)
  (ordered : ∀ (state : S), left state ≤ right state)
  (state : S)
  → operator left state ≤ operator right state
  where operator := value/nnrat-transition-signed-optimality-operator S A states actions transition reward discount fallback

value/nnrat-transition-signed-policy-fixed-point-below-optimality-operator.{u, v} :
  (discount : ℚ≥0) (S : Type u) (A : Type v) (states : Finset S) (actions : Finset A)
  (transition : S → A → S → ℚ≥0) (reward : S → A → ℚ) (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)
  (value : S → ℚ) (policy : S → A)
  (policy-admissible : ∀ (state : S), policy state ∈ actions)
  (policy-fixed : ∀ (state : S), (fun value₁ => fun state₁ => fun action => 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) value₁ state₁ action) value state (policy state) = value state)
  (state : S)
  → value state ≤ value/nnrat-transition-signed-optimality-operator S A states actions transition reward discount fallback value state

value/nnrat-transition-signed-policy-value-below-optimality-operator-iterate.{u, v} :
  (discount : ℚ≥0) (S : Type u) (A : Type v) (states : Finset S) (actions : Finset A)
  (transition : S → A → S → ℚ≥0) (reward : S → A → ℚ) (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)
  (policy : S → A)
  (policy-admissible : ∀ (state : S), policy state ∈ actions)
  (policy-value : S → ℚ)
  (policy-fixed : ∀ (state : S), (fun value => fun state₁ => fun action => 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) value state₁ action) policy-value state (policy state) = policy-value state)
  (steps : ℕ) (state : S)
  → policy-value state ≤ (fun steps₁ => value/signed-operator-iterate S (operator) steps₁ policy-value) steps state
  where operator := value/nnrat-transition-signed-optimality-operator S A states actions transition reward discount fallback

value/nnrat-transition-signed-policy-value-below-optimality-fixed-point.{u, v} :
  (ap gp : ℕ) (S : Type u) (A : Type v) (states : Finset S) (actions : Finset A)
  (transition : S → A → S → ℚ≥0) (reward : S → A → ℚ) (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/nnrat-transition-signed-optimality-operator S A states actions transition reward (make) fallback fixed-value state = fixed-value state)
  (policy : S → A)
  (policy-admissible : ∀ (state : S), policy state ∈ actions)
  (policy-value : S → ℚ)
  (policy-fixed : ∀ (state : S), (fun value => fun state₁ => fun action => 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 (make)) value state₁ action) policy-value state (policy state) = policy-value state)
  (initial-error : ℚ)
  (initial-error-nonnegative : 0 ≤ initial-error)
  (initial-bound : initial-error ≤ signed/from-nnrat (nnrat/general-harmonic ap gp 0))
  (initial-close : ∀ (state : S), proposition/conjunction (policy-value state ≤ fixed-value state + initial-error) (fixed-value state ≤ policy-value state + initial-error))
  (state : S)
  → policy-value state ≤ fixed-value state
  where make := nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))