Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.gauss-seidel

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/gauss_seidel.clj1 definitions, 2 theorems

Gauss-Seidel coordinate update (Kochenderfer Optimization O24.1), the last of the four signed-cluster algorithms deferred in August. The Gauss-Seidel sweep updates each coordinate against the current values of the others: x_i = (b_i - sum_{j!=i} a_ij x_j) / a_ii. The August note deferred this expecting signed division; keeping the diagonal a POSITIVE nnrat makes the division an nnrat reciprocal and the update a signed scale, so no signed division is needed: `optimization/gauss-seidel-step diagonal target off-diagonal = signed/scale (nnrat/reciprocal diagonal) (signed/subtract target off-diagonal)`. The worked theorem proves one 2-variable coordinate update -- diagonal a11=2, target b1=4, off-diagonal a12*x2 = 1 -> (4-1)/2 = 3/2 -- by signed cross-product reflexivity. Chains rational-division; native and axiom-free on D63. A proved native module; formal ledger crediting is the separate catalog follow-up. With this the four August-deferred signed-cluster algorithms (LQR, NNLS, Stieltjes, Gauss-Seidel) are all proved. This module also proves the UNIVERSAL exactness property -- the update satisfies its coordinate equation for every target and off-diagonal -- and two general signed lemmas proved en route that fill genuine corpus gaps (a subtract-then- add recovery law and reciprocal-scale cancellation); those two are general enough to promote to a core signed module later.

Depends onmath.rational.divisionmath.rational.signed.recovery-laws

optimization/gauss-seidel-step :
  (x₁ : ℚ≥0) (x₂ x₃ : ℚ)
  → ℚ

optimization/gauss-seidel-step-worked :
  → optimization/gauss-seidel-step 2 (signed/from-nnrat 4) (signed/from-nnrat 1) = signed/from-nnrat 3/2

optimization/gauss-seidel-step-exact :
  (p q : ℕ) (target off-diagonal : ℚ)
  → signed/scale (nnrat/make (data/succ p) q) (step) + off-diagonal = target
  where step := optimization/gauss-seidel-step (nnrat/make (data/succ p) q) target off-diagonal