Markov ⇔ partial recursive, twice — Detlovs' equivalence in Lean 4

A machine-checked development of Detlovs' theorem — Markov normal algorithms compute exactly the partial recursive functions — in Lean 4 over Mathlib, with the hard (compilation) direction proved twice, by two independent routes:

• machine simulation (ComputabilityEquivalence/Models/PartrecMarkovFinal.lean): compile through Mathlib's Partrec → TM2 → TM1 → TM0 spine, simulate the resulting Turing machine by a normal algorithm, and wrap the simulation in Markov-level unary encoders and decoders (partrec_to_markovComputesStrict, markovSpoke);
• the Detlovs-faithful compiler (ComputabilityEquivalence/Models/Detlovs*.lean): a direct constructor induction over Mathlib's vector basis Nat.Partrec', emitting a normal algorithm per constructor and composing them by program-level sequencing — the method of Detlovs' original 1958 paper (Trudy Mat. Inst. Steklov. 52, 75–139), with no machine model of any kind: the module's transitive import closure contains no Turing machine, project- or Mathlib-side (detlovs_partrec_to_markovComputesStrict, markovSpokeDetlovs).

Both routes land the strict, textbook convention: on every input outside the function's domain the constructed algorithm has no output word at all (MarkovComputesStrict), not merely no unary one. The interpretation direction (markov_to_partrec) closes the equivalence. The development also contains a complete register-machine (URM) spoke — RegisterComputes f ↔ Nat.Partrec f, interpreter and compiler — and classical corollaries: a universal normal algorithm exists, and no normal algorithm decides halting.

Every result is proved with no sorry, no admit, no added axioms and no native_decide; the axioms of every one of the project's declarations are at most Lean's standard [propext, Classical.choice, Quot.sound] (see Verification below).

The theorem graph

                         LambdaComputable
                               ↕
                               │
TMComputable     ↔       Nat.Partrec       ↔     RegisterComputes
                               │
                               ↕
                          MarkovComputes

Nat.Partrec is the extensional hub. A concrete model is a completed spoke only after proving both directions of Computes f ↔ Nat.Partrec f; the Markov spoke (twice-proved compilation) and the register spoke are complete. TMComputable and LambdaComputable are placeholder names for predicates not defined here (the lambda semantics is defined; its "computes" predicate and spoke are not).

Highlights

Result	Lean name(s)
Literal Markov semantics: first applicable rule in scheme order, leftmost occurrence, terminal rules, halt-when-stuck; fuelled runs and graph semantics	Markov.step, Markov.run, Markov.Outputs (Models/Markov.lean)
Interpretation: a normal algorithm's function is partial recursive	markov_to_partrec
Compilation, machine-simulation route — in the strict (inapplicability) convention	partrec_to_markovComputesStrict, partrecToMarkovStatement
Compilation, Detlovs-faithful route: every Nat.Partrec' function has a compiled block, then unary wrapper + alphabet truncation	Detlovs.hasBlock_partrec', Detlovs.exists_wrapped, detlovs_partrec_to_markovComputesStrict, detlovs_partrecToMarkovStatement
The Markov spoke, packaged — via either route, at both conventions	markovSpoke, markovSpokeStrict, markovSpokeDetlovs, markovSpokeStrictDetlovs
The graph and strict conventions agree extensionally	markovComputes_iff_strict
A universal normal algorithm exists (one program, one alphabet, all partial recursive functions via Nat.pair-coded input)	markov_universal
No normal algorithm decides halting	markov_halting_undecidable
TM0 machines simulated by normal algorithms, with the completeness converse	tm0_simulated_by_markov, tm0_eval_dom_of_markov_outputs
Alphabet flattening onto literal Fin (k+1), transporting runs and total divergence	Markov.exists_flatten_unary_strict
Register-machine (URM) spoke, both directions	register_to_partrec, registerComputes_of_partrec, registerSpoke

The design of both routes — the calling convention, the block specification with its exit characterization, the solo-control-letter discipline that stands in for a program counter, the composition/ primitive-recursion/minimization schemas, the unary wrapper, and the machine-simulation phases — is described in docs/ARCHITECTURE.md.

Verification

The trust basis is the Lean 4 kernel (toolchain v4.31.0) and Lean's three standard axioms. Concretely:

• Axioms, per declaration. Sweeping every constant the project defines — 4,556 of them, including auxiliaries, match functions and equation lemmas — 1,529 depend on no axioms at all, 749 on propext alone, 9 on Quot.sound alone, 1,782 on propext + Quot.sound, and 487 on the standard three with Classical.choice. None uses anything else: no sorryAx, no ofReduceBool (i.e. no native_decide), no custom axioms.
• External kernel replay. Every module has been re-checked by the toolchain's external checker (leanchecker), which replays each declaration through a fresh kernel — the standard defense against elaborator- or metaprogram-level tricks. The sources contain no metaprogramming at all (no elab, macro, unsafe, partial def, @[implemented_by], or @[extern]), and the only set_options used are autoImplicit false and maxRecDepth.
• Executable ground truth. Concrete programs are run inside Lean by kernel-reduced run fixtures, fuel-exact (run N … = some out alongside run (N−1) … = none), including the wrapper applied to real emitted blocks; each nontrivial program shape is also validated by an independent Python implementation of the semantics under scripts/.
• Statement fidelity. The finals are restated bare against the literal definitions of MarkovComputes/MarkovComputesStrict, and every compiled constructor case closes by a bare exact against Mathlib's Nat.Partrec'/Nat.Primrec' inductives.

Building

lake exe cache get
lake build

The project is pinned to Lean/Mathlib v4.31.0 (lean-toolchain, lake-manifest.json); lake exe cache get downloads the prebuilt Mathlib olean cache, after which the project's own 59 Lean files build in a few minutes. Run lake update only if you intend to move the Mathlib pin.

Repository layout

• ComputabilityEquivalence/ — the sources. Hub.lean/Equivalence.lean set up the spoke framework around Nat.Partrec; MarkovPartrec.lean holds the normal-algorithm semantics predicates and the interpreter direction; Models/Markov*.lean is the shared word-rewriting substrate plus the machine-simulation route; Models/Detlovs*.lean is the Detlovs-faithful compiler (block spec → solo discipline → leaves → relocation → composition → primitive recursion → minimization → wrapper → finals); Models/Register*.lean is the URM spoke; MarkovCorollaries.lean the classical corollaries.
• docs/ARCHITECTURE.md — the design of both routes.
• scripts/ — Python cross-checks: each nontrivial program shape (composition chains, the recursion loop, the search loop, the unary wrapper, the copy and region gadgets) is validated against a reference implementation of the rewriting semantics.

Citing this work

See CITATION.cff, or:

@software{alekseev-markov-lean,
  author = {Alekseev, Anton},
  title  = {Markov normal algorithms are exactly the partial recursive
            functions: a Lean 4 formalization with two independent proofs
            of the compilation direction},
  url    = {https://github.com/alexeyev/markov-normal-algorithms-lean}
}

A note on how this was prepared

This formalization was developed with heavy machine assistance (Anthropic's Claude). Every theorem is kernel-checked; the verification measures above — the per-declaration axiom sweep, the external kernel replay, the fuel-exact executable fixtures and the independent Python cross-checks — are what the correctness claim rests on.

License

"THE BEER-WARE LICENSE" (Revision 42) — see LICENSE. As long as you retain the notice you can do whatever you want with this stuff; if we meet some day, and you think this stuff is worth it, you can buy me a beer in return.

Mathlib, which this project depends on (and does not vendor), is licensed under Apache 2.0.