The Axiom Profile of Computation

We report the axiom profiles of computability theory's central theorems when formalized from the equational theory of monoidal closed categories in Lean 4. Starting from a common categorical formalization, we find that core diagonal and fixed-point theorems — the Y combinator, Kleene's recursion theorem, halting undecidability, both Gödel incompleteness theorems, and Myhill's isomorphism theorem — are constructive (zero axioms); Rice's theorem sits exactly at a Markov boundary; and full logical determination first appears at excluded middle (Post's backward direction, whose dovetail totality condition we prove equivalent to EM). The partition tracks three regimes of the double-negation monad's counit within the fourth level of the fixed-point derivation, where self-indexing introduces extensional equivalence. Verified with twenty Lean 4 files (zero sorry, zero Classical.choice, zero custom axioms). Companion formalization archived at DOI:10.5281/zenodo.18915083.