Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.nnls

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

Nonnegative projection for NNLS (Kochenderfer Optimization O13.4), a signed-cluster algorithm deferred in August: over nonnegative rationals the projection is degenerate, so it needed the signed layer's max(x,0). `optimization/nnls-project x = signed/max x signed/zero` clamps a signed value up to zero -- the projection onto the nonnegative orthant that each NNLS coordinate step applies. Two worked theorems cover both branches: a positive value passes through (max 5 0 ~ 5), a negative value projects to zero (max -3 0 ~ 0), each by signed cross-product reflexivity. Chains signed-minmax for signed/max; native and axiom-free on D63. A proved native module; formal ledger crediting is the separate catalog follow-up.

Depends onmath.rational.signed.minmax

optimization/nnls-project :
  (x₁ : ℚ)
  → ℚ

optimization/nnls-project-positive-worked :
  → optimization/nnls-project (signed/from-nnrat 5) = signed/from-nnrat 5

optimization/nnls-project-negative-worked :
  → optimization/nnls-project (signed/negate (signed/from-nnrat 3)) = 0

optimization/nnls-project-nonnegative :
  (value : ℚ)
  → 0 ≤ optimization/nnls-project value

optimization/nnls-project-fixes-nonnegative :
  (value : ℚ)
  (nonnegative : 0 ≤ value)
  → optimization/nnls-project value = value