the main-theorem closure Smooth analytic limit dissipation

(smooth_analytic_limit_dissipation), weak well-posedness (weakWellposedInput_of_A1) and the same-drift difference energy identity feed h1_reduction_conditional with p = p₊ < 2, giving the literal main theorem inequality for H¹ data.

theorem AVenhance.Infra.Section5.RelativeError.anomalous_dissipation_of_relative (β C₀ : ℝ) (hβ : 6 / 5 ≤ β) (hA8 : Integration.IndyStepDownStatement β C₀) : ∃ (Λ₀ : ℝ), ∀ (I : Ingredients β), I.Czeta ≤ C₀ → I.Cxi ≤ C₀ → I.Chat ≤ C₀ → Λ₀ ≤ ↑I.Λ → ∀ (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ), IsStreamSeq I Φ → (∀ (j : ℕ), ClassicalSolvable (streamVel (Φ j))) → ∀ (Ctail : ℝ), 1 ≤ Ctail → ∀ (φ : ℝ → Homogenization.Vec 2 → ℝ), MeasureTheory.AEStronglyMeasurable (fun (p : ℝ × Homogenization.Vec 2) => φ p.1 p.2) (MeasureTheory.volume.restrict (Set.Icc 0 1 ×ˢ Set.univ)) → (∀ t ∈ Set.Icc 0 1, IsZ2Periodic (φ t)) → (∀ t ∈ Set.Icc 0 1, Differentiable ℝ (φ t)) → (∀ (M : ℕ), 1 ≤ M → ∀ t ∈ Set.Icc 0 1, ∀ (x : Homogenization.Vec 2), |φ t x - Φ M t x| ≤ Ctail * epsilon β I.Λ (M + 1) ^ β) → MeasureTheory.AEStronglyMeasurable (fun (p : ℝ × Homogenization.Vec 2) => streamVel φ p.1 p.2) (MeasureTheory.volume.restrict (Set.Icc 0 1 ×ˢ Set.univ)) → (∃ (B : ℝ), ∀ t ∈ Set.Icc 0 1, ∀ (x : Homogenization.Vec 2), ‖streamVel φ t x‖ ≤ B) → (∀ t ∈ Set.Icc 0 1, IsZ2Periodic (streamVel φ t)) → IsDivFree (streamVel φ) → ∃ (ϱ : ℝ → ℝ), (∀ (L : ℝ), 0 < ϱ L ∧ ϱ L ≤ 1) ∧ ∀ (f : Homogenization.Vec 2 → ℝ) (Df : Homogenization.Vec 2 → Homogenization.Vec 2), IsPeriodicH1With f Df → Homogenization.MeanZeroOn unitCube f → ∀ (θ : ℝ → ℝ → Homogenization.Vec 2 → ℝ) (Dθ : ℝ → ℝ → Homogenization.Vec 2 → Homogenization.Vec 2), (∀ (κ : ℝ), 0 < κ → IsWeakSolutionGrad (streamVel φ) κ f (θ κ) (Dθ κ)) → ϱ (datumLength f Df) ^ 2 * l2NormSq f ≤ Filter.limsup (fun (κ : ℝ) => κ * spaceTimeGradNormSq (Dθ κ)) (nhdsWithin 0 (Set.Ioi 0))

The main-theorem closure: H¹ data, via h1_reduction_conditional with p = p₊ < 2.