The Bounded-Construction Axiom: A Terminating Subclass of Computable Programs

Turing showed that no general algorithm decides whether an arbitrary program halts. This is often misread as a paradox that "programs cannot stop." We do not refute Turing. We isolate a checkable admission axiom—the Bounded-Construction Axiom—under which termination becomes a constructive consequence of program shape: every repetitive control flow must be realized by a loop equipped with a well-founded variant, and recursion is admitted only when it reduces to such a loop. We prove that every program satisfying the axiom terminates, hence lies in the total computable functions. Because Turing's theorem entails that any Turing-complete language must admit non-halting programs, the class we characterize is a proper, non-Turing-complete subclass; the axiom is therefore consistent with the undecidability of halting. The contribution is one of isolation and positioning, not of new mathematical results: we assemble classical ingredients (structured programming, loop variants, the total/partial distinction) into a single criterion that can be checked at write time.