Reference · Algorithm guarantees

rainbow.algorithms.proofs.dual-ascent

Algorithm guaranteessrc/rainbow/algorithms/proofs/dual_ascent.clj1 definitions, 3 theorems

AHoF O52 Dual Ascent: the dual-variable ascent step over vector-valued multipliers. The dual function's gradient at the current point is the primal constraint residual r = A*x - b, so the multiplier ascends along it: lambda' = lambda + rate * residual Every term is a finite-vector operation (scale, add), reusing the n-dimensional vector state shared by the constraint methods. The inner primal minimization x*(lambda) = argmin_x L(x, lambda) and the residual r = A*x - b are problem data supplied to the step (matrix application and argmin are not exact-rational in general and stay an executable-only concern); what is proved here is the deterministic ascent recurrence and worked instances from a zero-initialized multiplier (the standard start for dual ascent), where a unit-rate step lands the multiplier exactly on the residual by reflexivity. Scope (measured by the kernel): this module has 2 worked instances (statements about specific values) and 1 definitional unfoldings (true by unfolding a definition). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.dual-ascent` prints this classification.

Depends onmath.finite.vector

dual-ascent/ascent-step :
  (x₁ x₂ : List ℚ) (x₃ : ℚ≥0)
  → List ℚ

dual-ascent/ascent-unfold :
  (multiplier residual : List ℚ) (rate : ℚ≥0)
  → dual-ascent/ascent-step multiplier residual rate = vector/add multiplier (vector/scale rate residual)

dual-ascent/unit-step-2d-example :
  → dual-ascent/ascent-step [signed/from-nnrat 0, signed/from-nnrat 0] [signed/from-nnrat 3, signed/from-nnrat 2] 1 = [signed/from-nnrat 3, signed/from-nnrat 2]

dual-ascent/unit-step-3d-example :
  → dual-ascent/ascent-step [signed/from-nnrat 0, signed/from-nnrat 0, signed/from-nnrat 0] [signed/from-nnrat 2, signed/from-nnrat 4, signed/from-nnrat 6] 1 = [signed/from-nnrat 2, signed/from-nnrat 4, signed/from-nnrat 6]