Lower Bounds for Advection-Diffusion Equations: An Exploration with AI-Generated Proofs

Technical Summary: Lower Bounds for Advection-Diffusion Equations: An Exploration with AI-Generated Proofs

Problem Statement
The paper investigates the long-time behavior of solutions to the advection-diffusion equation on the torus $\mathbb{T}^d$:
$$\partial_t \rho + u \cdot \nabla \rho = \mu \Delta \rho$$
Specifically, the authors focus on establishing explicit lower bounds for the decay of the $L^2$ norm and the mixing scale (defined as the ratio $\|\rho\|_{\dot{H}^{-1}} / \|\rho\|_{L^2}$). While it is known that without structural constraints on the velocity field $u$, the $L^2$ norm can decay at a double-exponential rate, the paper seeks to identify structural conditions (shear flows, time-periodic oscillations) that restore exponential lower bounds. A central goal is to provide constructive, explicit constants in these bounds, depending on the data ($\rho_0$, $u$, $\nu$), rather than relying on non-constructive existence arguments.

Methodology
The primary methodological novelty of this work is the complete reliance on an AI system for the generation of rigorous mathematical proofs.

• AI System: The proofs were generated by QED, a multi-agent math proving system. The workflow involves a sequential loop: a survey agent gathers background, a plan agent sketches strategies, a prover agent generates proofs, a verifier agent checks logical consistency and soundness, and a regulator agent decides on revisions.
• Human Role: The human authors (An and Xu) formulated the initial mathematical questions but provided no expert intervention during the proof generation process. They did not offer PDE-specific guidance, hints, or intermediate corrections. Their role was limited to reviewing the AI-verified output for correctness and performing minimal editorial adjustments to assemble the manuscript.
• Mathematical Techniques: Despite the AI generation, the proofs employ standard analytical techniques adapted for explicit estimates, including:
  • Fourier mode decomposition and exact phase evolution tracking.
  • High-low frequency decompositions in the transverse direction.
  • Resolvent estimates and finite-dimensional adjoint bundle constructions.
  • Fast-phase parabolic averaging arguments for time-periodic flows.
  • Application of Keldysh's theorem and Floquet theory for spectral analysis.

Key Contributions and Results
The paper establishes explicit lower bounds in three distinct settings:

1. Inviscid Shear Mixing ($\mu=0$):

   • Setting: Pure transport equation with a shear flow $u(y,t) \in L^\infty_t W^{1,1}_y$.
   • Result: Theorem 1.1 proves a polynomial lower bound for the homogeneous negative Sobolev norm:
     $$\|\theta(t)\|_{\dot{H}^{-1}} \ge \frac{c_*}{1+t^2}$$
   • Significance: This extends previous results (which often required higher regularity like $C^\alpha$ or Besov spaces, or provided bounds only along subsequences) to the weaker $W^{1,1}$ class and holds for all times $t \ge 0$. The proof relies on the exact evolution of $x$-Fourier modes and the linear growth of the phase function's $W^{1,1}$ norm.

2. Diffusive Shears ($\mu > 0$):

   • Setting: Advection-diffusion with a bounded shear $U(t,y) \in L^\infty_{t,y}$ and small diffusivity $\nu$.
   • Results:
     • Theorem 1.2 (Explicit $L^2$ Bound): Establishes an explicit exponential lower bound $\|\rho(t)\|_{L^2} \ge \|\rho_0\|_{L^2} e^{-c_2 t}$, where $c_2$ is explicitly computable from the data and scales as $O(\nu^{-1})$.
     • Mixing Scale: Proves a uniform positive lower bound on the mixing scale $\|\rho\|_{\dot{H}^{-1}} / \|\rho\|_{L^2} \ge c^*$. This rigorously justifies the "arrested cascade" phenomenon observed numerically, showing that diffusion prevents the mixing scale from vanishing.
   • Sharpness: The paper constructs specific initial data (high-frequency heat eigenfunctions) to show that the $\nu^{-1}$ scaling of the decay exponent is sharp.

3. Fast Time-Periodic Oscillations:

   • Setting: General divergence-free velocity fields $u(At, x, y)$ with frequency $A$ and period $L$.
   • Result: Theorem 1.3 proves that for sufficiently large frequencies $A > A_0$, the solution satisfies an exponential $L^2$ lower bound $\|\rho(t)\|_{L^2} \ge C e^{-c_A t}$.
   • Method: The proof constructs a finite-dimensional adjoint observable from the generalized root spaces of the time-averaged operator. It uses a fast-phase averaging argument to show that the "detecting bundle" persists despite the oscillation, preventing superexponential decay.
   • Corollary: This result implies that for time-independent flows (viewed as a limit or specific case), an exponential lower bound holds, filling a gap in the literature regarding explicit constants for such flows.

Significance and Claims
The paper positions itself primarily as a stress test for AI capabilities in mathematical research.

• AI Capability: The authors claim that the successful generation of these proofs, without any PDE-specific tuning or human intervention during the reasoning process, demonstrates that current AI systems can produce rigorous, constructive mathematics in complex analysis settings.
• Explicitness: The work emphasizes that all constants ($c_*, c_2, A_0$, etc.) are explicit and constructive, depending only on the input data. This contrasts with many existing non-constructive results in mixing theory.
• Verification: The paper highlights that the AI's verifier exhibited a "zero false-positive rate" on this problem set; the 14 proofs accepted by the AI were independently confirmed as correct by the human authors.
• Modesty: The authors do not claim that AI has replaced human mathematicians. Instead, they frame this as a demonstration of a new workflow where humans define the problem and verify the final output, while AI handles the heavy lifting of the proof construction. The paper notes that the proofs generated by the AI were sometimes "tedious" or less clear than human-written versions, suggesting that human editorial oversight remains necessary for readability.

In summary, the paper provides rigorous, explicit lower bounds for advection-diffusion equations in three regimes, serving as a benchmark for the reliability and capability of multi-agent AI systems in generating formal mathematical proofs.