Public statement.

theorem AVenhance.anomalous_dissipation_full (α : ℝ) (hα₀ : 0 < α) (hα₁ : α < 1 / 3) : ∃ (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2), IsHolderClass α b ∧ IsContinuousIntoHolder α b ∧ IsDivFree b ∧ ∃ (ϱ : ℝ → ℝ), (∀ (r : ℝ), 0 < ϱ r ∧ ϱ r ≤ 1) ∧ ∃ (κseq : ℕ → ℝ), (∀ (j : ℕ), 0 < κseq j) ∧ (∀ (j : ℕ), 4 * κseq (j + 1) < κseq j) ∧ Filter.Tendsto κseq Filter.atTop (nhds 0) ∧ ∃ (μ : ℝ) (ν : ℝ) (C : ℝ), 0 < μ ∧ 0 < ν ∧ ∃ (𝒟 : Set (Homogenization.Vec 2 → ℝ)), (∀ (θ₀ : Homogenization.Vec 2 → ℝ) (Dθ₀ : Homogenization.Vec 2 → Homogenization.Vec 2), IsPeriodicH1With θ₀ Dθ₀ → Homogenization.MeanZeroOn unitCube θ₀ → ∀ (θ : ℝ → ℝ → Homogenization.Vec 2 → ℝ) (Dθ : ℝ → ℝ → Homogenization.Vec 2 → Homogenization.Vec 2), (∀ (κ : ℝ), 0 < κ → IsWeakSolutionGrad b κ θ₀ (θ κ) (Dθ κ)) → Filter.limsup (fun (κ : ℝ) => κ * spaceTimeGradNormSq (Dθ κ)) (nhdsWithin 0 (Set.Ioi 0)) ≥ ϱ (√(l2NormSq θ₀) / √(gradNormSq Dθ₀)) ^ 2 * l2NormSq θ₀) ∧ (∀ (θ₀ : Homogenization.Vec 2 → ℝ) (Dθ₀ : Homogenization.Vec 2 → Homogenization.Vec 2), IsPeriodicH1With θ₀ Dθ₀ → Homogenization.MeanZeroOn unitCube θ₀ → ∀ κ ∈ ⋃ (j : ℕ), Set.Icc (κseq j / 2) (2 * κseq j), ∀ (θ : ℝ → Homogenization.Vec 2 → ℝ), IsWeakSolution b κ θ₀ θ → HolderTimeL2Le μ (C * √(l2NormSq θ₀ + gradNormSq Dθ₀)) θ) ∧ (∀ θ₀ ∈ 𝒟, ContDiff ℝ (↑⊤) θ₀ ∧ IsZ2Periodic θ₀ ∧ Homogenization.MeanZeroOn unitCube θ₀ ∧ 0 < l2NormSq θ₀) ∧ (∀ θ₀ ∈ 𝒟, ∀ (c : ℝ), c ≠ 0 → (fun (x : Homogenization.Vec 2) => c * θ₀ x) ∈ 𝒟) ∧ (∀ (N : ℕ), ∃ (n : ℕ), N ≤ n ∧ (fun (x : Homogenization.Vec 2) => Real.cos (2 * Real.pi * ↑n * x 0)) ∈ 𝒟) ∧ ∀ θ₀ ∈ 𝒟, ∀ (θ : ℝ → ℝ → Homogenization.Vec 2 → ℝ), (∀ (κ : ℝ), 0 < κ → IsWeakSolution b κ θ₀ (θ κ)) → ∃ (θ₁ : ℝ → Homogenization.Vec 2 → ℝ) (θ₂ : ℝ → Homogenization.Vec 2 → ℝ), IsTransportWeakSolution b θ₀ θ₁ ∧ IsTransportWeakSolution b θ₀ θ₂ ∧ (∀ (η : ℝ), 0 < η → ∀ᶠ (j : ℕ) in Filter.atTop, HolderTimeL2Le ν η fun (t : ℝ) (x : Homogenization.Vec 2) => θ (κseq (2 * j) / 2) t x - θ₁ t x) ∧ (∀ (η : ℝ), 0 < η → ∀ᶠ (j : ℕ) in Filter.atTop, HolderTimeL2Le ν η fun (t : ℝ) (x : Homogenization.Vec 2) => θ (2 * κseq (2 * j)) t x - θ₂ t x) ∧ ∃ t ∈ Set.Icc 0 1, l2NormSq (θ₁ t) ≠ l2NormSq (θ₂ t)

The combined main theorem. For every α ∈ (0, 1/3) there is one divergence-free, ℤ²-periodic drift b in C⁰_t C^{0,α}_x ∩ C^{0,α}_t C⁰_x on [0,1] × 𝕋² such that: (i) anomalous dissipation (Theorem 1.1 of Armstrong–Vicol) holds for every mean-zero H¹ datum, with a rate ϱ depending only on ‖θ₀‖_{L²}/‖∇θ₀‖_{L²}; (ii) uniform time regularity (Remark r.LeBron.2): for every κ ∈ 𝒦 = ⋃_j [κ_j/2, 2κ_j], where κ_j → 0 and 4κ_{j+1} < κ_j, every solution satisfies ‖θ^κ‖_{C^{0,μ}([0,1];L²)} ≤ C‖θ₀‖_{H¹}; (iii) non-uniqueness of vanishing-diffusivity limits (a corrected form of Proposition p.no.selection.principle): there is a class 𝒟 of smooth, mean-zero, nonzero data, closed under nonzero scalings and containing cos(2πn x₁) for infinitely many n, such that for every θ₀ ∈ 𝒟 the solutions along κ_{2j}/2 and along 2κ_{2j} converge in C^{0,ν}([0,1];L²) to two weak solutions of the transport equation whose L² norms differ at some time.