Reference · Signed rationals
rainbow.math.rational.signed.absolute-convex
Absolute value is convex -- the canonical non-smooth convex function, the basis of L1 / robust / minimax objectives. signed/absolute-convex : convex-on (x |-> |x|) i.e. |(w0)x + (w1)y| <= (w0)|x| + (w1)|y| for w0+w1~1. The triangle inequality bounds |(w0)x + (w1)y| by |(w0)x| + |(w1)y|; each term rewrites via |a*b| ~ |a|*|b| and |from-nnrat w| ~ from-nnrat w (weights are nonnegative) to (w0)|x| + (w1)|y|. Wall-free (no reciprocal); does not touch the LP checker.
signed/absolute-convex
signed/absolute-convex : → signed/convex-on (fun x => signed/absolute x)