The pair estimate: θ(κ_j) and θ(κ_{j'}) are close in sup-L²

Five-term splitting: tail (tail_sup), one step of the step-down estimate, the middle term (two diffusivities, flip-flop parity), the telescoped step-down steps of the longer chain, tail.

theorem AVenhance.Infra.FullTheorem.pair_bound (β C₀ : ℝ) : ∃ (Λc : ℝ) (ρ : ℝ), 0 < ρ ∧ ∀ (I : Ingredients β), I.Czeta ≤ C₀ → I.Cxi ≤ C₀ → I.Chat ≤ C₀ → Λc ≤ ↑I.Λ → ∀ (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ), IsStreamSeq I Φ → ∀ (φ : ℝ → Homogenization.Vec 2 → ℝ), (∀ (t : ℝ) (x : Homogenization.Vec 2), Filter.Tendsto (fun (M : ℕ) => Φ M t x) Filter.atTop (nhds (φ t x))) → ∃ (K : ℝ), 0 ≤ K ∧ ∀ (t : ℝ), t = 1 / 2 ∨ t = 2 → ∀ (R : ℝ), 0 < R → ∀ (θ₀ : Homogenization.Vec 2 → ℝ), ContDiff ℝ (↑⊤) θ₀ → IsZ2Periodic θ₀ → Homogenization.MeanZeroOn unitCube θ₀ → IsThetaAnalytic R θ₀ → ∀ (θ : ℝ → ℝ → Homogenization.Vec 2 → ℝ), (∀ (j : ℕ), IsWeakSolution (streamVel φ) (kfam β I.Λ t j) θ₀ (θ (kfam β I.Λ t j))) → ∀ (j : ℕ), 1 ≤ j → mTheta0 β I.Λ R ≤ 2 * j + 1 → K * epsilon β I.Λ (2 * j) ^ ρ ≤ 2 → ∀ (j' : ℕ), j ≤ j' → ∀ s ∈ Set.Icc 0 1, √(l2NormSq fun (x : Homogenization.Vec 2) => θ (kfam β I.Λ t j) s x - θ (kfam β I.Λ t j') s x) ≤ K * (epsilon β I.Λ (2 * j) ^ tailExp β + epsilon β I.Λ (2 * j) ^ delta β + epsilon β I.Λ (2 * j) ^ ρ) * √(l2NormSq θ₀)