Descent Is a Reduction: A Kolmogorov–Arnold Network That Proves Its Own Training, Down to the Silicon

Abstract

A training step is usually a number that goes down on a plot. We make it a theorem. We exhibit a finite rational Kolmogorov–Arnold network whose evaluation, squared-error loss, and least-squares gradient are each a composition of a single primitive — the binary integer-arithmetic active pair, the smallest local rewrite of an interaction net — and we prove that one gradient step strictly decreases the loss, the decrease computed entirely by that primitive, with an empty axiom footprint, that the network's output equals the reduction of its own net, and that a network with a wrong parameter is carried by one exact step to the correct network with zero loss. The gradient that drives the step is itself reverse-mode backpropagation: we prove the backward pass — the chain rule — is the same active-pair reduction, its per-edge backward maps summing to the network's gradient, and that one exact gradient step trains an entire one-parameter family of wrong networks to zero loss. Because the network is a net, the verified object and the executed object coincide. The same arithmetic nets the proof reduces are reduced on graphics-processor silicon, and the result read back is identical, byte for byte, across an ordinary processor, a discrete accelerator, and a unified-memory device, and equal to the value the proof predicts. The three artifacts of trustworthy learning — the specification of the algorithm, its verification, and the kernel that runs it — collapse to one structure observed at three resolutions. We argue this is the natural home for a small but load-bearing class of learning systems: those whose correctness must be a theorem about the thing that actually runs. Published by The Institute for Applied Ontological Mathematics.