Pair weights as two-block sources

Reindexing a pair by its two coordinates preserves normalization. Its one-coordinate prefix mass is the first marginal, so the two prefix caps are exactly the unconditional first cap and the conditional second cap.

theorem Algebraic.Cutwidth.Extractor.Internal.blockSource_two_probability_iff {α : Type u_1} [Fintype α] (p : α × α → ℝ) : (IsProbabilityWeight fun (x : Fin 2 → α) => p (x 0, x 1)) ↔ IsProbabilityWeight p

theorem Algebraic.Cutwidth.Extractor.Internal.blockPrefixWeight_two_one {α : Type u_1} [Fintype α] (p : α × α → ℝ) (u : Fin 1 → α) : blockPrefixWeight (fun (x : Fin 2 → α) => p (x 0, x 1)) blockPrefixWeight_two_one._proof_1 u = firstWeight p (u 0)

theorem Algebraic.Cutwidth.Extractor.Internal.blockSource_two_iff {α : Type u_1} [Fintype α] (p : α × α → ℝ) (K : ℕ) : IsBlockSource (fun (x : Fin 2 → α) => p (x 0, x 1)) K ↔ IsProbabilityWeight p ∧ CappedWeight (firstWeight p) K ∧ ∀ (a b : α), ↑K * p (a, b) ≤ firstWeight p a