The bounded data a composed edge depends on

A composed edge's second endpoint and its constraint depend on the outer graph only through what one killed walk meets: the darts it takes, the parity of each vertex it stands on, the code of each constraint there, and the darts it returns by — together with the random string and the read. All of that lives in finite types that do not mention the graph, so it is a key of bounded length, and the edge's data is a function of the key alone.

Main definitions

• Complexity.StepKey — that data
• Complexity.packKey, Complexity.keyOfString — writing it out as a string, and reading it back
• Complexity.relOfKey — the constraint it describes
• Complexity.satSetOfKey — and the satisfying set

Main results

• Complexity.keyOfString_packKey — the reading inverts the writing
• Complexity.relOfKey_stepKeyOf — on a walk's own data it is the killed constraint
• Complexity.cubeOfKey_eq, Complexity.codeOfKey_eq — so the data alone gives the composed edge's second endpoint and its constraint

@[reducible, inline]

abbrev Complexity.StepKey (E : ExpanderFamily) (T q B C : ℕ) : Type

The bounded data a composed edge's head and constraint depend on.

Equations

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

def Complexity.StepKey.dart {E : ExpanderFamily} {T q B C : ℕ} (k : StepKey E T q B C) : Fin T → PreDart E

The walk's darts.

Equations

• k.dart = k.1.1

def Complexity.StepKey.coins {E : ExpanderFamily} {T q B C : ℕ} (k : StepKey E T q B C) : Fin T → Fin q

Its coins.

Equations

• k.coins = k.1.2

def Complexity.StepKey.par {E : ExpanderFamily} {T q B C : ℕ} (k : StepKey E T q B C) : Fin T → Fin 2

The parity of the vertex each step stands on.

Equations

• k.par = k.2.1.1

def Complexity.StepKey.code {E : ExpanderFamily} {T q B C : ℕ} (k : StepKey E T q B C) : Fin T → Fin C

The code of the constraint each step meets.

Equations

• k.code = k.2.1.2

def Complexity.StepKey.rev {E : ExpanderFamily} {T q B C : ℕ} (k : StepKey E T q B C) : Fin T → PreDart E

The darts the walk returns by.

Equations

• k.rev = k.2.2.1

def Complexity.StepKey.rand {E : ExpanderFamily} {T q B C : ℕ} (k : StepKey E T q B C) : BooleanAnalysis.Cube (Tester.ROf B)

The tester's random string.

Equations

• k.rand = k.2.2.2.1

def Complexity.StepKey.read {E : ExpanderFamily} {T q B C : ℕ} (k : StepKey E T q B C) : ReadIdx

The read.

Equations

• k.read = k.2.2.2.2

def Complexity.StepKey.len {E : ExpanderFamily} {T q B C : ℕ} (k : StepKey E T q B C) : ℕ

How long the effective walk is.

Equations

• k.len = Complexity.stopAt k.coins

theorem Complexity.StepKey.len_le {E : ExpanderFamily} {T q B C : ℕ} (k : StepKey E T q B C) : k.len ≤ T

noncomputable def Complexity.relOfKey {α : Type} [Fintype α] [DecidableEq α] {E : ExpanderFamily} {T q B C : ℕ} (k : StepKey E T q B C) : (PreWalk E T → α) → (PreWalk E T → α) → Bool

The constraint the data describes: at each step of the effective walk, the preprocessed constraint its code and parity stand for.

Equations

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

noncomputable def Complexity.satSetOfKey {α : Type} [Fintype α] [DecidableEq α] {E : ExpanderFamily} {T q B C : ℕ} (encβ : (PreWalk E T → α) → BooleanAnalysis.Cube B) (k : StepKey E T q B C) : Finset (BooleanAnalysis.Cube (Tester.kOf B))

The satisfying set the data describes.

Equations

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

Writing the data out

noncomputable def Complexity.decOr {X : Type} [NumEnc X] (d : X) (n : ℕ) : X

The value a number names, or a default.

Equations

• Complexity.decOr d n = (Complexity.NumEnc.dec n).getD d

theorem Complexity.decOr_enc {X : Type} [NumEnc X] (d a : X) : decOr d (NumEnc.enc a) = a

noncomputable def Complexity.packKey {E : ExpanderFamily} {T q B C : ℕ} (k : StepKey E T q B C) : List Bool

The data written out: one unary number per component.

Equations

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

noncomputable def Complexity.keyOfString {E : ExpanderFamily} {T q B C : ℕ} (dflt : StepKey E T q B C) (s : List Bool) : StepKey E T q B C

The data read back from a string, falling back on a default.

Equations

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

theorem Complexity.keyOfString_packKey {E : ExpanderFamily} {T q B C : ℕ} (dflt k : StepKey E T q B C) : keyOfString dflt (packKey k) = k

The reading inverts the writing.

theorem Complexity.length_digitSum_eq_enc {X : Type} [NumEnc X] {T : ℕ} (s : Fin T → X) (digit : ℕ → List Bool → List Bool) (w : List Bool) (h : ∀ (j : ℕ) (hj : j < T), (digit j w).length = NumEnc.enc (s ⟨j, hj⟩)) : (digitSum (NumEnc.card X) digit T w).length = NumEnc.enc s

A digit sum is a tuple's number, when the digits are the entries'.

noncomputable def Complexity.stepKeyOf {α : Type} [Fintype α] [DecidableEq α] (G : ConstraintGraph α) (E : ExpanderFamily) {q T : ℕ} (v : (G.preprocess E).graph.V) (x : (Fin T → (G.preprocess E).graph.D) × (Fin T → Fin q)) (B : ℕ) (z : BooleanAnalysis.Cube (Tester.ROf B)) (i : ReadIdx) : StepKey E T q B (Fintype.card (α → α → Bool))

The data a killed walk actually shows.

Equations

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

theorem Complexity.relOfKey_stepKeyOf {α : 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)) (B : ℕ) (z : BooleanAnalysis.Cube (Tester.ROf B)) (i : ReadIdx) : relOfKey (stepKeyOf G E v x B z i) = ((G.preprocess E).killedPow q T hq).rel v x

The data a walk shows describes that walk's constraint.

theorem Complexity.satSetOfKey_stepKeyOf {α : 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)) {B : ℕ} (z : BooleanAnalysis.Cube (Tester.ROf B)) (i : ReadIdx) (encβ : (PreWalk E T → α) → BooleanAnalysis.Cube B) : satSetOfKey encβ (stepKeyOf G E v x B z i) = RegCSP.satSet encβ ((G.preprocess E).killedPow q T hq) (v, x)

The data a walk shows describes that walk's satisfying set.

noncomputable def Complexity.cubeOfKey {α : Type} [Fintype α] [DecidableEq α] {E : ExpanderFamily} {T q B C : ℕ} (encβ : (PreWalk E T → α) → BooleanAnalysis.Cube B) (k : StepKey E T q B C) : ℕ

The cube the data names.

Equations

• Complexity.cubeOfKey encβ k = Complexity.RegCSP.cubeOfSet (Complexity.satSetOfKey encβ k) k.rand k.read

noncomputable def Complexity.codeOfKey {α : Type} [Fintype α] [DecidableEq α] {E : ExpanderFamily} {T q B C : ℕ} (encβ : (PreWalk E T → α) → BooleanAnalysis.Cube B) (k : StepKey E T q B C) : ℕ

The constraint code the data names.

Equations

• Complexity.codeOfKey encβ k = Complexity.codeOfRel (Complexity.MultiTest.relOfCheck (Complexity.RegCSP.checkOfSet (Complexity.satSetOfKey encβ k) k.rand) k.read)

theorem Complexity.cubeOfKey_eq {α : 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)) {B : ℕ} (z : BooleanAnalysis.Cube (Tester.ROf B)) (i : ReadIdx) (encβ : (PreWalk E T → α) → BooleanAnalysis.Cube B) : cubeOfKey encβ (stepKeyOf G E v x B z i) = ((G.preprocess E).killedPow q T hq).cubeNum encβ (v, x) z i

The data gives the composed edge's cube.

theorem Complexity.codeOfKey_eq {α : 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)) {B : ℕ} (z : BooleanAnalysis.Cube (Tester.ROf B)) (i : ReadIdx) (encβ : (PreWalk E T → α) → BooleanAnalysis.Cube B) : codeOfKey encβ (stepKeyOf G E v x B z i) = codeOfRel (MultiTest.relOfCheck ((RegCSP.compose encβ ((G.preprocess E).killedPow q T hq)).check (v, x) z) i)

And the composed edge's constraint.