Monodromy Computation Model
Xiaoyang Liu
cs.CC
Nov 3, 2026 · v1
cs.LO
TL;DR
Formalizes the Monodromy calculus, its Turing simulation, the partial-recursive characterization, and the sublanguage separation in Lean 4 with Mathlib, building on Mathlib's covering-map monodromy and Turing machine library.
Abstract
A closed path can return to its starting point while analytic continuation reaches another branch. We construct a finite computational calculus in which retained logarithmic branches supply memory, analytic observations select operations, and descent through a covering exposes deeper memory. Three branch coordinates suffice, and every finite observation uses the same cubic power covering. Each program defines a globally real analytic return map whose integer-lattice execution is realized by actual path lifting. Our first theorem simulates every finite-alphabet, finite-control Post–Turing machine, preserving complete configurations, halting, and divergence. Our second theorem identifies the partial numeric functions of the calculus, under fixed primitive-recursive input and output maps, with exactly the partial recursive functions. Deleting descent leaves a Forward language with a syntax-derived finite observation quotient and a primitive-recursive halting predicate. This yields a strict separation within the calculus and identifies access to deeper memory as its decisive additional operation. The constructions and semantic correspondences are formalized in Lean 4 with Mathlib.
Problem
The question is whether analytic continuation and covering-space monodromy can support memory, conditional execution, and universal computation within a finite effective calculus.
Approach
Logarithmic branches retain integer memory in three coordinates, and a cubic power covering supplies analytic selectors that observe residues. Descent through the covering exposes deeper digits of memory. Programs define globally real analytic return maps, and path lifting realizes their execution on the integer lattice. Everything is formalized in Lean 4 with Mathlib, using IsCoveringMap.monodromy for transport and Mathlib's TM0 and partial-recursive-to-Turing translations.
Results
The calculus simulates every finite Post–Turing machine, preserving configurations, halting, and divergence. Its partial numeric functions are exactly the partial recursive functions. The descent-free Forward sublanguage has primitive-recursive halting, which gives a strict separation. The Lean development is audited to depend only on the standard axioms.
