CLASSO: a practical primal path-following algorithm for the constrained LASSO

We present CLASSO, a path-following method for the LASSO subject to general linear equality and inequality constraints. The local direction is obtained from a quadratic programme on an augmented active set, which determines both the coefficients that leave zero and the weakly active inequalities that remain binding. For a positive-definite Hessian and a nonempty feasible set, this programme has a unique primal minimiser, even when the binding constraint rows are dependent, and gives the local derivative of the solution path. The construction recovers the LASSO-modified LARS direction without constraints, and over the full cone gives the segment leaving the origin. We prove that the primal path is piecewise affine with finitely many kinks, without a constraint qualification or unique multipliers. A finite path does not imply a finite traversal: re-certifying at each kink can fail to terminate. CLASSO instead follows the minimum-norm certificate along a lexicographic rate; we prove that this rule reaches λ=0 in exact arithmetic within an explicit bound and traverses the whole path. These results are machine-checked in Lean~4, and the floating-point implementation agrees with an exact rational one on all 210 small test problems. We assess the implementation on a 39-case synthetic suite and six constrained versions of the diabetes benchmark. On the 31 nontrivial synthetic cases with n≥ p, sampled relative objective differences from numerical reference solves are below 10-9 in magnitude; unnormalised endpoint differences reach 1.5×10-7 in magnitude. For n<p, matched differences range from -3.6×10-7 to 2×10-9 across five ridge strengths. Across the synthetic and diabetes benchmarks, checks of all 580 recorded segments found no missed interior event and all checked KKT residuals within the stated tolerances.