Reference · Logic

rainbow.math.logic.strict-contraction-uniqueness

Logicsrc/rainbow/math/logic/strict_contraction_uniqueness.clj0 definitions, 5 theorems

Constructive uniqueness of support-relative fixed points for strict finite contractions.

nat/equal-zero-of-not-positive :
  (value : ℕ) (not-positive : nat/strict-below 0 value → proposition/falsity)
  → value = 0

list/nat-map-max-congruent-on.{u} :
  (A : Type u) (left right : A → ℕ) (source : List A)
  (pointwise : ∀ (value : A), ∀ (member : list/membership A source value), left value = right value)
  → list/nat-map-max A left source = list/nat-map-max A right source

metric/finite-sup-congruent-on.{u} :
  (A : Type u) (source : Finset A)
  (left-before right-before left-after right-after : A → ℕ)
  (left-pointwise : ∀ (state : A), ∀ (member : state ∈ source), left-before state = left-after state)
  (right-pointwise : ∀ (state : A), ∀ (member : state ∈ source), right-before state = right-after state)
  → metric/finite-sup-distance A source left-before right-before = metric/finite-sup-distance A source left-after right-after

metric/strict-contraction-fixed-points-have-zero-sup-distance.{u} :
  (A : Type u) (source : Finset A) (transform : (A → ℕ) → A → ℕ) (left right : A → ℕ)
  (strictly-contracts : ∀ (candidate-left : A → ℕ), ∀ (candidate-right : A → ℕ), ∀ (positive : nat/strict-below 0 (metric/finite-sup-distance A source candidate-left candidate-right)), nat/strict-below (metric/finite-sup-distance A source (transform candidate-left) (transform candidate-right)) (metric/finite-sup-distance A source candidate-left candidate-right))
  (left-fixed : ∀ (state : A), ∀ (member : state ∈ source), transform left state = left state)
  (right-fixed : ∀ (state : A), ∀ (member : state ∈ source), transform right state = right state)
  → metric/finite-sup-distance A source left right = 0

metric/strict-contraction-fixed-points-unique-on-support.{u} :
  (A : Type u) (source : Finset A) (transform : (A → ℕ) → A → ℕ) (left right : A → ℕ)
  (strictly-contracts : ∀ (candidate-left : A → ℕ), ∀ (candidate-right : A → ℕ), ∀ (positive : nat/strict-below 0 (metric/finite-sup-distance A source candidate-left candidate-right)), nat/strict-below (metric/finite-sup-distance A source (transform candidate-left) (transform candidate-right)) (metric/finite-sup-distance A source candidate-left candidate-right))
  (left-fixed : ∀ (state : A), ∀ (member : state ∈ source), transform left state = left state)
  (right-fixed : ∀ (state : A), ∀ (member : state ∈ source), transform right state = right state)
  (state : A)
  (member : state ∈ source)
  → left state = right state