Actual first refreshes in the opposite-advice flip-flop argument #
The common transcript records the right input pair and all four first look-ahead outputs. Each refresh reads the original right source. The first-output refresh retains this transcript and the full left state. The second-output refresh additionally retains the tampered refresh seeded by the tampered first output.
The seed errors are derived from the original first extraction or the actual two-round look-ahead theorem. The only seed-discrepancy hypothesis concerns the original prefix. Source hypotheses are joint envelopes, not bounds on every conditional row. The four left outputs are appended after extraction using the retained left state, so no seed is assumed uniform after revealing itself. Exact observation laws and envelope totals support subsequent repair and extraction steps.
These are finite first-phase steps in Chattopadhyay--Goyal--Li, Non-Malleable Extractors and Codes, with their Many Tampered Extensions (2015), Algorithm 1 and the proof of Lemma 6.8, printed pp.28--30: https://arxiv.org/pdf/1505.00107. The complete opposite-advice security argument and its iteration are separate results.
theorem
Algebraic.Cutwidth.Extractor.lookAheadBase_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}
[Fintype Z]
[Fintype A]
[Fintype B]
[Fintype Q]
(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)
(hl : ∀ (z : Z) (a : A), 0 ≤ l z a)
(hr : ∀ (z : Z) (b : B), 0 ≤ r z b)
:
mapWeight
(fun (p : (Z × B) × A) =>
have zq := (p.1.1, q p.1.1 p.1.2, q' p.1.1 p.1.2);
(((zq, lookAheadBaseMessage x x' initialSeed W QExt zq p.2), p.1.2), p.2))
(factoredWeight w l r) = factoredWeight (lookAheadBaseWeight w l r x x' q q' initialSeed W QExt) (lookAheadBaseLeft l x x' initialSeed W QExt)
(lookAheadBaseRight r q q')
Recording the right pair and all four left outputs preserves the full factored joint law.
theorem
Algebraic.Cutwidth.Extractor.lookAheadBase_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}
[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)
(hw : IsProbabilityWeight w)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
:
IsProbabilityWeight (lookAheadBaseWeight w l r x x' q q' initialSeed W QExt) ∧ (∀ (t : LookAheadBaseTranscript Z Q Mid), IsProbabilityWeight (lookAheadBaseLeft l x x' initialSeed W QExt t)) ∧ ∀ (t : LookAheadBaseTranscript Z Q Mid), IsProbabilityWeight (lookAheadBaseRight r q q' t)
The common transcript and both conditional kernels are normalized, including null rows.
theorem
Algebraic.Cutwidth.Extractor.lookAheadFirstRefreshWeight_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)
(hw : IsProbabilityWeight w)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
:
IsProbabilityWeight (lookAheadFirstRefreshWeight w l r x x' q q' initialSeed W QExt y R)
The first-output refresh and its complete retained state have a normalized actual law.
theorem
Algebraic.Cutwidth.Extractor.lookAheadTamperedRefreshWeight_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 y' : Z → B → Y)
(R : Y → Mid → Out)
(hw : IsProbabilityWeight w)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
:
IsProbabilityWeight (lookAheadTamperedRefreshWeight w l r x x' q q' initialSeed W QExt y y' R)
The second-output refresh, stored tampered refresh, and left state are normalized.
theorem
Algebraic.Cutwidth.Extractor.lookAheadBaseLeftEnvelope_nonnegative
{Z : Type u_1}
{B : Type u_2}
{Q : Type u_3}
{Mid : Type u_4}
[Fintype B]
(μ : Z → ℝ)
(r : Z → B → ℝ)
(q q' : Z → B → Q)
(hμ : ∀ (z : Z), 0 ≤ μ z)
(hr : ∀ (z : Z) (b : B), 0 ≤ r z b)
(t : LookAheadBaseTranscript Z Q Mid)
:
The common transcript preserves nonnegativity of the left source envelope.
theorem
Algebraic.Cutwidth.Extractor.lookAheadBaseRightEnvelope_nonnegative
{Z : Type u_1}
{A : Type u_2}
{X : Type u_3}
{Q : Type u_4}
{Seed : Type u_5}
{Mid : Type u_6}
[Fintype A]
(ν : Z → ℝ)
(l : Z → A → ℝ)
(x x' : Z → A → X)
(initialSeed : Q → Seed)
(W : X → Seed → Mid)
(QExt : Q → Mid → Seed)
(hν : ∀ (z : Z), 0 ≤ ν z)
(hl : ∀ (z : Z) (a : A), 0 ≤ l z a)
(t : LookAheadBaseTranscript Z Q Mid)
:
The common transcript preserves nonnegativity of the right source envelope.
theorem
Algebraic.Cutwidth.Extractor.lookAheadBase_left_envelope
{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}
[Fintype A]
[Fintype B]
(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)
(μ : Z → ℝ)
(hw : ∀ (z : Z), 0 ≤ w z)
(hl : ∀ (z : Z) (a : A), 0 ≤ l z a)
(hr : ∀ (z : Z) (b : B), 0 ≤ r z b)
(cap : ∀ (z : Z) (x₀ : X), w z * mapWeight (x z) (l z) x₀ ≤ μ z)
(t : LookAheadBaseTranscript Z Q Mid)
(x₀ : X)
:
lookAheadBaseWeight w l r x x' q q' initialSeed W QExt t * mapWeight (x t.1.1) (lookAheadBaseLeft l x x' initialSeed W QExt t) x₀ ≤ lookAheadBaseLeftEnvelope μ r q q' t
The original left source has the stated joint envelope under the common transcript.
theorem
Algebraic.Cutwidth.Extractor.lookAheadBase_right_envelope
{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}
[Fintype A]
[Fintype B]
(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)
(ν : Z → ℝ)
(hw : ∀ (z : Z), 0 ≤ w z)
(hl : ∀ (z : Z) (a : A), 0 ≤ l z a)
(hr : ∀ (z : Z) (b : B), 0 ≤ r z b)
(cap : ∀ (z : Z) (y₀ : Y), w z * mapWeight (y z) (r z) y₀ ≤ ν z)
(t : LookAheadBaseTranscript Z Q Mid)
(y₀ : Y)
:
lookAheadBaseWeight w l r x x' q q' initialSeed W QExt t * mapWeight (y t.1.1) (lookAheadBaseRight r q q' t) y₀ ≤ lookAheadBaseRightEnvelope ν l x x' initialSeed W QExt t
The original right source has the stated joint envelope under the common transcript.
theorem
Algebraic.Cutwidth.Extractor.lookAheadBaseLeftEnvelope_sum
{Z : Type u_1}
{B : Type u_2}
{Q : Type u_3}
{Mid : Type u_4}
[Fintype Z]
[Fintype B]
[Fintype Q]
[Fintype Mid]
(μ : Z → ℝ)
(r : Z → B → ℝ)
(q q' : Z → B → Q)
(mass : ∀ (z : Z), ∑ b : B, r z b = 1)
:
∑ t : LookAheadBaseTranscript Z Q Mid, lookAheadBaseLeftEnvelope μ r q q' t = ↑(Fintype.card ((Mid × Mid) × Mid × Mid)) * ∑ z : Z, μ z
The total left source envelope pays only for the four-output left message alphabet.
theorem
Algebraic.Cutwidth.Extractor.lookAheadBaseRightEnvelope_sum
{Z : Type u_1}
{A : Type u_2}
{X : Type u_3}
{Q : Type u_4}
{Seed : Type u_5}
{Mid : Type u_6}
[Fintype Z]
[Fintype A]
[Fintype Q]
[Fintype Mid]
(ν : Z → ℝ)
(l : Z → A → ℝ)
(x x' : Z → A → X)
(initialSeed : Q → Seed)
(W : X → Seed → Mid)
(QExt : Q → Mid → Seed)
(mass : ∀ (z : Z), ∑ a : A, l z a = 1)
:
∑ t : LookAheadBaseTranscript Z Q Mid, lookAheadBaseRightEnvelope ν l x x' initialSeed W QExt t = ↑(Fintype.card (Q × Q)) * ∑ z : Z, ν z
The total right source envelope pays only for the right-input pair alphabet.
theorem
Algebraic.Cutwidth.Extractor.lookAheadFirstRefreshWeight_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)
(hl : ∀ (z : Z) (a : A), 0 ≤ l z a)
(hr : ∀ (z : Z) (b : B), 0 ≤ r z b)
:
lookAheadFirstRefreshWeight w l r x x' q q' initialSeed W QExt y R = mapWeight (fun (p : (LookAheadBaseTranscript Z Q Mid × B) × A) => ((p.1.1, p.2), R (y p.1.1.1.1 p.1.2) 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'))
The first refresh is a right-only map once the common transcript fixes its seed.
theorem
Algebraic.Cutwidth.Extractor.lookAheadFirstRefreshWeight_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)
(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))
(lookAheadFirstRefreshWeight w l r x x' q q' initialSeed W QExt y R) = 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) t.2.1.1
Dropping the left state gives the exact refreshed seed law over the common transcript.
theorem
Algebraic.Cutwidth.Extractor.lookAheadTamperedRefresh_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)
(hl : ∀ (z : Z) (a : A), 0 ≤ l z a)
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
:
mapWeight
(fun (p : (Z × B) × A) =>
have zq := (p.1.1, q p.1.1 p.1.2, q' p.1.1 p.1.2);
have messages := lookAheadBaseMessage x x' initialSeed W QExt zq p.2;
((((zq, messages), R (y' p.1.1 p.1.2) messages.2.1), p.1.2), p.2))
(factoredWeight w l r) = factoredWeight
(observedTranscriptWeight (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) t.2.2.1)
(fun (tu : LookAheadBaseTranscript Z Q Mid × Out) => lookAheadBaseLeft l x x' initialSeed W QExt tu.1)
(observedTranscriptKernel (lookAheadBaseRight r q q') fun (t : LookAheadBaseTranscript Z Q Mid) (b : B) =>
R (y' t.1.1 b) t.2.2.1)
Revealing the tampered refresh preserves an exact successive-observation factorization.
theorem
Algebraic.Cutwidth.Extractor.lookAheadTamperedRefreshWeight_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]
[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 y' : Z → B → Y)
(R : Y → Mid → Out)
(hl : ∀ (z : Z) (a : A), 0 ≤ l z a)
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
:
lookAheadTamperedRefreshWeight w l r x x' q q' initialSeed W QExt y y' R = mapWeight
(fun (p : ((LookAheadBaseTranscript Z Q Mid × Out) × B) × A) =>
((p.1.1, p.2), R (y p.1.1.1.1.1 p.1.2) p.1.1.1.2.1.2))
(factoredWeight
(observedTranscriptWeight (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) t.2.2.1)
(fun (tu : LookAheadBaseTranscript Z Q Mid × Out) => lookAheadBaseLeft l x x' initialSeed W QExt tu.1)
(observedTranscriptKernel (lookAheadBaseRight r q q') fun (t : LookAheadBaseTranscript Z Q Mid) (b : B) =>
R (y' t.1.1 b) t.2.2.1))
The second refresh is right-only after the common transcript and tampered refresh.
theorem
Algebraic.Cutwidth.Extractor.WeightedStrongSeededExtractor.lookAhead_first_refresh_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}
{R : Y → Mid → Out}
{K J : ℕ}
{ε η δ : ℝ}
(first : WeightedStrongSeededExtractor W K ε)
(first_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)
(QExt : Q → Mid → Seed)
(y : 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 (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 (lookAheadFirstRefreshWeight w l r x x' q q' initialSeed W QExt y R)
(uniformSecondWeight (lookAheadFirstRefreshWeight w l r x x' q q' initialSeed W QExt y R)) ≤ η + (ε + δ + ↑K * ∑ z : Z, μ z) + ↑J * ↑(Fintype.card (Q × Q)) * ∑ z : Z, ν z
The actual first-output refresh is nearly uniform given the full left state and transcript.
theorem
Algebraic.Cutwidth.Extractor.WeightedStrongSeededExtractor.lookAhead_tampered_refresh_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 y' : 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)
(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 (lookAheadTamperedRefreshWeight w l r x x' q q' initialSeed W QExt y y' R)
(uniformSecondWeight (lookAheadTamperedRefreshWeight w l r x x' q q' initialSeed W QExt y y' R)) ≤ θ + (2 * ε + η + δ + ↑K * (1 + ↑(Fintype.card (Mid × Mid))) * ∑ z : Z, μ z + ↑L * ↑(Fintype.card (Seed × Seed)) * ∑ z : Z, ν z) + ↑J * ↑(Fintype.card (Q × Q)) * ↑(Fintype.card Out) * ∑ z : Z, ξ z
The actual second-output refresh is nearly uniform even retaining the tampered first refresh.