Actual refresh laws and their common look-ahead transcript

The transcript first records both right inputs and then the honest and tampered two-round outputs. Both refresh seeds are explicit coordinates. The first refresh uses the honest first output. The opposite-advice refresh uses the honest second output and retains the tampered refresh seeded by the tampered first output. Both calls read the original right source.

@[reducible, inline]

abbrev Algebraic.Cutwidth.Extractor.LookAheadBaseTranscript (Z : Type u_1) (Q : Type u_2) (Mid : Type u_3) : Type (max (max u_2 u_1) u_3)

The old transcript, both right inputs, then the two outputs of each look-ahead.

Equations

• Algebraic.Cutwidth.Extractor.LookAheadBaseTranscript Z Q Mid = ((Z × Q × Q) × (Mid × Mid) × Mid × Mid)

def Algebraic.Cutwidth.Extractor.lookAheadBaseMessage {Z : Type u_1} {A : Type u_2} {X : Type u_3} {Q : Type u_4} {Seed : Type u_5} {Mid : Type u_6} (x x' : Z → A → X) (initialSeed : Q → Seed) (W : X → Seed → Mid) (QExt : Q → Mid → Seed) (zq : Z × Q × Q) (a : A) : (Mid × Mid) × Mid × Mid

Both honest and tampered look-ahead outputs, after fixing the right input pair.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.lookAheadBaseWeight {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) : LookAheadBaseTranscript Z Q Mid → ℝ

The actual common transcript distribution after the right and left observations.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.lookAheadBaseLeft {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] (l : Z → A → ℝ) (x x' : Z → A → X) (initialSeed : Q → Seed) (W : X → Seed → Mid) (QExt : Q → Mid → Seed) : LookAheadBaseTranscript Z Q Mid → A → ℝ

The left conditional kernel after recording all four look-ahead outputs.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.lookAheadBaseRight {Z : Type u_1} {B : Type u_2} {Q : Type u_3} {Mid : Type u_4} [Fintype B] (r : Z → B → ℝ) (q q' : Z → B → Q) (t : LookAheadBaseTranscript Z Q Mid) : B → ℝ

The right conditional kernel after recording both right inputs.

Equations

• Algebraic.Cutwidth.Extractor.lookAheadBaseRight r q q' t = Algebraic.Cutwidth.Extractor.observedTranscriptKernel r (fun (z : Z) (b : B) => (q z b, q' z b)) t.1

noncomputable def Algebraic.Cutwidth.Extractor.lookAheadBaseLeftEnvelope {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) (t : LookAheadBaseTranscript Z Q Mid) : ℝ

The original left envelope scaled by the right-pair message probability.

Equations

• Algebraic.Cutwidth.Extractor.lookAheadBaseLeftEnvelope μ r q q' t = Algebraic.Cutwidth.Extractor.observedTranscriptWeight μ r (fun (z : Z) (b : B) => (q z b, q' z b)) t.1

noncomputable def Algebraic.Cutwidth.Extractor.lookAheadBaseRightEnvelope {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) : LookAheadBaseTranscript Z Q Mid → ℝ

The original right envelope scaled by the four-output left message probability.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.lookAheadFirstRefreshWeight {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] (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) : (LookAheadBaseTranscript Z Q Mid × A) × Out → ℝ

Refresh with the honest first output, retaining the common transcript and full left state.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.lookAheadTamperedRefreshWeight {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] (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) : ((LookAheadBaseTranscript Z Q Mid × Out) × A) × Out → ℝ

Refresh with the honest second output, retaining the tampered first-output refresh too.

Equations

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