Refresh from either output of an actual look-ahead

A nearly uniform honest right state suffices for the selected refresh. The theorem keeps the complete common look-ahead history and original left state. The tampered right state may be arbitrarily correlated with the honest state; no conditioned cap for either current state is assumed. Original left and right source envelopes are averaged over the transcript.

The proof repairs the honest state inside the correlated original right state and preserves the original source marginals. Comparing the final law with its actual retained marginal charges twice the original discrepancy. Exact factorization identifies the refreshed value as right-only after the common history is observed, including on completed null rows.

This supplies a single refresh step for the advice-chain analysis of Chattopadhyay--Goyal--Li, Non-Malleable Extractors and Codes, with their Many Tampered Extensions, Algorithm 2 and Claim 6.11, printed pp.31--32: https://arxiv.org/pdf/1505.00107. The finite repair and explicit average error estimate are the deductions formalized here; adviceCorrelationBreaker_dist_le iterates the advice chain.

theorem Algebraic.Cutwidth.Extractor.lookAheadSelectedRefreshWeight_probability {Z : Type u_1} {A : Type u_2} {B : Type u_3} {X : Type u_4} {Q : Type u_5} {Seed : Type u_6} {Mid : Type u_7} {Y : Type u_8} {Out : Type u_9} [Fintype Z] [Fintype A] [Fintype B] [Fintype Q] [Fintype Mid] [Fintype Out] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x x' : Z → A → X) (q q' : Z → B → Q) (initialSeed : Q → Seed) (W : X → Seed → Mid) (QExt : Q → Mid → Seed) (y : Z → B → Y) (R : Y → Mid → Out) (second : Bool) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (lookAheadSelectedRefreshWeight w l r x x' q q' initialSeed W QExt y R second)

The selected refresh and its complete retained history have a normalized actual law.

theorem Algebraic.Cutwidth.Extractor.lookAheadSelectedRefreshWeight_eq_factored {Z : Type u_1} {A : Type u_2} {B : Type u_3} {X : Type u_4} {Q : Type u_5} {Seed : Type u_6} {Mid : Type u_7} {Y : Type u_8} {Out : Type u_9} [Fintype Z] [Fintype A] [Fintype B] [Fintype Q] [Fintype Mid] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x x' : Z → A → X) (q q' : Z → B → Q) (initialSeed : Q → Seed) (W : X → Seed → Mid) (QExt : Q → Mid → Seed) (y : Z → B → Y) (R : Y → Mid → Out) (second : Bool) (hl : ∀ (z : Z) (a : A), 0 ≤ l z a) (hr : ∀ (z : Z) (b : B), 0 ≤ r z b) : lookAheadSelectedRefreshWeight w l r x x' q q' initialSeed W QExt y R second = mapWeight (fun (p : (LookAheadBaseTranscript Z Q Mid × B) × A) => ((p.1.1, p.2), R (y p.1.1.1.1 p.1.2) (if second = true then p.1.1.2.1.2 else p.1.1.2.1.1))) (factoredWeight (lookAheadBaseWeight w l r x x' q q' initialSeed W QExt) (lookAheadBaseLeft l x x' initialSeed W QExt) (lookAheadBaseRight r q q'))

Either refresh uses a seed fixed by the same exact common transcript.

theorem Algebraic.Cutwidth.Extractor.lookAheadSelectedRefreshWeight_retainedSeed {Z : Type u_1} {A : Type u_2} {B : Type u_3} {X : Type u_4} {Q : Type u_5} {Seed : Type u_6} {Mid : Type u_7} {Y : Type u_8} {Out : Type u_9} [Fintype Z] [Fintype A] [Fintype B] [Fintype Q] [Fintype Mid] [Fintype Out] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x x' : Z → A → X) (q q' : Z → B → Q) (initialSeed : Q → Seed) (W : X → Seed → Mid) (QExt : Q → Mid → Seed) (y : Z → B → Y) (R : Y → Mid → Out) (second : Bool) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z) (b : B), 0 ≤ r z b) : mapWeight (fun (p : (LookAheadBaseTranscript Z Q Mid × A) × Out) => (p.1.1, p.2)) (lookAheadSelectedRefreshWeight w l r x x' q q' initialSeed W QExt y R second) = retainedSeedWeight (lookAheadBaseWeight w l r x x' q q' initialSeed W QExt) (lookAheadBaseRight r q q') fun (t : LookAheadBaseTranscript Z Q Mid) (b : B) => R (y t.1.1 b) (if second = true then t.2.1.2 else t.2.1.1)

Dropping the left state gives the exact refreshed seed law over the common transcript.

theorem Algebraic.Cutwidth.Extractor.WeightedStrongSeededExtractor.lookAhead_uniformRefresh_dist_le {Z : Type u_1} {A : Type u_2} {B : Type u_3} {X : Type u_4} {Q : Type u_5} {Seed : Type u_6} {Mid : Type u_7} {Y : Type u_8} {Out : Type u_9} [Fintype Z] [Fintype A] [Fintype B] [Fintype X] [Fintype Q] [Fintype Seed] [Fintype Mid] [Fintype Y] [Fintype Out] [Nonempty Seed] [Nonempty Mid] [Nonempty Out] {W : X → Seed → Mid} {QExt : Q → Mid → Seed} {R : Y → Mid → Out} {K L J : ℕ} {ε η θ ρ : ℝ} (first : WeightedStrongSeededExtractor W K ε) (first_error : 0 ≤ ε) (second : WeightedStrongSeededExtractor QExt L η) (second_error : 0 ≤ η) (refresh : WeightedStrongSeededExtractor R J θ) (refresh_error : 0 ≤ θ) (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x x' : Z → A → X) (q q' : Z → B → Q) (initialSeed : Q → Seed) (y : Z → B → Y) (μ ξ : Z → ℝ) (chooseSecond : Bool) (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 (y z) (r z) y₀ ≤ ξ z) (balanced : mapWeight initialSeed (uniformWeight Q) = uniformWeight Seed) (state : weightDist (retainedSeedWeight w r q) (uniformSecondWeight (retainedSeedWeight w r q)) ≤ ρ) : weightDist (lookAheadSelectedRefreshWeight w l r x x' q q' initialSeed W QExt y R chooseSecond) (uniformSecondWeight (lookAheadSelectedRefreshWeight w l r x x' q q' initialSeed W QExt y R chooseSecond)) ≤ θ + 2 * ε + η + 2 * ρ + ↑K * (1 + ↑(Fintype.card (Mid × Mid))) * ∑ z : Z, μ z + ↑L * ↑(Fintype.card (Seed × Seed)) / ↑(Fintype.card Q) + ↑J * ↑(Fintype.card (Q × Q)) * ↑(Fintype.card Out) * ∑ z : Z, ξ z

Either selected refresh needs only average uniformity of its actual honest state.