带舍入的高斯随机动力系统的吸收截断与平稳奇点
Absorption cutoff and stationary singularities for rounded Gaussian random dynamical systems
AI总结：
本文研究带逐坐标tanh非线性、有限精度舍入的高斯随机动力系统，将动力学简化为归一化平方半径的马尔可夫链，在不同条件下证明吸收截断、亚稳态等结果，且所有结果均在Lean 4中基于Mathlib形式化验证。
AI中文摘要：
我们研究具有逐坐标tanh非线性的高斯随机动力系统，其中有限精度通过每一步后的最近网格舍入来建模。高斯对称性将动力学简化为归一化平方半径的精确马尔可夫链。舍入使原点成为吸收态，总变差距离与吸收平衡态的距离等于吸收时间的生存概率。在固定宽度下，我们确定临界增益并证明当网格趋于零时存在高斯分布的吸收截断；在固定精度下，全局收缩产生大维度的吸收截断，而正漂移产生亚稳态。在超临界区域，我们证明存在非零不变律的大维度截断，并表明在固定维度下，其在排斥原点附近的质量具有幂律渐近。所有六个主要结果均在Lean 4中基于Mathlib形式化，并通过仅导入Mathlib的重述独立验证。
英文摘要：
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.
