Winding Metastability: a verified research program on metastability of reversible diffusions on the torus

Abstract

Winding Metastability — documentary release (math-v2.0.2) A documentary release: zero mathematical change. Apart from README.md, CITATION.cff and one appended entry in the operational log (COORDINATION.md entry [123], the record of the math-v2.0.1 release itself), every file of math-v2.0.1 is byte-identical here. One file is added. It brings two things. The T2 rate-scope erratum, formal-framework/pre-physics/lane-c-exit-time-lower-bound-rate-scope-erratum-v1.md. It fixes how the T2 lane (lane-c-exit-time-lower-bound-v1.md, unchanged, blob aeb5a6ce) is read. The T2 bound on the zero-sector exit time, liminf_{beta -> infinity} beta^-1 log E_q[tau_exit(Sigma_0)] >= 2 kappa - J(q), is a one-sided lower bound, never an exact rate. 2 kappa is an interface floor, not a proved crossing height. Leaving the energy domain is not the same event as changing sector. The source condition is the Freidlin-Wentzell Chapter 6 Condition (A) setting, with the internal attractor input P0. The T2 statement, its proof and every other result are unchanged. The erratum's status block records the state on 2026-09-21, when no release was yet authorized. Relation to prior work (the same section is in README.md). For a single ring, the winding sectors and their energy barrier, the classification of equilibria and saddles, and the transition law are already in the published literature, and this repository claims no priority for them. Cosco and Shapira [1] define the same discrete winding number on the periodic XY chain, identify the energy barrier to changing it (2J with their coupling constant J; 2 kappa here), and prove the time scale on which the winding changes as the number of rotors N grows, with its log N correction. Berglund, Medvedev and Simpson [2] study the stochastic nearest-neighbour Kuramoto model, which is this program's single-ring diffusion after the change of variables theta = 2 pi u, kappa = K/(2 pi), a linear time change and eps = 1/beta. They find all equilibria and classify them by Morse index, identify the stable twisted states and the relevant one-jump saddles, split off the global phase as a Brownian motion, and prove the metastable hierarchy and sharp Eyring-Kramers estimates, with prefactor, for the transition times. Their barrier height equals this program's single-ring label exponent S_k - m_k (an identity recomputed by machine). Their estimate is sharper than the program's logarithmic label law; it is stated for reaching the lower twisted states rather than for the first change of winding. So this program claims no new classification, no new saddle exponent, no new phase-mode decoupling and no sharper transition law for a single ring. What it adds is the verification record (Part I machine-checked in Lean; the signed external AI audits and the census under formal-framework/governance/cross-provider/) and the extension to two coupled rings and to maintenance that acts only through the energy readout (lanes M2, M3, MC, MR, WC, LT and LP). A preliminary search found no exact match for that extension; that is not a novelty test, and no novelty is claimed for it. [1] C. Cosco and A. Shapira, Topologically induced metastability in a periodic XY chain, J. Math. Phys. 62, 043301 (2021), doi:10.1063/5.0004606, arXiv:2001.07950. [2] N. Berglund, G. S. Medvedev and G. Simpson, Metastability in the stochastic nearest-neighbour Kuramoto model of coupled phase oscillators, Nonlinearity 38, 095031 (2025), doi:10.1088/1361-6544/ae05aa, arXiv:2412.15136. How each piece was checked. The erratum changes no statement and adds no calculation. Two independent read-only AI reviews read it before it was merged into the working repository; the record does not name their provider. That is not a signed cross-provider verdict, so the census is unchanged (56 physical artifacts, 55 authoritative signatures, 1 superseded). The prose invariant guard passes. The two references were checked against their published records (Crossref, arXiv and the papers' own text). The equality between their barrier height and S_k - m_k was recomputed by machine for N = 5..40 and every k in their saddle range (largest difference 6e-15). The release text (the prior-work section, the README changes and these notes) was read by an independent same-provider AI context (Anthropic). It found no real error, and its wording points are applied. That is not cross-provider verification. README.md also corrects one count: the census selftest has nine fixtures since math-v2.0.1. Verify it yourself: python scripts/verdict_census_selftest.py python scripts/verdict_census.py python scripts/prose_invariants.py What remains open is unchanged; see formal-framework/governance/math-v2.0-tag-annotation.md and formal-framework/governance/math-v2.0.1-tag-annotation.md.