Tuple identities for shared-seed block condensation

Head/tail transport and the empty tuple case connect the block-source induction to the finite weighted-output contract. These identities retain the seed once and require no independence between source blocks.

theorem Algebraic.Cutwidth.Extractor.Internal.blockCondenser_mapWeight_cons {α : Type u_1} [Fintype α] {t : ℕ} (w : α → ℝ) (p : α → (Fin t → α) → ℝ) : (mapWeight (fun (az : α × (Fin t → α)) => Fin.cons az.1 az.2) fun (az : α × (Fin t → α)) => w az.1 * p az.1 az.2) = fun (x : Fin (t + 1) → α) => w (x 0) * p (x 0) (Fin.tail x)

theorem Algebraic.Cutwidth.Extractor.Internal.blockCondenser_cons_map {α : Type u_1} {β : Type u_2} {t : ℕ} (f : α → β) (a : α) (z : Fin t → α) : (fun (i : Fin (t + 1)) => f (Fin.cons a z i)) = Fin.cons (f a) fun (i : Fin t) => f (z i)

theorem Algebraic.Cutwidth.Extractor.Internal.blockCondenser_zero {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype α] [Fintype Seed] [Fintype Ω] (C : α → Seed → Ω) (p : (Fin 0 → α) → ℝ) (hp : IsProbabilityWeight p) (K : ℕ) : ∃ (q : Seed → (Fin 0 → Ω) → ℝ), (∀ (y : Seed), IsBlockSource (q y) K) ∧ (weightedSeededOutput p fun (x : Fin 0 → α) (y : Seed) (i : Fin 0) => C (x i) y) = seedFamilyWeight q