Skip to content
Rainbow docs menu

Reference · Algorithm guarantees

rainbow.algorithms.proofs.counterfactual-distance-laws

Algorithm guaranteessrc/rainbow/algorithms/proofs/counterfactual_distance_laws.clj0 definitions, 3 theorems

Native algebraic laws for exact counterfactual squared distance. counterfactual/distance-squared-symmetric counterfactual/distance-squared-self-zero counterfactual/distance-squared-zero-of-equivalent Symmetry transports norm invariance under negation across `-(left - right) ~ right - left`. Self-distance and equivalence use the shape-preserving zero vector and squared-norm congruence. Native and axiom-free on D63.

Depends onalgorithms.proofs.counterfactual-distance-separation

counterfactual/distance-squared-symmetric

TheoremFor all inputsNo axiomsSource, line 73

counterfactual/distance-squared-symmetric :
  (left right : List ℚ)
  → counterfactual/distance-squared left right = counterfactual/distance-squared right left

= = signed/equivalent: equality of rational valuesList = data/Listℚ = signed/SignedRational

counterfactual/distance-squared-self-zero

TheoremFor all inputsNo axiomsSource, line 101

counterfactual/distance-squared-self-zero :
  (values : List ℚ)
  → counterfactual/distance-squared values values = 0

0 = signed/zero= = signed/equivalent: equality of rational valuesList = data/Listℚ = signed/SignedRational

counterfactual/distance-squared-zero-of-equivalent

TheoremFor all inputsNo axiomsSource, line 125

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

0 = signed/zero= = signed/equivalent: equality of rational valuesList = data/Listℚ = signed/SignedRational