Reference · Signed rationals

rainbow.math.rational.signed.vector-sup-distance

Signed rationalssrc/rainbow/math/rational/signed/vector_sup_distance.clj3 definitions, 18 theorems

Finite maxima and sup distance for signed-rational list vectors. The older V1.54 metric is Nat-valued over functions on an explicit finite carrier. Affine Rainbow states are lists of signed rationals, so this module supplies the representation bridge they actually need: a universe-polymorphic signed map-max fold with zero base, and the maximum component distance of two signed lists. The fold has structural, nonnegativity, boundedness, and congruence laws. Vector sup distance has a component-bound predicate, structural equations, nonnegativity, a global pointwise upper bound, symmetry, and zero on the diagonal. Native, kernel-checked, and axiom-free on D63.

Depends onmath.rational.signed.distance

list/signed-map-max.{u} :
  (A : Type u) (mapping : A → ℚ) (x₁ : List A)
  → ℚ

vector/sup-distance :
  (x₁ x₂ : List ℚ)
  → ℚ

vector/within :
  (x₁ : ℚ) (x₂ x₃ : List ℚ)
  → Prop

list/signed-map-max-empty.{u} :
  (A : Type u) (mapping : A → ℚ)
  → list/signed-map-max A mapping [] = 0

signed/equivalent-of-equality :
  (left right : ℚ)
  (same : left = right)
  → left = right

list/signed-map-max-cons.{u} :
  (A : Type u) (mapping : A → ℚ) (head : A) (tail : List A)
  → list/signed-map-max A mapping (data/cons A head tail) = signed/max (mapping head) (list/signed-map-max A mapping tail)

list/signed-map-max-nonnegative.{u} :
  (A : Type u) (mapping : A → ℚ) (source : List A)
  → 0 ≤ list/signed-map-max A mapping source

list/signed-map-max-bounded.{u} :
  (A : Type u) (mapping : A → ℚ) (upper : ℚ)
  (zero-upper : 0 ≤ upper)
  (source : List A)
  (pointwise : ∀ (value : A), ∀ (member : list/membership A source value), mapping value ≤ upper)
  → list/signed-map-max A mapping source ≤ upper

list/signed-map-max-congruent.{u} :
  (A : Type u) (left right : A → ℚ)
  (pointwise : ∀ (value : A), left value = right value)
  (source : List A)
  → list/signed-map-max A left source = list/signed-map-max A right source

vector/sup-distance-empty-left :
  (right : List ℚ)
  → vector/sup-distance [] right = 0

vector/sup-distance-empty-right :
  (left : List ℚ)
  → vector/sup-distance left [] = 0

vector/sup-distance-cons :
  (left-head : ℚ) (left-tail : List ℚ) (right-head : ℚ) (right-tail : List ℚ)
  → vector/sup-distance (data/cons ℚ left-head left-tail) (data/cons ℚ right-head right-tail) = signed/max (signed/distance left-head right-head) (distance)
  where distance := vector/sup-distance left-tail right-tail

vector/sup-distance-nonnegative :
  (left right : List ℚ)
  → 0 ≤ vector/sup-distance left right

vector/sup-distance-cons-bounded :
  (left-head : ℚ) (left-tail : List ℚ) (right-head : ℚ) (right-tail : List ℚ)
  (upper : ℚ)
  (head-bound : signed/distance left-head right-head ≤ upper)
  (tail-bound : vector/sup-distance left-tail right-tail ≤ upper)
  → vector/sup-distance (data/cons ℚ left-head left-tail) (data/cons ℚ right-head right-tail) ≤ upper

vector/sup-distance-bounded :
  (left right : List ℚ) (upper : ℚ)
  (zero-upper : 0 ≤ upper)
  (pointwise : vector/within upper left right)
  → vector/sup-distance left right ≤ upper

vector/sup-distance-cons-symmetric :
  (left-head : ℚ) (left-tail : List ℚ) (right-head : ℚ) (right-tail : List ℚ)
  (tail-same : vector/sup-distance left-tail right-tail = vector/sup-distance right-tail left-tail)
  → vector/sup-distance (data/cons ℚ left-head left-tail) (data/cons ℚ right-head right-tail) = vector/sup-distance (data/cons ℚ right-head right-tail) (data/cons ℚ left-head left-tail)

vector/sup-distance-empty-symmetric :
  (values : List ℚ)
  → vector/sup-distance [] values = vector/sup-distance values []

vector/sup-distance-cons-empty-symmetric :
  (head : ℚ) (tail : List ℚ)
  → vector/sup-distance (data/cons ℚ head tail) [] = vector/sup-distance [] (data/cons ℚ head tail)

vector/sup-distance-cons-symmetric-all :
  (left-head : ℚ) (left-tail : List ℚ)
  (tail-symmetry : ∀ (right-tail : List ℚ), vector/sup-distance left-tail right-tail = vector/sup-distance right-tail left-tail)
  (right : List ℚ)
  → vector/sup-distance (data/cons ℚ left-head left-tail) right = vector/sup-distance right (data/cons ℚ left-head left-tail)

vector/sup-distance-symmetric :
  (left right : List ℚ)
  → vector/sup-distance left right = vector/sup-distance right left

vector/sup-distance-self-zero :
  (values : List ℚ)
  → vector/sup-distance values values = 0