Reference · Algorithm guarantees

rainbow.algorithms.proofs.counterfactual-objective-laws

Algorithm guaranteessrc/rainbow/algorithms/proofs/counterfactual_objective_laws.clj1 definitions, 4 theorems

Native guarantees for the exact counterfactual optimization objective. counterfactual/objective = distance-squared + scale(weight, class-penalty) signed/scale-nonnegative counterfactual/objective-nonnegative counterfactual/distance-squared-at-most-objective counterfactual/equivalent-of-objective-zero A nonnegative-rational weight preserves a nonnegative signed penalty. Hence the objective is nonnegative, cannot undercut its proximity term, and—under the necessary same-shape hypothesis—can be zero only for equivalent plans. Native and axiom-free on D63.

Depends onalgorithms.proofs.counterfactual-distance-laws

counterfactual/objective :
  (x₁ x₂ : List ℚ) (x₃ : ℚ≥0) (x₄ : ℚ)
  → ℚ

signed/scale-nonnegative :
  (rate : ℚ≥0) (value : ℚ) (value-nonnegative : signed/nonnegative value)
  → signed/nonnegative (signed/scale rate value)

counterfactual/objective-nonnegative :
  (original candidate : List ℚ) (weight : ℚ≥0) (class-penalty : ℚ)
  (penalty-nonnegative : signed/nonnegative class-penalty)
  → signed/nonnegative (counterfactual/objective original candidate weight class-penalty)

counterfactual/distance-squared-at-most-objective :
  (original candidate : List ℚ) (weight : ℚ≥0) (class-penalty : ℚ)
  (penalty-nonnegative : signed/nonnegative class-penalty)
  → counterfactual/distance-squared original candidate ≤ counterfactual/objective original candidate weight class-penalty

counterfactual/equivalent-of-objective-zero :
  (original candidate : List ℚ) (weight : ℚ≥0) (class-penalty : ℚ)
  (shape : vector/same-shape original candidate)
  (penalty-nonnegative : signed/nonnegative class-penalty)
  (objective-zero : counterfactual/objective original candidate weight class-penalty = 0)
  → vector/equivalent original candidate