The killed walk, in numbers

A dart of the powered graph is a tuple of steps together with a tuple of coins; the walk runs until the first coin that is zero. NumEncPi numbers both tuples digit by digit, so an algorithm recovers a step or a coin by dividing and taking the remainder. This module reads the stopping rule off those digits.

Main definitions

• Complexity.stopAtNum — where a killed walk stops, from the coins' number

Main results

• Complexity.stopAtNum_eq — it is the abstract stopping index
• Complexity.ConstraintGraph.walkNum_eq — and following the step digits walks the preprocessed graph
• Complexity.ConstraintGraph.killedRevNum_eq — the dart a killed walk comes back by, digit by digit
• Complexity.ConstraintGraph.killedRotNum_eq — the powered graph's rotation map, in numbers

theorem Complexity.findIdx_congr {β : Type} {l : List β} {p q : β → Bool} (h : ∀ x ∈ l, p x = q x) : List.findIdx p l = List.findIdx q l

def Complexity.stopAtNum (T q c : ℕ) : ℕ

Where a killed walk stops, read off the coins' number: the first digit that is zero, or the whole length if there is none.

Equations

• Complexity.stopAtNum T q c = List.findIdx (fun (j : Fin T) => c / q ^ ↑j % q == 0) (List.finRange T)

theorem Complexity.stopAtNum_eq {T q : ℕ} (hq : 0 < q) (c : Fin T → Fin q) : stopAtNum T q (NumEnc.enc c) = stopAt c

The digits give the stopping index.

noncomputable def Complexity.ConstraintGraph.preDeg {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) : ℕ

How many darts the preprocessed graph has at each vertex.

Equations

• G.preDeg E = Complexity.NumEnc.card (G.preprocess E).graph.D

noncomputable def Complexity.ConstraintGraph.walkNum {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) (s : ℕ) : ℕ → ℕ → ℕ

The vertex reached after k steps, following the digits of s.

Equations

• G.walkNum E s 0 x✝ = x✝
• G.walkNum E s k.succ x✝ = (G.preRotNum E (G.walkNum E s k x✝) (s / G.preDeg E ^ k % G.preDeg E)).1

theorem Complexity.ConstraintGraph.digit_enc {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) {T : ℕ} (s : Fin T → (G.preprocess E).graph.D) (hpos : 0 < G.preDeg E) (k : ℕ) (hk : k < T) : NumEnc.enc s / G.preDeg E ^ k % G.preDeg E = NumEnc.enc (s ⟨k, hk⟩)

The digits of a tuple's number are its entries' numbers.

theorem Complexity.ConstraintGraph.walkNum_eq {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) {T : ℕ} (v : G.HalfEdge) (s : Fin T → (G.preprocess E).graph.D) (n : ℕ) (hdig : ∀ (k : ℕ) (hk : k < T), n / G.preDeg E ^ k % G.preDeg E = NumEnc.enc (s ⟨k, hk⟩)) {k : ℕ} : k ≤ T → G.walkNum E n k (NumEnc.enc v) = NumEnc.enc ((G.preprocess E).graph.walkAt T v s k)

Following the digits walks the graph. The steps are read from any number whose digits are the tuple's entries, so a prefix of a longer walk may be run from that walk's own number.

The dart the walk comes back by

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

The dart a killed walk comes back by, in numbers: below the stopping index the digits are the labels pointing back, read in reverse order; above it they are the original steps.

Equations

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

theorem Complexity.ConstraintGraph.killedRevNum_eq {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) {T q : ℕ} (hq : 0 < q) (hpos : 0 < G.preDeg E) (v : G.HalfEdge) (s : Fin T → (G.preprocess E).graph.D) (c : Fin T → Fin q) : G.killedRevNum E T q (NumEnc.enc v) (NumEnc.enc s) (NumEnc.enc c) = NumEnc.enc ((G.preprocess E).graph.killedRev v s c)

The digits give the dart the walk comes back by.

The powered graph's rotation map

noncomputable def Complexity.ConstraintGraph.killedRotNum {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) (T q v s c : ℕ) : ℕ × ℕ

The powered graph's rotation map, in numbers: walk to the end, come back by the reversed labels, and keep the coins.

Equations

• G.killedRotNum E T q v s c = (G.walkNum E s (Complexity.stopAtNum T q c) v, G.killedRevNum E T q v s c * q ^ T + c)

theorem Complexity.ConstraintGraph.killedRotNum_eq {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) {T q : ℕ} (hq : 0 < q) (hpos : 0 < G.preDeg E) (v : G.HalfEdge) (x : (Fin T → (G.preprocess E).graph.D) × (Fin T → Fin q)) {w : G.HalfEdge} {y : (Fin T → (G.preprocess E).graph.D) × (Fin T → Fin q)} (hw : ((G.preprocess E).graph.killedPower q T hq).rot (v, x) = (w, y)) : G.killedRotNum E T q (NumEnc.enc v) (NumEnc.enc x.1) (NumEnc.enc x.2) = (NumEnc.enc w, NumEnc.enc y)

The numbers run the powered graph's rotation map.