The Axiom Profile of Computation

Reports the axiom profiles of computability theory's central theorems when formalized from the equational theory of monoidal closed categories in Lean 4. Core theorems — the Y combinator, Kleene's recursion theorem, halting undecidability, both Gödel incompleteness theorems, Myhill's isomorphism theorem — are constructive (zero axioms). Rice's theorem sits exactly at a Markov boundary. Full excluded middle first appears at Post's backward direction. The partition tracks three regimes of the double-negation monad's counit, established by twenty standalone Lean 4 files with zero sorry and zero Classical.choice.