This is the final Young's-inequality absorption of the mixed-term bound eq:aniso:closure:mixed:bound of lem:aniso:closure, arXiv:2609.20803, with the Cauchy–Schwarz/elliptic inputs abstracted as the real hypothesis hI.

theorem CIV.mixed_term_bound_of_cauchy_schwarz {I C C₁ W M Y : ℝ} (hC : 0 ≤ C) (hM : 0 ≤ M) (hY : 0 ≤ Y) (hI : |I| ≤ C + C₁ * W * √(M + 1) * √Y + C₁ * W * √(Y + 1) * √M) : |I| ≤ 1 / 4 * M + (C + 1 / 8 + 4 * C₁ ^ 2) * (W ^ 2 + 1) * (Y + 1)