Reading an edge's data off the input

The constants of a round — the expander's degree, the walk's length, the killing rate, how many constraints the alphabet has, how many random strings the tester uses — are fixed. Given them, an edge number of the composed graph splits by division into a test, a random string and a read; the test splits into a vertex and a killed dart; and the killed dart drives the walk, whose parities, codes and return darts are what the edge's data is made of.

This module writes that out as FP functions.

Main definitions

• Complexity.Round — the constants of a round
• Complexity.keyFn — the edge's data, as a string

Main results

• Complexity.keyFn_mem_FP — it is an FP function
• Complexity.keyFn_length_le — of bounded length, whatever the input
• Complexity.keyFn_eq — on a real edge it writes that edge's own data
• Complexity.cubeFn_eq, Complexity.codeFn_eq — so the composed edge's second endpoint and its constraint are FP functions of the input

structure Complexity.Round : Type

The constants of one round of amplification, as an algorithm sees them.

• deg : ℕ

  The expander's degree.

• P : ℕ

  The preprocessed system's degree.

• T : ℕ

  The walk's length.

• q : ℕ

  The killing rate.

• C : ℕ

  How many constraints there are on the alphabet.

• cZ : ℕ

  How many random strings the tester has.

def Complexity.Round.cD (r : Round) : ℕ

How many darts the powered graph has at a vertex.

Equations

• r.cD = r.P ^ r.T * r.q ^ r.T

def Complexity.Round.cQ (r : Round) : ℕ

How many coin tuples there are.

Equations

• r.cQ = r.q ^ r.T

Splitting an edge number

noncomputable def Complexity.testFn (r : Round) (w : List Bool) : List Bool

The test an edge belongs to.

Equations

• Complexity.testFn r w = Complexity.divC (r.cZ * 22) (Complexity.pairSnd w)

noncomputable def Complexity.randFn (r : Round) (w : List Bool) : List Bool

The random string it runs on.

Equations

• Complexity.randFn r w = Complexity.divC 22 (Complexity.modC (r.cZ * 22) (Complexity.pairSnd w))

noncomputable def Complexity.readFn (w : List Bool) : List Bool

The read it asks for.

Equations

• Complexity.readFn w = Complexity.modC 22 (Complexity.pairSnd w)

noncomputable def Complexity.dartFn (r : Round) (w : List Bool) : List Bool

The killed dart the test is.

Equations

• Complexity.dartFn r w = Complexity.modC r.cD (Complexity.testFn r w)

noncomputable def Complexity.vertFn (r : Round) (w : List Bool) : List Bool

The vertex it starts at.

Equations

• Complexity.vertFn r w = Complexity.divC r.cD (Complexity.testFn r w)

noncomputable def Complexity.stepsFn (r : Round) (w : List Bool) : List Bool

The walk's steps.

Equations

• Complexity.stepsFn r w = Complexity.divC r.cQ (Complexity.dartFn r w)

noncomputable def Complexity.coinFn (r : Round) (w : List Bool) : List Bool

The walk's coins.

Equations

• Complexity.coinFn r w = Complexity.modC r.cQ (Complexity.dartFn r w)

noncomputable def Complexity.walkArg (r : Round) (w : List Bool) : List Bool

The input the walk algorithm reads.

Equations

• Complexity.walkArg r w = Complexity.pair (Complexity.pairFst w) (Complexity.pair (Complexity.vertFn r w) (Complexity.stepsFn r w))

noncomputable def Complexity.killArg (r : Round) (w : List Bool) : List Bool

The input the killed-walk algorithms read.

Equations

• Complexity.killArg r w = Complexity.pair (Complexity.pairFst w) (Complexity.pair (Complexity.vertFn r w) (Complexity.dartFn r w))

theorem Complexity.testFn_mem_FP (r : Round) : testFn r ∈ FP

theorem Complexity.randFn_mem_FP (r : Round) : randFn r ∈ FP

theorem Complexity.readFn_mem_FP : readFn ∈ FP

theorem Complexity.dartFn_mem_FP (r : Round) : dartFn r ∈ FP

theorem Complexity.vertFn_mem_FP (r : Round) : vertFn r ∈ FP

theorem Complexity.stepsFn_mem_FP (r : Round) : stepsFn r ∈ FP

theorem Complexity.coinFn_mem_FP (r : Round) : coinFn r ∈ FP

theorem Complexity.walkArg_mem_FP (r : Round) : walkArg r ∈ FP

theorem Complexity.killArg_mem_FP (r : Round) : killArg r ∈ FP

The walk's data

noncomputable def Complexity.stopBlk (r : Round) (w : List Bool) : List Bool

Where the walk stops.

Equations

• Complexity.stopBlk r w = Complexity.stopFn r.q (Complexity.coinsOf r.q r.T) 0 r.T (Complexity.killArg r w)

theorem Complexity.stopBlk_mem_FP (r : Round) : stopBlk r ∈ FP

noncomputable def Complexity.parDigit (F : FinBase) (pol : Polynomial ℕ) (r : Round) (i : ℕ) (w : List Bool) : List Bool

The parity of the vertex the i-th step stands on, and 0 past the end.

Equations

• Complexity.parDigit F pol r i w = Complexity.ifLtLen (List.replicate i true) (Complexity.stopBlk r w) (Complexity.modC 2 (Complexity.walkFn F pol r.deg r.P i (Complexity.walkArg r w))) []

theorem Complexity.parDigit_mem_FP (F : FinBase) (pol : Polynomial ℕ) (r : Round) (i : ℕ) : parDigit F pol r i ∈ FP

noncomputable def Complexity.codeDigit (F : FinBase) (pol : Polynomial ℕ) (r : Round) (i : ℕ) (w : List Bool) : List Bool

The code of the constraint the i-th step meets, and 0 past the end.

Equations

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

theorem Complexity.codeDigit_mem_FP (F : FinBase) (pol : Polynomial ℕ) (r : Round) (i : ℕ) : codeDigit F pol r i ∈ FP

The data as a string

noncomputable def Complexity.keyFn (F : FinBase) (pol : Polynomial ℕ) (r : Round) (w : List Bool) : List Bool

An edge's data, written out as the seven blocks packKey expects.

Equations

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

theorem Complexity.keyFn_mem_FP (F : FinBase) (pol : Polynomial ℕ) (r : Round) : keyFn F pol r ∈ FP

What the blocks read

theorem Complexity.blocks_eq (r : Round) (hD : 0 < r.cD) (hZ : 0 < r.cZ) (g : List Bool) (a b c d : ℕ) (hb : b < r.cD) (hc : c < r.cZ) (hd : d < 22) : testFn r (pair g (List.replicate (((a * r.cD + b) * r.cZ + c) * 22 + d) true)) = List.replicate (a * r.cD + b) true ∧ vertFn r (pair g (List.replicate (((a * r.cD + b) * r.cZ + c) * 22 + d) true)) = List.replicate a true ∧ dartFn r (pair g (List.replicate (((a * r.cD + b) * r.cZ + c) * 22 + d) true)) = List.replicate b true ∧ randFn r (pair g (List.replicate (((a * r.cD + b) * r.cZ + c) * 22 + d) true)) = List.replicate c true ∧ readFn (pair g (List.replicate (((a * r.cD + b) * r.cZ + c) * 22 + d) true)) = List.replicate d true

The blocks split an edge number.

theorem Complexity.steps_coin_eq (r : Round) (hQ : 0 < r.cQ) (w : List Bool) (s t : ℕ) (ht : t < r.cQ) (hdart : dartFn r w = List.replicate (s * r.cQ + t) true) : stepsFn r w = List.replicate s true ∧ coinFn r w = List.replicate t true

The dart block splits into steps and coins.

theorem Complexity.walkArg_eq (r : Round) {w g : List Bool} {a s : ℕ} (hg : pairFst w = g) (hv : vertFn r w = List.replicate a true) (hs : stepsFn r w = List.replicate s true) : walkArg r w = pair g (pair (List.replicate a true) (List.replicate s true))

The walk's input, once the blocks are known.

theorem Complexity.killArg_eq (r : Round) {w g : List Bool} {a b : ℕ} (hg : pairFst w = g) (hv : vertFn r w = List.replicate a true) (hb : dartFn r w = List.replicate b true) : killArg r w = pair g (pair (List.replicate a true) (List.replicate b true))

The killed walk's input, likewise.

The walk, on encoded vertices

theorem Complexity.walkFn_enc {F : FinBase} {pol : Polynomial ℕ} {α : Type} [Fintype α] [DecidableEq α] (hd : 1 < F.deg) (G : ConstraintGraph α) {T q : ℕ} (v : (G.preprocess (F.toFamily hd)).graph.V) (x : (Fin T → (G.preprocess (F.toFamily hd)).graph.D) × (Fin T → Fin q)) (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) (j : ℕ) (hj : j ≤ (G.preprocess (F.toFamily hd)).graph.kLen x) : walkFn F pol (F.toFamily hd).degree (G.preDeg (F.toFamily hd)) j (pair (encGraph G) (pair (List.replicate (NumEnc.enc v) true) (List.replicate (NumEnc.enc x.1) true))) = List.replicate (NumEnc.enc ((G.preprocess (F.toFamily hd)).graph.walkAt ((G.preprocess (F.toFamily hd)).graph.kLen x) v ((G.preprocess (F.toFamily hd)).graph.kWalk x) j)) true

The walk algorithm, run on a dart's own numbers.

theorem Complexity.stopBlk_eq {F : FinBase} (r : Round) {α : Type} [Fintype α] [DecidableEq α] (hd : 1 < F.deg) (G : ConstraintGraph α) (hq : 0 < r.q) (v : (G.preprocess (F.toFamily hd)).graph.V) (x : (Fin r.T → (G.preprocess (F.toFamily hd)).graph.D) × (Fin r.T → Fin r.q)) {w : List Bool} (hg : pairFst w = encGraph G) (hv : vertFn r w = List.replicate (NumEnc.enc v) true) (hdart : dartFn r w = List.replicate (NumEnc.enc x) true) : stopBlk r w = List.replicate ((G.preprocess (F.toFamily hd)).graph.kLen x) true

The stopping block is the effective walk's length.

theorem Complexity.parBlk_eq {F : FinBase} {pol : Polynomial ℕ} (r : Round) {α : Type} [Fintype α] [DecidableEq α] (hd : 1 < F.deg) (G : ConstraintGraph α) (hq : 0 < r.q) (hdeg : r.deg = (F.toFamily hd).degree) (hP : r.P = G.preDeg (F.toFamily hd)) (v : (G.preprocess (F.toFamily hd)).graph.V) (x : (Fin r.T → (G.preprocess (F.toFamily hd)).graph.D) × (Fin r.T → Fin r.q)) {w : List Bool} (hg : pairFst w = encGraph G) (hv : vertFn r w = List.replicate (NumEnc.enc v) true) (hs : stepsFn r w = List.replicate (NumEnc.enc x.1) true) (hdart : dartFn r w = List.replicate (NumEnc.enc x) true) (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) (B : ℕ) (z : BooleanAnalysis.Cube (Tester.ROf B)) (i : ReadIdx) : marks (digitSum 2 (parDigit F pol r) r.T w) = List.replicate (NumEnc.enc (stepKeyOf G (F.toFamily hd) v x B z i).par) true

The parity block is the parity tuple's number.

theorem Complexity.enc_halfEdge_div_two {α : Type} (G : ConstraintGraph α) (p : G.HalfEdge) : NumEnc.enc p / 2 = ↑p.1

theorem Complexity.codeBlk_eq {F : FinBase} {pol : Polynomial ℕ} (r : Round) {α : Type} [Fintype α] [DecidableEq α] (hd : 1 < F.deg) (G : ConstraintGraph α) (hq : 0 < r.q) (hdeg : r.deg = (F.toFamily hd).degree) (hP : r.P = G.preDeg (F.toFamily hd)) (hC : r.C = Fintype.card (α → α → Bool)) (v : (G.preprocess (F.toFamily hd)).graph.V) (x : (Fin r.T → (G.preprocess (F.toFamily hd)).graph.D) × (Fin r.T → Fin r.q)) {w : List Bool} (hg : pairFst w = encGraph G) (hv : vertFn r w = List.replicate (NumEnc.enc v) true) (hs : stepsFn r w = List.replicate (NumEnc.enc x.1) true) (hdart : dartFn r w = List.replicate (NumEnc.enc x) true) (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) (B : ℕ) (z : BooleanAnalysis.Cube (Tester.ROf B)) (i : ReadIdx) : marks (digitSum r.C (codeDigit F pol r) r.T w) = List.replicate (NumEnc.enc (stepKeyOf G (F.toFamily hd) v x B z i).code) true

The code block is the code tuple's number.

theorem Complexity.revBlk_eq {F : FinBase} {pol : Polynomial ℕ} (r : Round) {α : Type} [Fintype α] [DecidableEq α] (hd : 1 < F.deg) (G : ConstraintGraph α) (hq : 0 < r.q) (hdeg : r.deg = (F.toFamily hd).degree) (hP : r.P = G.preDeg (F.toFamily hd)) (v : (G.preprocess (F.toFamily hd)).graph.V) (x : (Fin r.T → (G.preprocess (F.toFamily hd)).graph.D) × (Fin r.T → Fin r.q)) {w : List Bool} (hg : pairFst w = encGraph G) (hv : vertFn r w = List.replicate (NumEnc.enc v) true) (hdart : dartFn r w = List.replicate (NumEnc.enc x) true) (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) (B : ℕ) (z : BooleanAnalysis.Cube (Tester.ROf B)) (i : ReadIdx) : List.take (r.P ^ r.T) (revNumFn F pol r.deg r.P r.T r.q (killArg r w)) = List.replicate (NumEnc.enc (stepKeyOf G (F.toFamily hd) v x B z i).rev) true

The return-dart block is the return tuple's number.

theorem Complexity.keyFn_eq {F : FinBase} {pol : Polynomial ℕ} (r : Round) {α : Type} [Fintype α] [DecidableEq α] (hd : 1 < F.deg) (G : ConstraintGraph α) (hq : 0 < r.q) (hdeg : r.deg = (F.toFamily hd).degree) (hP : r.P = G.preDeg (F.toFamily hd)) (hC : r.C = Fintype.card (α → α → Bool)) (hZ : 0 < r.cZ) (v : (G.preprocess (F.toFamily hd)).graph.V) (x : (Fin r.T → (G.preprocess (F.toFamily hd)).graph.D) × (Fin r.T → Fin r.q)) {B : ℕ} (z : BooleanAnalysis.Cube (Tester.ROf B)) (i : ReadIdx) (hcZ : r.cZ = NumEnc.card (BooleanAnalysis.Cube (Tester.ROf B))) (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) : keyFn F pol r (pair (encGraph G) (List.replicate (((NumEnc.enc v * r.cD + NumEnc.enc x) * r.cZ + NumEnc.enc z) * 22 + NumEnc.enc i) true)) = packKey (stepKeyOf G (F.toFamily hd) v x B z i)

The algorithm writes out the walk's own data.

def Complexity.keyBound (r : Round) : ℕ

A bound on the length of an edge's data.

Equations

• Complexity.keyBound r = 2 * (2 * r.cD + 2 + r.cQ) + 2 + (2 * (2 * (r.T * (1 * 2 ^ r.T)) + 2 + r.T * (r.C * r.C ^ r.T)) + 2 + (2 * r.P ^ r.T + 2 + (2 * r.cZ + 2 + 22)))

theorem Complexity.keyFn_length_le (F : FinBase) (pol : Polynomial ℕ) (r : Round) (hQ : 0 < r.cQ) (hD : 0 < r.cD) (hZ : 0 < r.cZ) (hC : 0 < r.C) (w : List Bool) : (keyFn F pol r w).length ≤ keyBound r

The cube and the code, in polynomial time

noncomputable def Complexity.cubeFn (F : FinBase) (pol : Polynomial ℕ) (r : Round) {α : Type} [Fintype α] [DecidableEq α] {E : ExpanderFamily} {B : ℕ} (dflt : StepKey E r.T r.q B (Fintype.card (α → α → Bool))) (encβ : (PreWalk E r.T → α) → BooleanAnalysis.Cube B) (w : List Bool) : List Bool

The cube a composed edge's second endpoint names.

Equations

• Complexity.cubeFn F pol r dflt encβ w = List.replicate (Complexity.cubeOfKey encβ (Complexity.keyOfString dflt (Complexity.keyFn F pol r w))) true

noncomputable def Complexity.codeFn (F : FinBase) (pol : Polynomial ℕ) (r : Round) {α : Type} [Fintype α] [DecidableEq α] {E : ExpanderFamily} {B : ℕ} (dflt : StepKey E r.T r.q B (Fintype.card (α → α → Bool))) (encβ : (PreWalk E r.T → α) → BooleanAnalysis.Cube B) (w : List Bool) : List Bool

The code of a composed edge's constraint.

Equations

• Complexity.codeFn F pol r dflt encβ w = List.replicate (Complexity.codeOfKey encβ (Complexity.keyOfString dflt (Complexity.keyFn F pol r w))) true

theorem Complexity.cubeFn_mem_FP (F : FinBase) (pol : Polynomial ℕ) (r : Round) {α : Type} [Fintype α] [DecidableEq α] {E : ExpanderFamily} {B : ℕ} (hQ : 0 < r.cQ) (hD : 0 < r.cD) (hZ : 0 < r.cZ) (hC : 0 < r.C) (dflt : StepKey E r.T r.q B (Fintype.card (α → α → Bool))) (encβ : (PreWalk E r.T → α) → BooleanAnalysis.Cube B) : cubeFn F pol r dflt encβ ∈ FP

theorem Complexity.codeFn_mem_FP (F : FinBase) (pol : Polynomial ℕ) (r : Round) {α : Type} [Fintype α] [DecidableEq α] {E : ExpanderFamily} {B : ℕ} (hQ : 0 < r.cQ) (hD : 0 < r.cD) (hZ : 0 < r.cZ) (hC : 0 < r.C) (dflt : StepKey E r.T r.q B (Fintype.card (α → α → Bool))) (encβ : (PreWalk E r.T → α) → BooleanAnalysis.Cube B) : codeFn F pol r dflt encβ ∈ FP

theorem Complexity.cubeFn_eq {F : FinBase} {pol : Polynomial ℕ} (r : Round) {α : Type} [Fintype α] [DecidableEq α] {B : ℕ} (hd : 1 < F.deg) (G : ConstraintGraph α) (hq : 0 < r.q) (hdeg : r.deg = (F.toFamily hd).degree) (hP : r.P = G.preDeg (F.toFamily hd)) (hC : r.C = Fintype.card (α → α → Bool)) (hZ : 0 < r.cZ) (v : (G.preprocess (F.toFamily hd)).graph.V) (x : (Fin r.T → (G.preprocess (F.toFamily hd)).graph.D) × (Fin r.T → Fin r.q)) (z : BooleanAnalysis.Cube (Tester.ROf B)) (i : ReadIdx) (hcZ : r.cZ = NumEnc.card (BooleanAnalysis.Cube (Tester.ROf B))) (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) (dflt : StepKey (F.toFamily hd) r.T r.q B (Fintype.card (α → α → Bool))) (encβ : (PreWalk (F.toFamily hd) r.T → α) → BooleanAnalysis.Cube B) : cubeFn F pol r dflt encβ (pair (encGraph G) (List.replicate (((NumEnc.enc v * r.cD + NumEnc.enc x) * r.cZ + NumEnc.enc z) * 22 + NumEnc.enc i) true)) = List.replicate (((G.preprocess (F.toFamily hd)).killedPow r.q r.T hq).cubeNum encβ (v, x) z i) true

The cube algorithm computes the composed edge's cube.

theorem Complexity.cubeFn_eq' {F : FinBase} {pol : Polynomial ℕ} (r : Round) {α : Type} [Fintype α] [DecidableEq α] {B : ℕ} (hd : 1 < F.deg) (G : ConstraintGraph α) (hq : 0 < r.q) (hdeg : r.deg = (F.toFamily hd).degree) (hP : r.P = G.preDeg (F.toFamily hd)) (hC : r.C = Fintype.card (α → α → Bool)) (hZ : 0 < r.cZ) (p : ((G.preprocess (F.toFamily hd)).killedPow r.q r.T hq).Dart) (z : BooleanAnalysis.Cube (Tester.ROf B)) (i : ReadIdx) (hcZ : r.cZ = NumEnc.card (BooleanAnalysis.Cube (Tester.ROf B))) (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) (dflt : StepKey (F.toFamily hd) r.T r.q B (Fintype.card (α → α → Bool))) (encβ : (PreWalk (F.toFamily hd) r.T → α) → BooleanAnalysis.Cube B) : cubeFn F pol r dflt encβ (pair (encGraph G) (List.replicate (((NumEnc.enc p.1 * r.cD + NumEnc.enc p.2) * r.cZ + NumEnc.enc z) * 22 + NumEnc.enc i) true)) = List.replicate (((G.preprocess (F.toFamily hd)).killedPow r.q r.T hq).cubeNum encβ p z i) true

The cube algorithm, with the dart given as one object.

theorem Complexity.codeFn_eq {F : FinBase} {pol : Polynomial ℕ} (r : Round) {α : Type} [Fintype α] [DecidableEq α] {B : ℕ} (hd : 1 < F.deg) (G : ConstraintGraph α) (hq : 0 < r.q) (hdeg : r.deg = (F.toFamily hd).degree) (hP : r.P = G.preDeg (F.toFamily hd)) (hC : r.C = Fintype.card (α → α → Bool)) (hZ : 0 < r.cZ) (v : (G.preprocess (F.toFamily hd)).graph.V) (x : (Fin r.T → (G.preprocess (F.toFamily hd)).graph.D) × (Fin r.T → Fin r.q)) (z : BooleanAnalysis.Cube (Tester.ROf B)) (i : ReadIdx) (hcZ : r.cZ = NumEnc.card (BooleanAnalysis.Cube (Tester.ROf B))) (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) (dflt : StepKey (F.toFamily hd) r.T r.q B (Fintype.card (α → α → Bool))) (encβ : (PreWalk (F.toFamily hd) r.T → α) → BooleanAnalysis.Cube B) : codeFn F pol r dflt encβ (pair (encGraph G) (List.replicate (((NumEnc.enc v * r.cD + NumEnc.enc x) * r.cZ + NumEnc.enc z) * 22 + NumEnc.enc i) true)) = List.replicate (codeOfRel (MultiTest.relOfCheck ((RegCSP.compose encβ ((G.preprocess (F.toFamily hd)).killedPow r.q r.T hq)).check (v, x) z) i)) true

The code algorithm computes the composed edge's constraint.

theorem Complexity.codeFn_eq' {F : FinBase} {pol : Polynomial ℕ} (r : Round) {α : Type} [Fintype α] [DecidableEq α] {B : ℕ} (hd : 1 < F.deg) (G : ConstraintGraph α) (hq : 0 < r.q) (hdeg : r.deg = (F.toFamily hd).degree) (hP : r.P = G.preDeg (F.toFamily hd)) (hC : r.C = Fintype.card (α → α → Bool)) (hZ : 0 < r.cZ) (p : ((G.preprocess (F.toFamily hd)).killedPow r.q r.T hq).Dart) (z : BooleanAnalysis.Cube (Tester.ROf B)) (i : ReadIdx) (hcZ : r.cZ = NumEnc.card (BooleanAnalysis.Cube (Tester.ROf B))) (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) (dflt : StepKey (F.toFamily hd) r.T r.q B (Fintype.card (α → α → Bool))) (encβ : (PreWalk (F.toFamily hd) r.T → α) → BooleanAnalysis.Cube B) : codeFn F pol r dflt encβ (pair (encGraph G) (List.replicate (((NumEnc.enc p.1 * r.cD + NumEnc.enc p.2) * r.cZ + NumEnc.enc z) * 22 + NumEnc.enc i) true)) = List.replicate (codeOfRel (MultiTest.relOfCheck ((RegCSP.compose encβ ((G.preprocess (F.toFamily hd)).killedPow r.q r.T hq)).check p z) i)) true

The code algorithm, with the dart given as one object.