A second-output refresh with an arbitrary left-only tampered seed

The honest refresh rereads the original right source, seeded by the actual second look-ahead output. The tampered refresh uses an arbitrary seed computed from the left state. The final guarantee retains that seed, the original right input to the look-ahead, both honest look-ahead outputs, the tampered refresh, and the full original left state. Only original joint source envelopes and the original prefix-seed discrepancy are assumed.

Revealing a normalized left-only message preserves the average original seed discrepancy exactly. It multiplies the original left envelope total by the message alphabet size and leaves the right envelope totals unchanged. Null observations require no conditional-positivity assumption.

This finite composition supports the already-distinct-advice analysis of Chattopadhyay--Goyal--Li, Non-Malleable Extractors and Codes, with their Many Tampered Extensions, Algorithm 1, Lemma 6.5 and Claim 6.6, printed pp.25--29: https://arxiv.org/abs/1505.00107. It uses the finite two-sided leakage estimate underlying Chattopadhyay--Liao (2021), Lemma 3.26: https://arxiv.org/abs/2110.12652. The complete advice-chain invariant is proved in Advice.Extraction (adviceCorrelationBreaker_dist_le).

theorem Algebraic.Cutwidth.Extractor.retainedSeedWeight_observe_left_dist {Z : Type u_1} {A : Type u_2} {B : Type u_3} {U : Type u_4} {Seed : Type u_5} [Fintype Z] [Fintype A] [Fintype B] [Fintype U] [Fintype Seed] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (f : Z → A → U) (s : Z → B → Seed) (hw : ∀ (z : Z), 0 ≤ w z) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : weightDist (retainedSeedWeight (observedTranscriptWeight w l f) (fun (zu : Z × U) => r zu.1) fun (zu : Z × U) => s zu.1) (uniformSecondWeight (retainedSeedWeight (observedTranscriptWeight w l f) (fun (zu : Z × U) => r zu.1) fun (zu : Z × U) => s zu.1)) = weightDist (retainedSeedWeight w r s) (uniformSecondWeight (retainedSeedWeight w r s))

A normalized left-only observation preserves the average original right-seed discrepancy.

theorem Algebraic.Cutwidth.Extractor.fixedTamperingSecondRefreshWeight_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 Mid] [Fintype Q] [Fintype Out] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x : Z → A → X) (q : Z → B → Q) (y y' : Z → B → Y) (leak : Z → A → Mid) (initialSeed : Q → Seed) (W : X → Seed → Mid) (QExt : Q → Mid → Seed) (R : Y → Mid → Out) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (fixedTamperingSecondRefreshWeight w l r x q y y' leak initialSeed W QExt R)

The second-output refresh is the probability law of the actual retained variables.

theorem Algebraic.Cutwidth.Extractor.WeightedStrongSeededExtractor.fixedTampering_second_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 : Z → A → X) (q : Z → B → Q) (y y' : Z → B → Y) (leak : Z → A → Mid) (initialSeed : Q → Seed) (μ ν ξ : 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) (refresh_nonnegative : ∀ (z : Z), 0 ≤ ξ z) (left_cap : ∀ (z : Z) (x₀ : X), w z * mapWeight (x z) (l z) x₀ ≤ μ z) (right_cap : ∀ (z : Z) (q₀ : Q), w z * mapWeight (q z) (r z) q₀ ≤ ν z) (refresh_cap : ∀ (z : Z) (y₀ : Y), w z * mapWeight (y z) (r z) y₀ ≤ ξ z) (seed : weightDist (retainedSeedWeight w r fun (z : Z) (b : B) => initialSeed (q z b)) (uniformSecondWeight (retainedSeedWeight w r fun (z : Z) (b : B) => initialSeed (q z b))) ≤ δ) : weightDist (fixedTamperingSecondRefreshWeight w l r x q y y' leak initialSeed W QExt R) (uniformSecondWeight (fixedTamperingSecondRefreshWeight w l r x q y y' leak initialSeed W QExt R)) ≤ θ + 2 * ε + η + δ + ↑K * ↑(Fintype.card Mid) * (1 + ↑(Fintype.card (Mid × Mid))) * ∑ z : Z, μ z + ↑L * ↑(Fintype.card (Seed × Seed)) * ∑ z : Z, ν z + ↑J * ↑(Fintype.card Q) * ↑(Fintype.card Out) * ∑ z : Z, ξ z

The actual two-round second output seeds a refresh against arbitrary left-only tampering.