Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.stieltjes

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

Stieltjes three-term recurrence for orthogonal polynomials (Kochenderfer Optimization O21.3), a signed-cluster algorithm deferred in August until the signed layer landed. The orthogonal-polynomial recurrence evaluates p_n(x) = (x - alpha) * p_{n-1}(x) - beta * p_{n-2}(x). As a higher-order composition of signed multiply and subtract: `optimization/stieltjes-step x alpha beta previous second = signed/subtract (signed/multiply (signed/subtract x alpha) previous) (signed/multiply beta second)`. The worked theorem proves one step for x=5, alpha=2, beta=1, p1=p2=1 -> (5-2)*1 - 1*1 = 2, by signed cross-product reflexivity. Chains signed-multiply; native and axiom-free on D63. A proved native module; formal ledger crediting is the separate catalog follow-up.

Depends onmath.rational.signed.multiply

optimization/stieltjes-step :
  (x₁ x₂ x₃ x₄ x₅ : ℚ)
  → ℚ

optimization/stieltjes-step-worked :
  → optimization/stieltjes-step (signed/from-nnrat 5) (signed/from-nnrat 2) (signed/from-nnrat 1) (signed/from-nnrat 1) (signed/from-nnrat 1) = signed/from-nnrat 2

optimization/stieltjes-step-preserves-zero :
  (x alpha beta : ℚ)
  → optimization/stieltjes-step x alpha beta 0 0 = 0