Finite seeded steps retaining all earlier randomness

One fresh independent uniform seed can be appended to an existing joint source without increasing its statistical approximation error. Product seed averaging identifies the resulting conditional laws, and successive seeded programs agree exactly with their deterministic composition.

The distance and composition identities apply to arbitrary real weights and empty seed types. Probability preservation requires only that the new seed type be nonempty. These are finite transport identities supporting the retained-seed induction of Chattopadhyay--Goodman--Liao, Theorem 5.6: https://eccc.weizmann.ac.il/report/2021/075/download/. They make no claim about computing arbitrary real weights or ideal conditional witnesses.

theorem Algebraic.Cutwidth.Extractor.seedFamilyWeight_product {Earlier : Type u_1} {Fresh : Type u_2} {Ω : Type u_3} [Fintype Earlier] [Fintype Fresh] [Fintype Ω] (p : Earlier → Fresh → Ω → ℝ) : mapWeight (⇑(Equiv.prodAssoc Earlier Fresh Ω).symm) (seedFamilyWeight fun (s : Earlier) => seedFamilyWeight (p s)) = seedFamilyWeight fun (sy : Earlier × Fresh) => p sy.1 sy.2

Successive uniform seed families agree with the uniform product-seed family.

theorem Algebraic.Cutwidth.Extractor.retainedSeedStep_seedFamilyWeight {Earlier : Type u_1} {Fresh : Type u_2} {X : Type u_3} {Ω : Type u_4} [Fintype Earlier] [Fintype Fresh] [Fintype X] [Fintype Ω] (F : Earlier → X → Fresh → Ω) (p : Earlier → X → ℝ) : retainedSeedStep F (seedFamilyWeight p) = seedFamilyWeight fun (sy : Earlier × Fresh) => mapWeight (fun (x : X) => F sy.1 x sy.2) (p sy.1)

A fresh seeded step has the expected conditional law at each retained seed pair.

theorem Algebraic.Cutwidth.Extractor.weightDist_seedFamilyWeight_product {Earlier : Type u_1} {Fresh : Type u_2} {Ω : Type u_3} [Fintype Earlier] [Fintype Fresh] [Fintype Ω] (p q : Earlier → Fresh → Ω → ℝ) : weightDist (seedFamilyWeight fun (sy : Earlier × Fresh) => p sy.1 sy.2) (seedFamilyWeight fun (sy : Earlier × Fresh) => q sy.1 sy.2) = (∑ s : Earlier, weightDist (seedFamilyWeight (p s)) (seedFamilyWeight (q s))) / ↑(Fintype.card Earlier)

Product-seed distance averages the joint fresh-seed distances over earlier seeds.

theorem Algebraic.Cutwidth.Extractor.weightedSeededOutput_dist_le {X : Type u_1} {Fresh : Type u_2} {Ω : Type u_3} [Fintype X] [Fintype Fresh] [Fintype Ω] (p q : X → ℝ) (F : X → Fresh → Ω) : weightDist (weightedSeededOutput p F) (weightedSeededOutput q F) ≤ weightDist p q

Adding an independent uniform seed and applying a deterministic map contracts distance.

theorem Algebraic.Cutwidth.Extractor.retainedSeedStep_dist_le {Earlier : Type u_1} {Fresh : Type u_2} {X : Type u_3} {Ω : Type u_4} [Fintype Earlier] [Fintype Fresh] [Fintype X] [Fintype Ω] (F : Earlier → X → Fresh → Ω) (p q : Earlier × X → ℝ) : weightDist (retainedSeedStep F p) (retainedSeedStep F q) ≤ weightDist p q

Keeping both seeds preserves the bound on a previous joint approximation error.

theorem Algebraic.Cutwidth.Extractor.IsProbabilityWeight.retainedSeedStep {Earlier : Type u_1} {Fresh : Type u_2} {X : Type u_3} {Ω : Type u_4} [Fintype Earlier] [Fintype Fresh] [Fintype X] [Fintype Ω] [Nonempty Fresh] {p : Earlier × X → ℝ} (probability : IsProbabilityWeight p) (F : Earlier → X → Fresh → Ω) : IsProbabilityWeight (Extractor.retainedSeedStep F p)

A probability source stays normalized after adding a nonempty fresh uniform seed.

theorem Algebraic.Cutwidth.Extractor.retainedSeedStep_weightedSeededOutput {A : Type u_1} {Earlier : Type u_2} {Fresh : Type u_3} {X : Type u_4} {Ω : Type u_5} [Fintype A] [Fintype Earlier] [Fintype Fresh] [Fintype X] [Fintype Ω] (F : Earlier → X → Fresh → Ω) (p : A → ℝ) (E : A → Earlier → X) : retainedSeedStep F (weightedSeededOutput p E) = weightedSeededOutput p fun (a : A) (sy : Earlier × Fresh) => F sy.1 (E a sy.1) sy.2

Successive seeded maps equal their deterministic composition with both seeds retained.