Walk programs and certificates for fixed-length graph walks

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.

A rotation certificate charges the runtime input together with the vertex and label. A fixed number of calls therefore has polynomial cost, including all intermediate vertices and the complete returned label sequence. The walk length and killing rate are fixed parameters; these results do not claim a bound uniform in either parameter.

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.
• Turing.MultiTapeTM.ComputableInPolyTime.rotationMap_walkAtWithInput: a vertex along a fixed walk.
• Turing.MultiTapeTM.ComputableInPolyTime.rotationMap_powRotWithInput: a fixed power rotation.
• Turing.MultiTapeTM.ComputableInPolyTime.rotationMap_killedPowRotWithInput: a fixed killed power.

References

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

def Cslib.RotationMap.powRotWithInput {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 × (Fin T → D)

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

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)) (m : ℕ) : 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.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.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.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.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.

theorem Turing.MultiTapeTM.ComputableInPolyTime.rotationMap_powRotWithInput {P V D : Type} {input : P ↪ List Bool} {vertex : V ↪ List Bool} {label : D ↪ List Bool} {rotate : P × V × D → V × D} (hrotate : ComputableInPolyTime rotate (encPair input (encPair vertex label)) (encPair vertex label)) (T : ℕ) : ComputableInPolyTime (Cslib.RotationMap.powRotWithInput rotate T) (encPair input (encPair vertex (encPi label))) (encPair vertex (encPi label))

A fixed power reverses all return labels while charging the runtime graph at every call.

theorem Turing.MultiTapeTM.ComputableInPolyTime.rotationMap_walkAtWithInput {P V D : Type} {input : P ↪ List Bool} {vertex : V ↪ List Bool} {label : D ↪ List Bool} {rotate : P × V × D → V × D} (hrotate : ComputableInPolyTime rotate (encPair input (encPair vertex label)) (encPair vertex label)) (T m : ℕ) : ComputableInPolyTime (fun (p : P × V × (Fin T → D)) => Cslib.RotationMap.walkAtWithInput rotate p m) (encPair input (encPair vertex (encPi label))) vertex

A fixed step of a fixed-length walk uses the joint certificate for the runtime graph.

theorem Turing.MultiTapeTM.ComputableInPolyTime.rotationMap_killedPowRotWithInput {P V D : Type} {input : P ↪ List Bool} {vertex : V ↪ List Bool} {label : D ↪ List Bool} {rotate : P × V × D → V × D} (hrotate : ComputableInPolyTime rotate (encPair input (encPair vertex label)) (encPair vertex label)) (T q : ℕ) [NeZero q] (signal : Fin q ↪ List Bool) : ComputableInPolyTime (Cslib.RotationMap.killedPowRotWithInput rotate T q) (encPair input (encPair vertex (encPair (encPi label) (encPi signal)))) (encPair vertex (encPair (encPi label) (encPi signal)))

A killed power branches on the fixed finite signal sequence, computes the actual stopped walk, and retains every unused label and every signal in the result.