Conley index theory for asymptotically autonomous systems and UV-to-IR connections
Alireza Behtash, Syo Kamata, Mauricio M. Martinez
math-ph
Nov 5, 2026 · v1
hep-th math.DS
TL;DR
The paper's results on Conley index theory for asymptotically autonomous systems were formalized in Lean 4 with AI assistance; the formalization compiles without unproved steps and is publicly released.
Abstract
Many non-equilibrium systems, such as expanding plasmas, evolve by equations that depend explicitly on time and interpolate between autonomous early-time (UV) and late-time (IR) limits. After time is compactified, fixed points lie on invariant boundary fibers, where the Conley index is one-sided and blind to the UV. For time dependence that admits a $C^1$ compactification, we reflect the extended phase space across these fibers. Both sheets of the double run from the UV to the IR, and the UV index reappears, suspended by one degree. Extending one sheet slightly beyond both fibers gives an explicit UV-to-IR transport map between the Conley indices of the limit systems, and its non-vanishing forces connecting solutions. If one block with a fixed strict entrance/exit decomposition serves every frozen system, this map is an isomorphism at every admissible rate. If the block also has nonzero relative homology, the isolated invariant sets of the two limits are connected at every rate. In the Gubser flow of Israel-Stewart theory, the separatrix between two classes of initial data is a transversal connection at every finite relaxation scale $c$, with splitting $Δ(c)\propto1/c$. In the Bjorken flow at the lowest moment truncation, we prove existence and uniqueness of the attractor solution without regularization. For the three-dimensional Gubser system we construct the global Morse decomposition. In the one-loop flow of the $(4+ε)$-dimensional $O(N)$ model with cubic anisotropy, a shift of $N$ through $N=4$ has vanishing transport map, but a driven connection and a nonzero connecting homomorphism detect it at every rate.
Problem
Non-autonomous systems that interpolate between autonomous UV (early-time) and IR (late-time) limits have all their fixed points on boundary fibers once time is compactified. There the Conley index is one-sided and does not see the UV, so a different construction is needed to relate the UV and IR dynamics.
Approach
For time dependence admitting a C^1 compactification, the extended phase space is reflected across the boundary fibers to form a double. In the double the UV index reappears, suspended by one degree. Extending one sheet beyond both fibers yields an explicit UV-to-IR transport map between the Conley indices of the limit systems. The theory is applied to Gubser flow in Israel–Stewart theory, to Bjorken flow, and to the one-loop (4+ε)-dimensional O(N) model with cubic anisotropy. The results were formalized in Lean 4 with an AI-assisted workflow and partial human input.
Results
A non-vanishing transport map forces connecting solutions, and it is an isomorphism at every admissible rate when a single isolating block serves all frozen systems. The applications give a transversal separatrix in Gubser flow with splitting proportional to 1/c, existence and uniqueness of the Bjorken attractor without regularization, and a global Morse decomposition for the 3D Gubser system. In the O(N) model, a shift of N through 4 has vanishing transport map but is detected by connection data. The Lean formalization uses only standard axioms.
