Walk programs carrying an immutable input

An encoded graph supplies a total rotation program with the graph data as an extra input. The programs here carry that input through each call. Their interpretation lemmas require agreement only on encoded vertices of the mathematical graph, so malformed inputs and unused vertex names may have any total behavior.

Main definitions

• Cslib.RotationMap.walkAtWithInput: a vertex reached along a walk.
• Cslib.RotationMap.powRotWithInput: a walk and its complete reversed return labels.
• Cslib.RotationMap.killedPowRotWithInput: a stopped walk, retaining unused labels and signals.

Main results

• Cslib.RotationMap.walkAtWithInput_eq: agreement with a mathematical trajectory.
• Cslib.RotationMap.powRotWithInput_eq: agreement with a mathematical power rotation.
• Cslib.RotationMap.killedPowRotWithInput_eq: agreement with a killed power rotation.

References

• I. Dinur, The PCP theorem by gap amplification
• J. Radhakrishnan, Gap amplification in PCPs using lazy random walks

def Cslib.RotationMap.walkAtWithInput {P : Type u_1} {W : Type u_3} {D : Type u_4} (rotate : P × W × D → W × D) {T : ℕ} (p : P × W × (Fin T → D)) : ℕ → W

Follow the labels, retaining the original graph input at every rotation call. After all labels have been used, the walk stays at its endpoint.

def Cslib.RotationMap.powRotWithInput {P : Type u_1} {W : Type u_3} {D : Type u_4} (rotate : P × W × D → W × D) (T : ℕ) : P × W × (Fin T → D) → W × (Fin T → D)

A power rotation carries the immutable input and reverses all return labels.

def Cslib.RotationMap.killedPowRotWithInput {P : Type u_1} {W : Type u_3} {D : Type u_4} (rotate : P × W × D → W × D) (T q : ℕ) [NeZero q] (p : P × W × (Fin T → D) × (Fin T → Fin q)) : W × (Fin T → D) × (Fin T → Fin q)

A killed power reverses only the used prefix, preserving unused labels and kill signals.

theorem Cslib.RotationMap.killedPowRotWithInput_of_killTime {P : Type u_1} {W : Type u_3} {D : Type u_4} (rotate : P × W × D → W × D) {T q : ℕ} [NeZero q] (p : P × W × (Fin T → D) × (Fin T → Fin q)) {n : ℕ} (hn : n ≤ T) (hc : killTime p.2.2.2 = n) : killedPowRotWithInput rotate T q p = have stopped := powRotWithInput rotate n (p.1, p.2.1, Fin.take n hn p.2.2.1); (stopped.1, fun (i : Fin T) => if h : ↑i < n then stopped.2 ⟨↑i, h⟩ else p.2.2.1 i, p.2.2.2)

Once the stopping time is known, the dependent prefix has that concrete length.

theorem Cslib.RotationMap.walkAtWithInput_eq {P : Type u_1} {V : Type u_2} {W : Type u_3} {D : Type u_4} (rotate : P × W × D → W × D) (input : P) (G : RotationMap V D) (encode : V → W) (hrotate : ∀ (v : V) (d : D), rotate (input, encode v, d) = (encode (G.rot (v, d)).1, (G.rot (v, d)).2)) {T : ℕ} (v : V) (k : Fin T → D) (m : ℕ) : walkAtWithInput rotate (input, encode v, k) m = encode (G.walkAt (v, k) m)

Agreement of one rotation on encoded vertices gives agreement of every trajectory.

theorem Cslib.RotationMap.powRotWithInput_eq {P : Type u_1} {V : Type u_2} {W : Type u_3} {D : Type u_4} (rotate : P × W × D → W × D) (input : P) (G : RotationMap V D) (encode : V → W) (hrotate : ∀ (v : V) (d : D), rotate (input, encode v, d) = (encode (G.rot (v, d)).1, (G.rot (v, d)).2)) (T : ℕ) (v : V) (k : Fin T → D) : powRotWithInput rotate T (input, encode v, k) = (encode ((G.pow T).rot (v, k)).1, ((G.pow T).rot (v, k)).2)

A power program returns both the encoded endpoint and exactly the reversed mathematical return labels. No hypothesis is needed on rotations of unused vertex names.

theorem Cslib.RotationMap.killedPowRotWithInput_eq {P : Type u_1} {V : Type u_2} {W : Type u_3} {D : Type u_4} (rotate : P × W × D → W × D) (input : P) (G : RotationMap V D) (encode : V → W) (hrotate : ∀ (v : V) (d : D), rotate (input, encode v, d) = (encode (G.rot (v, d)).1, (G.rot (v, d)).2)) (T q : ℕ) [NeZero q] (v : V) (k : Fin T → D) (c : Fin T → Fin q) : killedPowRotWithInput rotate T q (input, encode v, k, c) = (encode ((G.killedPow T q).rot (v, k, c)).1, ((G.killedPow T q).rot (v, k, c)).2)

A killed power program agrees with the mathematical stopped walk, including its unused labels and original kill signals.