exists_closure_gronwall_bound_of_exists_energy_inequality composes the substitution step deriv_le_of_closure_energy of eq:aniso:closure:energy with the Grönwall step closure_gronwall_bound of lem:aniso:closure: from the energy inequality in the form ∃ Cstar ≥ 1, … (as produced by CIV.energy_inequality_of_mixed_term_bound) together with the G, W decay data, it gives the enstrophy decay Y + 1 ≤ C' (−t)^{−C_*η}. eta_sixteenth_valid records that the manuscript's choice η = 1/(16 C_*) satisfies the Grönwall step's smallness hypothesis 0 < η ∧ 2η < 1, and exists_closure_gronwall_bound_sixteenth_eta shows that this choice collapses the decay exponent C_* η to the universal constant 1/16, independent of C_* — the fact behind the remark of eq:aniso:closure:energy that 2 C_* η = 1/8 < 1.

theorem CIV.exists_closure_gronwall_bound_of_exists_energy_inequality {Y M G W : ℝ → ℝ} {tη η Cη : ℝ} (htη : tη < 0) (hη : 0 < η ∧ 2 * η < 1) (hCη : 0 ≤ Cη) (hM : ∀ t ∈ Set.Ioo tη 0, 0 ≤ M t) (hY : ∀ t ∈ Set.Ioo tη 0, 0 ≤ Y t) (hG : ∀ t ∈ Set.Ioo tη 0, G t ≤ η / -t) (hW0 : ∀ t ∈ Set.Ioo tη 0, 0 ≤ W t) (hW : ∀ t ∈ Set.Ioo tη 0, W t ≤ Cη * (-t) ^ (-η)) (hcont : ∀ t ∈ Set.Ico tη 0, ContinuousOn Y (Set.Icc tη t)) (hderiv : ∀ t ∈ Set.Ioo tη 0, HasDerivWithinAt Y (deriv Y t) (Set.Ici t) t) (hY0 : 0 ≤ Y tη) (hex : ∃ (Cstar : ℝ), 1 ≤ Cstar ∧ ∀ t ∈ Set.Ioo tη 0, deriv Y t + M t ≤ Cstar * (G t + W t ^ 2 + 1) * (Y t + 1)) : ∃ (Cstar : ℝ), 1 ≤ Cstar ∧ ∃ (C' : ℝ), 0 ≤ C' ∧ ∀ t ∈ Set.Ioo tη 0, Y t + 1 ≤ C' * (-t) ^ (-(Cstar * η))

theorem CIV.eta_sixteenth_valid {Cstar : ℝ} (hCstar : 1 ≤ Cstar) : 0 < 1 / (16 * Cstar) ∧ 2 * (1 / (16 * Cstar)) < 1

theorem CIV.exists_closure_gronwall_bound_sixteenth_eta {Y M G W : ℝ → ℝ} {tη Cη : ℝ} (htη : tη < 0) (hCη : 0 ≤ Cη) (hM : ∀ t ∈ Set.Ioo tη 0, 0 ≤ M t) (hY : ∀ t ∈ Set.Ioo tη 0, 0 ≤ Y t) (hW0 : ∀ t ∈ Set.Ioo tη 0, 0 ≤ W t) (hcont : ∀ t ∈ Set.Ico tη 0, ContinuousOn Y (Set.Icc tη t)) (hderiv : ∀ t ∈ Set.Ioo tη 0, HasDerivWithinAt Y (deriv Y t) (Set.Ici t) t) (hY0 : 0 ≤ Y tη) (hex : ∃ (Cstar : ℝ), 1 ≤ Cstar ∧ (∀ t ∈ Set.Ioo tη 0, deriv Y t + M t ≤ Cstar * (G t + W t ^ 2 + 1) * (Y t + 1)) ∧ (∀ t ∈ Set.Ioo tη 0, G t ≤ 1 / (16 * Cstar) / -t) ∧ ∀ t ∈ Set.Ioo tη 0, W t ≤ Cη * (-t) ^ (-(1 / (16 * Cstar)))) : ∃ (C' : ℝ), 0 ≤ C' ∧ ∀ t ∈ Set.Ioo tη 0, Y t + 1 ≤ C' * (-t) ^ (-(1 / 16))