Reference · Algorithm guarantees

rainbow.algorithms.proofs.counterfactual-distance-separation

Algorithm guaranteessrc/rainbow/algorithms/proofs/counterfactual_distance_separation.clj0 definitions, 4 theorems

Native separation laws for the existing counterfactual squared distance. signed/subtract-zero-reflects-equivalence vector/subtract-zero-reflects-equivalence counterfactual/distance-squared-nonnegative counterfactual/equivalent-of-distance-squared-zero Vector subtraction truncates, so separation explicitly requires equal shape. Under that hypothesis, zero squared distance reflects each component through signed subtraction and yields vector/equivalent. Native and axiom-free.

Depends onmath.linear.vector.norm-zero-reflection

signed/subtract-zero-reflects-equivalence :
  (left right : ℚ)
  (difference-zero : left - right = 0)
  → left = right

vector/subtract-zero-reflects-equivalence :
  (left right : List ℚ) (shape : vector/same-shape left right)
  (difference-zero : vector/equivalent (vector/subtract left right) (vector/zero-like (vector/subtract left right)))
  → vector/equivalent left right

counterfactual/distance-squared-nonnegative :
  (left right : List ℚ)
  → signed/nonnegative (counterfactual/distance-squared left right)

counterfactual/equivalent-of-distance-squared-zero :
  (left right : List ℚ) (shape : vector/same-shape left right)
  (distance-zero : counterfactual/distance-squared left right = 0)
  → vector/equivalent left right