A note on the rectangular Schoenberg-Whitney theorem for clamped B-splines
Shutao Tang, Zixuan Zhao
math.NA
Oct 17, 2026 · v1
cs.GR
TL;DR
An attempted Lean formalization of the published proof uncovered the incorrect inequality; no Lean artifact is described.
Abstract
Wang et al.(Computer-Aided Design 40 (2008) 999-1008) proposed a knot-subsequence characterization of full row rank for rectangular B-spline collocation matrices. We identify an incorrect inequality in their Appendix proof, which invalidates the argument as written, and make explicit the endpoint and multiplicity conventions on which the criterion depends. The defect lies in the proof, not in the underlying result, which is valid under suitably stated hypotheses; in the lofting construction of Wang et al. these hypotheses are implicitly satisfied, so the lofted curves are unaffected. We state the corrected result and give a new proof, independent of the disputed argument, for clamped B-splines of arbitrary degree with continuous interior multiplicities. In our proof, sufficiency follows from inclusion of spline spaces and knot insertion; necessity selects independent columns and builds the reduced knot vector from them. The proof uses no recursive column-selection construction.
Problem
Wang et al. (2008) gave a knot-subsequence criterion for full row rank of rectangular B-spline collocation matrices, which underlies energy-minimizing B-spline lofting. Their Appendix proof contains an incorrect inequality and leaves the endpoint and multiplicity conventions implicit.
Approach
The work began as an attempt to formalize the original proof in the Lean proof assistant, and that attempt exposed the defect. The authors localize the error and give counterexamples showing which conventions are needed. They then state a corrected theorem for clamped B-splines with interior multiplicities at most the degree. The new proof derives sufficiency from spline-space inclusion and knot insertion, and necessity by selecting independent columns and building the reduced knot vector from them.
Results
The corrected criterion holds in the continuous, clamped, endpoint-aware setting, and each hypothesis is shown to be essential. The lofting construction of Wang et al. satisfies these hypotheses, so its lofted curves are unaffected.
