The killed walk, as an algorithm

The walk length and the killing denominator are constants of a round, so the walk is a constant-depth unrolling of the preprocessed rotation map, and the stopping index is chosen by a constant-depth chain of comparisons.

Main definitions

• Complexity.selectAt — choose among constantly many functions by a unary key
• Complexity.walkFn — the vertex a walk reaches after a constant number of steps

Main results

• Complexity.walkFn_mem_FP, Complexity.walkFn_eq — it is an FP function, and it computes ConstraintGraph.walkNum

theorem Complexity.ConstraintGraph.mem_cloudCodes_lt {α : Type} (G : ConstraintGraph α) {u : Fin G.numVerts} {c : ℕ} (h : c ∈ G.cloudCodes u) : c < 2 * G.numEdges

Every code in a cloud is below twice the edge count.

theorem Complexity.ConstraintGraph.preRotNum_fst_lt {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) {v : ℕ} (hv : v < 2 * G.numEdges) (d : ℕ) : (G.preRotNum E v d).1 < 2 * G.numEdges

The rotation map keeps a vertex number in range.

theorem Complexity.ConstraintGraph.walkNum_lt {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) {v : ℕ} (hv : v < 2 * G.numEdges) (s k : ℕ) : G.walkNum E s k v < 2 * G.numEdges

A walk stays in range.

theorem Complexity.ConstraintGraph.preDeg_eq {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) : G.preDeg E = 2 + 2 * E.degree

The preprocessed graph has 2 + 2 · deg darts at a vertex.

theorem Complexity.ConstraintGraph.preDeg_pos {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) : 0 < G.preDeg E

Choosing by a unary key

noncomputable def Complexity.selectAt (f : ℕ → List Bool → List Bool) (key : List Bool → List Bool) : ℕ → List Bool → List Bool

Choose among n + 1 functions by a unary key.

Equations

• Complexity.selectAt f key 0 x✝ = f 0 x✝
• Complexity.selectAt f key n.succ x✝ = Complexity.ifEqLen (key x✝) (List.replicate (n + 1) true) (f (n + 1) x✝) (Complexity.selectAt f key n x✝)

theorem Complexity.selectAt_mem_FP {f : ℕ → List Bool → List Bool} {key : List Bool → List Bool} (hf : ∀ (k : ℕ), f k ∈ FP) (hkey : key ∈ FP) (n : ℕ) : selectAt f key n ∈ FP

theorem Complexity.selectAt_eq {f : ℕ → List Bool → List Bool} {key : List Bool → List Bool} {z : List Bool} {m : ℕ} (hkey : key z = List.replicate m true) {n : ℕ} : m ≤ n → selectAt f key n z = f m z

Walking

noncomputable def Complexity.walkFn (F : FinBase) (pol : Polynomial ℕ) (deg P : ℕ) : ℕ → List Bool → List Bool

The vertex a walk reaches after k steps, on pair (graph) (pair (unary vertex) (unary steps)).

Equations

• One or more equations did not get rendered due to their size.
• Complexity.walkFn F pol deg P 0 x✝ = Complexity.pairFst (Complexity.pairSnd x✝)

theorem Complexity.walkFn_mem_FP (F : FinBase) (pol : Polynomial ℕ) (deg P k : ℕ) : walkFn F pol deg P k ∈ FP

theorem Complexity.walkFn_eq {α : Type} [Fintype α] [DecidableEq α] (F : FinBase) (pol : Polynomial ℕ) (hd : 1 < F.deg) (G : ConstraintGraph α) (v s : ℕ) (hv : v < 2 * G.numEdges) (hpc : ∀ (u : Fin G.numVerts), F.fitLevel hd (G.cloudList u).length ≤ Polynomial.eval (G.cloudList u).length pol) (hpe : F.fitLevel hd (2 * G.numEdges) ≤ Polynomial.eval (2 * G.numEdges) pol) (k : ℕ) : walkFn F pol (F.toFamily hd).degree (G.preDeg (F.toFamily hd)) k (pair (encGraph G) (pair (List.replicate v true) (List.replicate s true))) = List.replicate (G.walkNum (F.toFamily hd) s k v) true

The walk algorithm computes the walk.

Where the walk stops

theorem Complexity.findIdx_map {β γ : Type} (f : β → γ) (p : γ → Bool) (l : List β) : List.findIdx p (List.map f l) = List.findIdx (fun (x : β) => p (f x)) l

def Complexity.stopFromNum (q c : ℕ) : ℕ → ℕ → ℕ

The first zero digit at or after i, among the next n digits.

Equations

• Complexity.stopFromNum q c x✝ 0 = x✝
• Complexity.stopFromNum q c x✝ n.succ = if c / q ^ x✝ % q = 0 then x✝ else Complexity.stopFromNum q c (x✝ + 1) n

theorem Complexity.stopFromNum_eq_findIdx (q c n i : ℕ) : stopFromNum q c i n = i + List.findIdx (fun (j : Fin n) => c / q ^ (i + ↑j) % q == 0) (List.finRange n)

theorem Complexity.stopAtNum_eq_stopFromNum (T q c : ℕ) : stopAtNum T q c = stopFromNum q c 0 T

noncomputable def Complexity.stopFn (q : ℕ) (co : List Bool → List Bool) : ℕ → ℕ → List Bool → List Bool

Where the walk stops, from a unary reading co of the coins.

Equations

• Complexity.stopFn q co x✝¹ 0 x✝ = List.replicate x✝¹ true
• Complexity.stopFn q co x✝¹ n.succ x✝ = Complexity.ifEqLen (Complexity.modC q (Complexity.divC (q ^ x✝¹) (co x✝))) [] (List.replicate x✝¹ true) (Complexity.stopFn q co (x✝¹ + 1) n x✝)

theorem Complexity.stopFn_mem_FP {q : ℕ} {co : List Bool → List Bool} (hco : co ∈ FP) (n i : ℕ) : stopFn q co i n ∈ FP

theorem Complexity.stopFn_eq {q : ℕ} (hq : 0 < q) {co : List Bool → List Bool} {z : List Bool} {c : ℕ} (hco : co z = List.replicate c true) (n i : ℕ) : stopFn q co i n z = List.replicate (stopFromNum q c i n) true

The stopping algorithm finds the stopping index.

The dart the walk comes back by

noncomputable def Complexity.backFn (F : FinBase) (pol : Polynomial ℕ) (deg P i : ℕ) (w : List Bool) : List Bool

The label the walk's i-th step points back along.

Equations

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

theorem Complexity.backFn_mem_FP (F : FinBase) (pol : Polynomial ℕ) (deg P i : ℕ) : backFn F pol deg P i ∈ FP

theorem Complexity.backFn_eq {α : Type} [Fintype α] [DecidableEq α] {F : FinBase} {pol : Polynomial ℕ} (hd : 1 < F.deg) (G : ConstraintGraph α) (v s i : ℕ) (hv : v < 2 * G.numEdges) (hpc : ∀ (u : Fin G.numVerts), F.fitLevel hd (G.cloudList u).length ≤ Polynomial.eval (G.cloudList u).length pol) (hpe : F.fitLevel hd (2 * G.numEdges) ≤ Polynomial.eval (2 * G.numEdges) pol) : backFn F pol (F.toFamily hd).degree (G.preDeg (F.toFamily hd)) i (pair (encGraph G) (pair (List.replicate v true) (List.replicate s true))) = List.replicate (G.preRotNum (F.toFamily hd) (G.walkNum (F.toFamily hd) s i v) (s / G.preDeg (F.toFamily hd) ^ i % G.preDeg (F.toFamily hd))).2 true

The back-label algorithm reads the label off the rotation map.

noncomputable def Complexity.revSum (F : FinBase) (pol : Polynomial ℕ) (deg P k : ℕ) : ℕ → List Bool → List Bool

The reversed dart's digits, for a fixed stopping index k, over the first n places.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.revSum F pol deg P k 0 x✝ = []

theorem Complexity.revSum_mem_FP (F : FinBase) (pol : Polynomial ℕ) (deg P k n : ℕ) : revSum F pol deg P k n ∈ FP

theorem Complexity.length_revSum {α : Type} [Fintype α] [DecidableEq α] {F : FinBase} {pol : Polynomial ℕ} (hd : 1 < F.deg) (G : ConstraintGraph α) (v s k : ℕ) (hv : v < 2 * G.numEdges) (hpc : ∀ (u : Fin G.numVerts), F.fitLevel hd (G.cloudList u).length ≤ Polynomial.eval (G.cloudList u).length pol) (hpe : F.fitLevel hd (2 * G.numEdges) ≤ Polynomial.eval (2 * G.numEdges) pol) (n : ℕ) : (revSum F pol (F.toFamily hd).degree (G.preDeg (F.toFamily hd)) k n (pair (encGraph G) (pair (List.replicate v true) (List.replicate s true)))).length = ∑ j ∈ Finset.range n, (if j < k then (G.preRotNum (F.toFamily hd) (G.walkNum (F.toFamily hd) s (k - 1 - j) v) (s / G.preDeg (F.toFamily hd) ^ (k - 1 - j) % G.preDeg (F.toFamily hd))).2 else s / G.preDeg (F.toFamily hd) ^ j % G.preDeg (F.toFamily hd)) * G.preDeg (F.toFamily hd) ^ j

The digit sum has the reversed dart's number as its length.

noncomputable def Complexity.ConstraintGraph.revAtNum {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) (T k v s : ℕ) : ℕ

The reversed dart's number, for a fixed stopping index.

Equations

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

theorem Complexity.ConstraintGraph.killedRevNum_eq_revAtNum {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) (T q v s c : ℕ) : G.killedRevNum E T q v s c = G.revAtNum E T (stopAtNum T q c) v s

The powered graph's rotation map

noncomputable def Complexity.coinsOf (q T : ℕ) (z : List Bool) : List Bool

The coins of a killed dart.

Equations

• Complexity.coinsOf q T z = Complexity.modC (q ^ T) (Complexity.pairSnd (Complexity.pairSnd z))

noncomputable def Complexity.toWalk (q T : ℕ) (z : List Bool) : List Bool

A killed dart's steps, in the walk's input format.

Equations

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

theorem Complexity.coinsOf_mem_FP (q T : ℕ) : coinsOf q T ∈ FP

theorem Complexity.toWalk_mem_FP (q T : ℕ) : toWalk q T ∈ FP

noncomputable def Complexity.revNumFn (F : FinBase) (pol : Polynomial ℕ) (deg P T q : ℕ) (z : List Bool) : List Bool

The dart a killed walk comes back by, on pair (graph) (pair (unary vertex) (unary dart)).

Equations

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

theorem Complexity.revNumFn_mem_FP (F : FinBase) (pol : Polynomial ℕ) (deg P T q : ℕ) : revNumFn F pol deg P T q ∈ FP

noncomputable def Complexity.killedRotFn (F : FinBase) (pol : Polynomial ℕ) (deg P T q : ℕ) (z : List Bool) : List Bool

The powered graph's rotation map, on pair (graph) (pair (unary vertex) (unary dart)): walk to the end, come back by the reversed labels, and keep the coins.

Equations

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

theorem Complexity.killedRotFn_mem_FP (F : FinBase) (pol : Polynomial ℕ) (deg P T q : ℕ) : killedRotFn F pol deg P T q ∈ FP

theorem Complexity.marks_revSum_eq {α : Type} [Fintype α] [DecidableEq α] {F : FinBase} {pol : Polynomial ℕ} (hd : 1 < F.deg) (G : ConstraintGraph α) (T v s k : ℕ) (hv : v < 2 * G.numEdges) (hpc : ∀ (u : Fin G.numVerts), F.fitLevel hd (G.cloudList u).length ≤ Polynomial.eval (G.cloudList u).length pol) (hpe : F.fitLevel hd (2 * G.numEdges) ≤ Polynomial.eval (2 * G.numEdges) pol) : marks (revSum F pol (F.toFamily hd).degree (G.preDeg (F.toFamily hd)) k T (pair (encGraph G) (pair (List.replicate v true) (List.replicate s true)))) = List.replicate (G.revAtNum (F.toFamily hd) T k v s) true

theorem Complexity.revNumFn_eq {α : Type} [Fintype α] [DecidableEq α] {F : FinBase} {pol : Polynomial ℕ} (hd : 1 < F.deg) (G : ConstraintGraph α) (T q v s c : ℕ) (hq : 0 < q) (hv : v < 2 * G.numEdges) (hc : c < q ^ T) (hpc : ∀ (u : Fin G.numVerts), F.fitLevel hd (G.cloudList u).length ≤ Polynomial.eval (G.cloudList u).length pol) (hpe : F.fitLevel hd (2 * G.numEdges) ≤ Polynomial.eval (2 * G.numEdges) pol) : revNumFn F pol (F.toFamily hd).degree (G.preDeg (F.toFamily hd)) T q (pair (encGraph G) (pair (List.replicate v true) (List.replicate (s * q ^ T + c) true))) = List.replicate (G.killedRevNum (F.toFamily hd) T q v s c) true

The return-dart algorithm computes the dart the walk comes back by.

theorem Complexity.killedRotFn_eq {α : Type} [Fintype α] [DecidableEq α] {F : FinBase} {pol : Polynomial ℕ} (hd : 1 < F.deg) (G : ConstraintGraph α) (T q v s c : ℕ) (hq : 0 < q) (hv : v < 2 * G.numEdges) (hc : c < q ^ T) (hpc : ∀ (u : Fin G.numVerts), F.fitLevel hd (G.cloudList u).length ≤ Polynomial.eval (G.cloudList u).length pol) (hpe : F.fitLevel hd (2 * G.numEdges) ≤ Polynomial.eval (2 * G.numEdges) pol) : killedRotFn F pol (F.toFamily hd).degree (G.preDeg (F.toFamily hd)) T q (pair (encGraph G) (pair (List.replicate v true) (List.replicate (s * q ^ T + c) true))) = pair (List.replicate (G.killedRotNum (F.toFamily hd) T q v s c).1 true) (List.replicate (G.killedRotNum (F.toFamily hd) T q v s c).2 true)

The rotation algorithm runs the powered graph's rotation map.