The preprocessed constraint, in numbers

Preprocessing leaves three kinds of constraint: the original one at an edge-link, oriented by the half-edge's side; equality inside a cloud; and nothing at all at a self-loop or an expander edge. So the constraint at a dart is a fixed function of the dart's number, the half-edge's side, and the code of the original constraint — a bounded amount of data.

Main definitions

• Complexity.preRelCode — the constraint a dart's number and a code stand for

Main results

• Complexity.preRel_eq — it is the preprocessed system's constraint
• Complexity.rel_killedPow_preprocess — the killed power's constraint runs those codes along the walk
• Complexity.rel_killedPow_eq_relOfSteps — so it depends on the graph only through the walk's parities and codes
• Complexity.rel_killedPow_eq_preRelOfSteps — the same, with every argument at a type that does not mention the graph

noncomputable def Complexity.preRelCode (α : Type) [Fintype α] [DecidableEq α] (deg c u d : ℕ) (a b : α) : Bool

The preprocessed system's constraint, from the dart's number d, the half-edge's number u and the code c of the original constraint.

Equations

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

theorem Complexity.preRel_eq {α : Type} [Fintype α] [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) (p : G.HalfEdge) (d : (G.preprocess E).graph.D) (a b : α) : (G.preprocess E).rel p d a b = preRelCode α E.degree (codeOfRel (G.rel p.1)) (NumEnc.enc p) (NumEnc.enc d) a b

The numbers give the preprocessed constraint.

theorem Complexity.preRelCode_mod {α : Type} [Fintype α] [DecidableEq α] (deg c u d : ℕ) (a b : α) : preRelCode α deg c (u % 2) d a b = preRelCode α deg c u d a b

Only the parity of a half-edge's number matters.

theorem Complexity.rel_killedPow_preprocess {α : Type} [Fintype α] [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) {q T : ℕ} (hq : 0 < q) (v : (G.preprocess E).graph.V) (x : (Fin T → (G.preprocess E).graph.D) × (Fin T → Fin q)) (a b : KOpinion (G.preprocess E).graph T α) : ((G.preprocess E).killedPow q T hq).rel v x a b = decide (∀ (i : Fin ((G.preprocess E).graph.kLen x)), preRelCode α E.degree (codeOfRel (G.rel ((G.preprocess E).graph.walkAt ((G.preprocess E).graph.kLen x) v ((G.preprocess E).graph.kWalk x) ↑i).1)) (NumEnc.enc ((G.preprocess E).graph.walkAt ((G.preprocess E).graph.kLen x) v ((G.preprocess E).graph.kWalk x) ↑i)) (NumEnc.enc ((G.preprocess E).graph.kWalk x i)) (a ((G.preprocess E).graph.startIdx ⋯ ((G.preprocess E).graph.kWalk x) i)) (b ((G.preprocess E).graph.endIdx ⋯ v ((G.preprocess E).graph.kWalk x) i)) = true)

The killed power's constraint, along the walk. Each step contributes the preprocessed constraint at the vertex it stands on, read off that vertex's number and the code of the original constraint there.

noncomputable def Complexity.relOfSteps {α : Type} [Fintype α] [DecidableEq α] {Gr : RegGraph} [NumEnc Gr.D] {T : ℕ} (deg n : ℕ) (dart : Fin n → Gr.D) (par code : Fin n → ℕ) (sIdx eIdx : Fin n → VarWalk Gr T) (a b : KOpinion Gr T α) : Bool

What a killed dart's constraint runs: at each step, the dart it takes, the parity of the vertex it stands on, the code of the constraint there, and where the two ends hold their opinions about that step.

Equations

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

theorem Complexity.rel_killedPow_eq_relOfSteps {α : Type} [Fintype α] [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) {q T : ℕ} (hq : 0 < q) (v : (G.preprocess E).graph.V) (x : (Fin T → (G.preprocess E).graph.D) × (Fin T → Fin q)) : ((G.preprocess E).killedPow q T hq).rel v x = relOfSteps E.degree ((G.preprocess E).graph.kLen x) ((G.preprocess E).graph.kWalk x) (fun (i : Fin ((G.preprocess E).graph.kLen x)) => NumEnc.enc ((G.preprocess E).graph.walkAt ((G.preprocess E).graph.kLen x) v ((G.preprocess E).graph.kWalk x) ↑i) % 2) (fun (i : Fin ((G.preprocess E).graph.kLen x)) => codeOfRel (G.rel ((G.preprocess E).graph.walkAt ((G.preprocess E).graph.kLen x) v ((G.preprocess E).graph.kWalk x) ↑i).1)) ((G.preprocess E).graph.startIdx ⋯ ((G.preprocess E).graph.kWalk x)) ((G.preprocess E).graph.endIdx ⋯ v ((G.preprocess E).graph.kWalk x))

The killed power's constraint depends on the graph only through the walk's parities and codes — a bounded amount of data.

Types that do not mention the graph

@[reducible, inline]

abbrev Complexity.PreDart (E : ExpanderFamily) : Type

The darts of a preprocessed system: the self-loop, the edge-link, the cloud's and the expander's. This is the dart type of preprocess for every graph, so data about a preprocessed walk lives at a type that does not grow with the input.

Equations

• Complexity.PreDart E = (Unit ⊕ Option (Fin E.degree) ⊕ Fin E.degree)

theorem Complexity.D_preprocess {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) : (G.preprocess E).graph.D = PreDart E

@[reducible, inline]

abbrev Complexity.PreWalk (E : ExpanderFamily) (T : ℕ) : Type

Walks of length at most T in a preprocessed system, likewise.

Equations

• Complexity.PreWalk E T = ((ℓ : Fin (T + 1)) × (Fin ↑ℓ → Complexity.PreDart E))

theorem Complexity.varWalk_preprocess {α : Type} [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) (T : ℕ) : VarWalk (G.preprocess E).graph T = PreWalk E T

noncomputable def Complexity.preRelOfSteps {α : Type} [Fintype α] [DecidableEq α] (E : ExpanderFamily) (T deg n : ℕ) (dart : Fin n → PreDart E) (par code : Fin n → ℕ) (sIdx eIdx : Fin n → PreWalk E T) (a b : PreWalk E T → α) : Bool

The killed constraint, with every argument at a graph-free type.

Equations

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

theorem Complexity.rel_killedPow_eq_preRelOfSteps {α : Type} [Fintype α] [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) {q T : ℕ} (hq : 0 < q) (v : (G.preprocess E).graph.V) (x : (Fin T → (G.preprocess E).graph.D) × (Fin T → Fin q)) : ((G.preprocess E).killedPow q T hq).rel v x = preRelOfSteps E T E.degree ((G.preprocess E).graph.kLen x) ((G.preprocess E).graph.kWalk x) (fun (i : Fin ((G.preprocess E).graph.kLen x)) => NumEnc.enc ((G.preprocess E).graph.walkAt ((G.preprocess E).graph.kLen x) v ((G.preprocess E).graph.kWalk x) ↑i) % 2) (fun (i : Fin ((G.preprocess E).graph.kLen x)) => codeOfRel (G.rel ((G.preprocess E).graph.walkAt ((G.preprocess E).graph.kLen x) v ((G.preprocess E).graph.kWalk x) ↑i).1)) ((G.preprocess E).graph.startIdx ⋯ ((G.preprocess E).graph.kWalk x)) ((G.preprocess E).graph.endIdx ⋯ v ((G.preprocess E).graph.kWalk x))

The killed power's constraint, as data at graph-free types. Two graphs whose walks show the same darts, parities, codes and opinion indices carry the same constraint.

theorem Complexity.rel_eq_of_data {α : Type} [Fintype α] [DecidableEq α] (G G' : ConstraintGraph α) (E : ExpanderFamily) {q T : ℕ} (hq : 0 < q) (v : (G.preprocess E).graph.V) (v' : (G'.preprocess E).graph.V) (x : (Fin T → (G.preprocess E).graph.D) × (Fin T → Fin q)) (hpar : (fun (i : Fin ((G.preprocess E).graph.kLen x)) => NumEnc.enc ((G.preprocess E).graph.walkAt ((G.preprocess E).graph.kLen x) v ((G.preprocess E).graph.kWalk x) ↑i) % 2) = fun (i : Fin ((G'.preprocess E).graph.kLen x)) => NumEnc.enc ((G'.preprocess E).graph.walkAt ((G'.preprocess E).graph.kLen x) v' ((G'.preprocess E).graph.kWalk x) ↑i) % 2) (hcode : (fun (i : Fin ((G.preprocess E).graph.kLen x)) => codeOfRel (G.rel ((G.preprocess E).graph.walkAt ((G.preprocess E).graph.kLen x) v ((G.preprocess E).graph.kWalk x) ↑i).1)) = fun (i : Fin ((G'.preprocess E).graph.kLen x)) => codeOfRel (G'.rel ((G'.preprocess E).graph.walkAt ((G'.preprocess E).graph.kLen x) v' ((G'.preprocess E).graph.kWalk x) ↑i).1)) (hend : (G.preprocess E).graph.endIdx ⋯ v ((G.preprocess E).graph.kWalk x) = (G'.preprocess E).graph.endIdx ⋯ v' ((G'.preprocess E).graph.kWalk x)) : ((G.preprocess E).killedPow q T hq).rel v x = ((G'.preprocess E).killedPow q T hq).rel v' x

Two graphs whose walks show the same data carry the same constraint. The walk itself is shared: an algorithm reads it off the dart's number, which is the same on both sides.