Prepending a two-block source to its conditional tails

Disintegrating the two-coordinate head gives a capped first coordinate and a capped second coordinate for every first value. Two applications of the one-coordinate prepend theorem then retain all tail caps. Zero-mass rows are already handled by the existing disintegration theorem.

theorem Algebraic.Cutwidth.Extractor.Internal.isBlockSource_pairPrepend {α : Type u_1} [Fintype α] {t K : ℕ} (head : α × α → ℝ) (tail : α × α → (Fin t → α) → ℝ) (head_source : IsBlockSource (fun (x : Fin 2 → α) => head (x 0, x 1)) K) (tail_source : ∀ (ab : α × α), IsBlockSource (tail ab) K) : IsBlockSource (fun (x : Fin (t + 2) → α) => head (x 0, x 1) * tail (x 0, x 1) (Fin.tail (Fin.tail x))) K