The actual opposite-advice flip-flop law

The retained transcript records the old transcript, both initial right states, the four first look-ahead outputs, both refreshed states, the four second look-ahead outputs, and the tampered final output. The law also retains the entire original left state. Every recorded value is computed from the original factored source law by the actual matched extractors.

This is the opposite-advice step of Chattopadhyay--Goyal--Li, Algorithm 1 and Lemma 6.8, in Non-Malleable Extractors and Codes, with their Many Tampered Extensions, Section 6.3: https://arxiv.org/pdf/1505.00107. No repaired distribution or supplied independence invariant occurs in this definition. The two honest advice-bit cases share exactly this transcript.

@[reducible, inline]

abbrev Algebraic.Cutwidth.Extractor.FlipFlopOppositeTranscript (Z : Type u_1) (L : ℕ) : Type u_1

Both complete look-ahead histories followed by the tampered final refresh.

Equations

• One or more equations did not get rendered due to their size.

def Algebraic.Cutwidth.Extractor.flipFlopOppositeTranscript (n m L e : ℕ) {Z : Type u_1} {A : Type u_2} {B : Type u_3} (x x' : Z → A → Fin n → Bool) (y y' : Z → B → Fin m → Bool) (q q' : Z → B → Fin (matchedBlockOutputBits 64 L) → Bool) (b : Bool) (p : (Z × B) × A) : FlipFlopOppositeTranscript Z L

The full retained history of the actual honest and opposite-advice tampered executions.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algebraic.Cutwidth.Extractor.flipFlopOppositeWeight (n m L e : ℕ) {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x x' : Z → A → Fin n → Bool) (y y' : Z → B → Fin m → Bool) (q q' : Z → B → Fin (matchedBlockOutputBits 64 L) → Bool) (b : Bool) : (FlipFlopOppositeTranscript Z L × A) × (Fin (matchedBlockOutputBits 64 L) → Bool) → ℝ

The original-law output, retaining the full history and the complete original left state.

Equations

• One or more equations did not get rendered due to their size.