Reference · Algorithm guarantees

rainbow.algorithms.proofs.box-projection

Algorithm guaranteessrc/rainbow/algorithms/proofs/box_projection.clj1 definitions, 5 theorems

AHoF box projection (the projection step of Projected Gradient Descent and box-constrained optimization): after an unconstrained gradient step lands at x, the iterate is projected back onto the feasible box [lo, hi] by clamping, clamp lo hi x = max(lo, min(x, hi)) using the decidable rational order. The projection is designed to keep every iterate in the box (lo <= clamp lo hi x <= hi); that is NOT proved here for all inputs. The gradient step itself is an executable concern; what is proved here is the clamp operation and worked instances on the box [2, 8]: clamp 5 = 5 (identity inside), clamp 10 = 8 and clamp 1 = 2 (saturation at the active bound), and feasibility of those two, clamp 10 <= 8 and 2 <= clamp 1. Requires nnrat/at-most, audit/decide-nnrat-at-most, nnrat/decide-at-most-true-sound, and logic/if-data (all carried by the D63 checkpoint). Scope (measured by the kernel): this module has 5 worked instances (statements about specific values). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.box-projection` prints this classification.

projection/clamp :
  (x₁ x₂ x₃ : ℚ≥0)
  → ℚ≥0

projection/clamp-inside :
  → projection/clamp 2 8 5 = 5

projection/clamp-above :
  → projection/clamp 2 8 10 = 8

projection/clamp-below :
  → projection/clamp 2 8 1 = 2

projection/clamp-below-hi :
  → projection/clamp 2 8 10 ≤ 8

projection/clamp-above-lo :
  → 2 ≤ projection/clamp 2 8 1