Alternating extraction retaining the entire opposite side

After a right-side observation, a seed computed from the left source and that observation can extract from the right source. The actual output law retains the full left state and the message, and pays for the seed discrepancy once. The source budget is an average joint envelope, with no uniform bound on individual conditional rows.

A second theorem supplies that seed using an actual affine extraction call. Revealing its seed and extracted mask makes the first output a function of the left side and transcript. The two checked extraction steps therefore compose without resampling either source or imposing seed-mask independence.

These finite estimates support the alternating-extraction transitions in Chattopadhyay--Liao, Extractors for Sum of Two Sources, Theorem 6.1, printed pp.23--25: https://arxiv.org/pdf/2110.12652. The advice correlation breaker's flip-flop rounds use these transitions; its full tampering-set induction and parameter budgets are adviceCorrelationBreaker_dist_le.

theorem Algebraic.Cutwidth.Extractor.alternatingExtractionWeight_probability {Z : Type u_1} {A : Type u_2} {B : Type u_3} {V : Type u_4} {X : Type u_5} {Seed : Type u_6} {Out : Type u_7} [Fintype Z] [Fintype A] [Fintype B] [Fintype V] [Fintype Out] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (v : Z → B → V) (s : Z × V → A → Seed) (x : Z → B → X) (E : X → Seed → Out) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (alternatingExtractionWeight w l r v s x E)

The actual alternating output is a probability law when its original factors are normalized.

theorem Algebraic.Cutwidth.Extractor.WeightedStrongSeededExtractor.alternating_joint_dist_le {Z : Type u_1} {A : Type u_2} {B : Type u_3} {V : Type u_4} {X : Type u_5} {Seed : Type u_6} {Out : Type u_7} [Fintype Z] [Fintype A] [Fintype B] [Fintype V] [Fintype X] [Fintype Seed] [Fintype Out] [Nonempty Seed] [Nonempty Out] {E : X → Seed → Out} {K : ℕ} {ε δ : ℝ} (extract : WeightedStrongSeededExtractor E K ε) (error : 0 ≤ ε) (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (v : Z → B → V) (s : Z × V → A → Seed) (x : Z → B → X) (μ : Z × V → ℝ) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) (nonnegative : ∀ (zv : Z × V), 0 ≤ μ zv) (cap : ∀ (z : Z) (v₀ : V) (x₀ : X), w z * mapWeight (fun (b : B) => (v z b, x z b)) (r z) (v₀, x₀) ≤ μ (z, v₀)) (seed : weightDist (alternatingSeedWeight w l r v s) (uniformSecondWeight (alternatingSeedWeight w l r v s)) ≤ δ) : weightDist (alternatingExtractionWeight w l r v s x E) (uniformSecondWeight (alternatingExtractionWeight w l r v s x E)) ≤ ε + δ + ↑K * ∑ zv : Z × V, μ zv

A joint message-and-source envelope bounds extraction with the entire opposite side retained.

theorem Algebraic.Cutwidth.Extractor.WeightedStrongSeededExtractor.alternating_dist_le {Z : Type u_1} {A : Type u_2} {B : Type u_3} {V : Type u_4} {X : Type u_5} {Seed : Type u_6} {Out : Type u_7} [Fintype Z] [Fintype A] [Fintype B] [Fintype V] [Fintype X] [Fintype Seed] [Fintype Out] [Nonempty Seed] [Nonempty Out] {E : X → Seed → Out} {K : ℕ} {ε δ : ℝ} (extract : WeightedStrongSeededExtractor E K ε) (error : 0 ≤ ε) (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (v : Z → B → V) (s : Z × V → A → Seed) (x : Z → B → X) (μ : Z → ℝ) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) (nonnegative : ∀ (z : Z), 0 ≤ μ z) (cap : ∀ (z : Z) (x₀ : X), w z * mapWeight (x z) (r z) x₀ ≤ μ z) (seed : weightDist (alternatingSeedWeight w l r v s) (uniformSecondWeight (alternatingSeedWeight w l r v s)) ≤ δ) : weightDist (alternatingExtractionWeight w l r v s x E) (uniformSecondWeight (alternatingExtractionWeight w l r v s x E)) ≤ ε + δ + ↑K * ↑(Fintype.card V) * ∑ z : Z, μ z

An alternating step pays only the observed message size against the original source envelope.

theorem Algebraic.Cutwidth.Extractor.affineAlternatingWeight_probability {Z : Type u_1} {A : Type u_2} {B : Type u_3} {X : Type u_4} {Seed : Type u_5} {Mid : Type u_6} {Y : Type u_7} {Out : Type u_8} [Fintype Z] [Fintype A] [Fintype B] [Fintype Seed] [Fintype Mid] [Fintype Out] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x : Z → A → X) (mask : Z → B → X) (y : Z → B → Seed) (source : Z → B → Y) (combine : X → X → X) (E : X → Seed → Mid) (F : Y → Mid → Out) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (affineAlternatingWeight w l r x mask y source combine E F)

Two actual extraction calls preserve normalization of the original joint law.

theorem Algebraic.Cutwidth.Extractor.WeightedStrongSeededExtractor.affine_alternating_dist_le {Z : Type u_1} {A : Type u_2} {B : Type u_3} {X : Type u_4} {Seed : Type u_5} {Mid : Type u_6} {Y : Type u_7} {Out : Type u_8} [Fintype Z] [Fintype A] [Fintype B] [Fintype X] [Fintype Seed] [Fintype Mid] [Fintype Y] [Fintype Out] [Nonempty Seed] [Nonempty Mid] [Nonempty Out] {E : X → Seed → Mid} {F : Y → Mid → Out} {K L : ℕ} {ε η δ : ℝ} (first : WeightedStrongSeededExtractor E K ε) (first_error : 0 ≤ ε) (second : WeightedStrongSeededExtractor F L η) (second_error : 0 ≤ η) (combine : X → X → X) (translate : Mid → Mid ≃ Mid) (linear : ∀ (a b : X) (s : Seed), E (combine a b) s = (translate (E b s)) (E a s)) (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x : Z → A → X) (mask : Z → B → X) (y : Z → B → Seed) (source : Z → B → Y) (μ ν : Z → ℝ) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) (left_nonnegative : ∀ (z : Z), 0 ≤ μ z) (right_nonnegative : ∀ (z : Z), 0 ≤ ν z) (left_cap : ∀ (z : Z) (x₀ : X), w z * mapWeight (x z) (l z) x₀ ≤ μ z) (right_cap : ∀ (z : Z) (y₀ : Y), w z * mapWeight (source z) (r z) y₀ ≤ ν z) (seed : weightDist (retainedSeedWeight w r y) (uniformSecondWeight (retainedSeedWeight w r y)) ≤ δ) : weightDist (affineAlternatingWeight w l r x mask y source combine E F) (uniformSecondWeight (affineAlternatingWeight w l r x mask y source combine E F)) ≤ η + (ε + δ + ↑K * ∑ z : Z, μ z) + ↑L * ↑(Fintype.card (Seed × Mid)) * ∑ z : Z, ν z

An affine extraction seeds the next right extraction while retaining the whole left state.