Reference · Finite types, distributions and Markov chains

rainbow.math.finite.signed-argmax

Finite types, distributions and Markov chainssrc/rainbow/math/finite/signed_argmax.clj3 definitions, 8 theorems

Executable finite argmax over exact signed-rational scores. The fold accepts an explicit fallback action, compares scores with the computable signed order, and returns an action rather than only a maximum value. The certificates prove that the result comes from the declared finite carrier (when the fallback does) and dominates every declared action. Runtime carrier length and arbitrary signed scores are both supported. Native, kernel-checked, and axiom-free on D63.

Depends onmath.rational.signed.order-transitivitymath.rational.signed.minmax

decision/signed-select.{u} :
  (A : Type u) (score : A → ℚ) (x₁ x₂ : A)
  → A

list/signed-argmax-from.{u} :
  (A : Type u) (score : A → ℚ) (x₁ : A) (x₂ : List A)
  → A

decision/finite-signed-argmax.{u} :
  (A : Type u) (actions : Finset A) (initial : A) (score : A → ℚ)
  → A

decision/signed-select-is-left-or-right.{u} :
  (A : Type u) (score : A → ℚ) (left right : A)
  → proposition/disjunction (select = left) (select = right)
  where select := decision/signed-select A score left right

decision/signed-select-left-bound.{u} :
  (A : Type u) (score : A → ℚ) (left right : A)
  → score left ≤ score (decision/signed-select A score left right)

decision/signed-select-right-bound.{u} :
  (A : Type u) (score : A → ℚ) (left right : A)
  → score right ≤ score (decision/signed-select A score left right)

list/signed-argmax-from-bounds-initial.{u} :
  (A : Type u) (score : A → ℚ) (initial : A) (source : List A)
  → (fun source₁ => score initial ≤ score (list/signed-argmax-from A score initial source₁)) source

list/signed-argmax-from-bounds-member.{u} :
  (A : Type u) (score : A → ℚ) (initial : A) (source : List A) (value : A)
  (member : list/membership A source value)
  → score value ≤ score (list/signed-argmax-from A score initial source)

list/signed-argmax-from-is-initial-or-member.{u} :
  (A : Type u) (score : A → ℚ) (initial : A) (source : List A)
  → proposition/disjunction (list/signed-argmax-from A score initial source = initial) (membership)
  where membership := list/membership A source (list/signed-argmax-from A score initial source)

decision/finite-signed-argmax-is-member.{u} :
  (A : Type u) (actions : Finset A) (initial : A) (score : A → ℚ)
  (initial-member : initial ∈ actions)
  → decision/finite-signed-argmax A actions initial score ∈ actions

decision/finite-signed-argmax-dominates.{u} :
  (A : Type u) (actions : Finset A) (initial : A) (score : A → ℚ) (candidate : A)
  (candidate-member : candidate ∈ actions)
  → score candidate ≤ score (decision/finite-signed-argmax A actions initial score)