Absorption cutoff and stationary singularities for rounded Gaussian random dynamical systems

Abstract

We study Gaussian random dynamical systems with coordinatewise $\tanh$ nonlinearity, where finite precision is modeled by nearest-grid rounding after each step. Gaussian symmetry reduces the dynamics to an exact Markov chain for the normalized squared radius. Rounding makes the origin absorbing, and the total variation distance to the absorbing equilibrium equals the survival probability of the absorption time. At fixed width, we identify the critical gain and prove an absorption cutoff with Gaussian profile as the mesh tends to zero. At fixed precision, global contraction yields a large-dimension absorption cutoff, while positive drift produces metastability. In the supercritical regime, we prove a large-dimension cutoff to a nonzero invariant law and show that, at fixed dimension, its mass near the repelling origin has a power-law asymptotic. All six main results are formalized in Lean 4 on top of Mathlib and independently checked against restatements that import only Mathlib.

Disclosure

“Nash–Moser theory by Armstrong and Kempe [AK26a], and of coarse-graining theory for elliptic equations by Armstrong and Kuusi [AK26b]. The development was produced by autoformalization. Under the author’s supervision, OpenAI’s ChatGPT and Anthropic’s Claude generated the proofs from the arguments of this paper. The Lean kernel checks every definition, statement, and proof in the production library against Mathlib. 1.6. Proof overview and organization. To prove Theorem 1.4, we couple Y pN q t”

PDF page 9

Classification

Drafting a complete proof for author revision

Multiplier

9

Verified

2026-08-23T05:18:31.456759Z

Structural counts