Reference · Logic

rainbow.math.logic.strict-contraction-stabilization

Logicsrc/rainbow/math/logic/strict_contraction_stabilization.clj1 definitions, 9 theorems

Constructive bounded stabilization of strict contractions in a finite Nat sup metric.

function/nat-iterate.{u} :
  (C : Type u) (transform : C → C) (x₁ : ℕ) (x₂ : C)
  → C

nat/at-most-successor-cancel :
  (left right : ℕ)
  (ordered : data/succ left ≤ data/succ right)
  → left ≤ right

nat/strict-below-of-strict-below-at-most-successor :
  (left middle bound : ℕ) (strict : nat/strict-below left middle)
  (bounded : middle ≤ data/succ bound)
  → left ≤ bound

nat/equal-zero-or-positive :
  (value : ℕ)
  → proposition/disjunction (value = 0) (nat/strict-below 0 value)

function/nat-iterate-zero.{u} :
  (C : Type u) (transform : C → C) (initial : C)
  → function/nat-iterate C transform 0 initial = initial

function/nat-iterate-successor.{u} :
  (C : Type u) (transform : C → C) (steps : ℕ) (initial : C)
  → function/nat-iterate C transform (data/succ steps) initial = transform (function/nat-iterate C transform steps initial)

nat/strictly-descending-sequence-reaches-zero-within-bound :
  (bound : ℕ) (sequence : ℕ → ℕ)
  (initial-bounded : sequence 0 ≤ bound)
  (descending : ∀ (steps : ℕ), ∀ (positive : nat/strict-below 0 (sequence steps)), nat/strict-below (sequence (data/succ steps)) (sequence steps))
  → proposition/existence ℕ (fun steps => proposition/conjunction (steps ≤ bound) (sequence steps = 0))

metric/strict-contraction-consecutive-iterate-distance-decreases.{u} :
  (A : Type u) (source : Finset A) (transform : (A → ℕ) → A → ℕ) (initial : A → ℕ)
  (strictly-contracts : ∀ (left : A → ℕ), ∀ (right : A → ℕ), ∀ (positive : nat/strict-below 0 (metric/finite-sup-distance A source left right)), nat/strict-below (metric/finite-sup-distance A source (transform left) (transform right)) (metric/finite-sup-distance A source left right))
  (steps : ℕ) (positive : nat/strict-below 0 (distance₁))
  → nat/strict-below (distance) (distance₁)
  where distance := metric/finite-sup-distance A source (function/nat-iterate (A → ℕ) transform (data/succ steps) initial) (function/nat-iterate (A → ℕ) transform (data/succ (data/succ steps)) initial)
  where distance₁ := metric/finite-sup-distance A source (function/nat-iterate (A → ℕ) transform steps initial) (function/nat-iterate (A → ℕ) transform (data/succ steps) initial)

metric/strict-contraction-iterate-stabilizes-within-initial-distance.{u} :
  (A : Type u) (source : Finset A) (transform : (A → ℕ) → A → ℕ) (initial : A → ℕ)
  (strictly-contracts : ∀ (left : A → ℕ), ∀ (right : A → ℕ), ∀ (positive : nat/strict-below 0 (metric/finite-sup-distance A source left right)), nat/strict-below (metric/finite-sup-distance A source (transform left) (transform right)) (metric/finite-sup-distance A source left right))
  → proposition/existence ℕ (fun steps => proposition/conjunction (steps ≤ distance) ((fun steps₁ => metric/finite-sup-distance A source (function/nat-iterate (A → ℕ) transform steps₁ initial) (function/nat-iterate (A → ℕ) transform (data/succ steps₁) initial)) steps = 0))
  where distance := metric/finite-sup-distance A source (function/nat-iterate (A → ℕ) transform 0 initial) (function/nat-iterate (A → ℕ) transform 1 initial)

metric/strict-contraction-has-bounded-support-fixed-point.{u} :
  (A : Type u) (source : Finset A) (transform : (A → ℕ) → A → ℕ) (initial : A → ℕ)
  (strictly-contracts : ∀ (left : A → ℕ), ∀ (right : A → ℕ), ∀ (positive : nat/strict-below 0 (metric/finite-sup-distance A source left right)), nat/strict-below (metric/finite-sup-distance A source (transform left) (transform right)) (metric/finite-sup-distance A source left right))
  → proposition/existence ℕ (fun steps => proposition/conjunction (steps ≤ distance) (∀ (state : A), ∀ (member : state ∈ source), transform (function/nat-iterate (A → ℕ) transform steps initial) state = function/nat-iterate (A → ℕ) transform steps initial state))
  where distance := metric/finite-sup-distance A source (function/nat-iterate (A → ℕ) transform 0 initial) (function/nat-iterate (A → ℕ) transform 1 initial)