Reference · Algorithm guarantees
rainbow.algorithms.proofs.counterfactual-distance-laws
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.
counterfactual/distance-squared-symmetric
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
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
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