The composed graph, in numbers

The binary graph a family of tests produces has one vertex per position and per (test, random string), and one edge per (test, random string, read). Both are numbered by NumEnc, so an edge index splits by division and remainder into the test, the string and the read, and the two endpoints are read off from there.

Main results

• Complexity.MultiTest.enc_edgeOf — the edge a number names carries that number
• Complexity.MultiTest.enc_edge — how an edge's number splits
• Complexity.MultiTest.val_tail_toGraph, val_head_toGraph — the endpoints
• Complexity.RegCSP.enc_pos_inl, enc_pos_lin, enc_pos_quad — the three kinds of position of the composed proof

theorem Complexity.MultiTest.enc_edgeOf {Pos E Q : Type} (M : MultiTest Pos E Q) [Fintype E] [Fintype Q] [NumEnc E] [NumEnc Q] (k : Fin (Fintype.card M.Edge)) : NumEnc.enc (M.edgeOf k) = ↑k

theorem Complexity.MultiTest.val_vertIdx {Pos E Q : Type} (M : MultiTest Pos E Q) [Fintype Pos] [Fintype E] [NumEnc Pos] [NumEnc E] (v : M.Vert) : ↑(M.vertIdx v) = NumEnc.enc v

theorem Complexity.MultiTest.enc_edge {Pos E Q : Type} (M : MultiTest Pos E Q) [NumEnc E] [NumEnc Q] (x : M.Edge) : NumEnc.enc x = NumEnc.enc x.1 * (NumEnc.card (BooleanAnalysis.Cube M.R) * NumEnc.card Q) + (NumEnc.enc x.2.1 * NumEnc.card Q + NumEnc.enc x.2.2)

How an edge's number splits: the test, then the random string, then the read.

theorem Complexity.MultiTest.val_tail_toGraph {Pos E Q : Type} (M : MultiTest Pos E Q) [Fintype Pos] [Fintype E] [Fintype Q] [NumEnc Pos] [NumEnc E] [NumEnc Q] (k : Fin (Fintype.card M.Edge)) : ↑(M.toGraph.tail k) = NumEnc.card Pos + (NumEnc.enc (M.edgeOf k).1 * NumEnc.card (BooleanAnalysis.Cube M.R) + NumEnc.enc (M.edgeOf k).2.1)

The first endpoint: the test vertex, numbered after all the positions.

theorem Complexity.MultiTest.val_head_toGraph {Pos E Q : Type} (M : MultiTest Pos E Q) [Fintype Pos] [Fintype E] [Fintype Q] [NumEnc Pos] [NumEnc E] [NumEnc Q] (k : Fin (Fintype.card M.Edge)) : ↑(M.toGraph.head k) = NumEnc.enc (M.pos (M.edgeOf k).1 (M.edgeOf k).2.1 (M.edgeOf k).2.2)

The second endpoint: the position the read asks for.

The composed proof's positions

theorem Complexity.RegCSP.enc_pos_inl {β : Type} (R : RegCSP β) [NumEnc R.graph.V] [NumEnc R.graph.D] {B : ℕ} (v : R.graph.V) (y : BooleanAnalysis.Cube B) : NumEnc.enc (Sum.inl (v, y)) = NumEnc.enc v * NumEnc.card (BooleanAnalysis.Cube B) + NumEnc.enc y

A position in a vertex's encoding block.

theorem Complexity.RegCSP.enc_pos_lin {β : Type} (R : RegCSP β) [NumEnc R.graph.V] [NumEnc R.graph.D] {B : ℕ} (p : R.Dart) (y : BooleanAnalysis.Cube (Tester.nOf B)) : NumEnc.enc (Sum.inr (Sum.inl (p, y))) = NumEnc.card R.graph.V * NumEnc.card (BooleanAnalysis.Cube B) + (NumEnc.enc p * NumEnc.card (BooleanAnalysis.Cube (Tester.nOf B)) + NumEnc.enc y)

A position in a dart's linear table, after all the encoding blocks.

theorem Complexity.RegCSP.enc_pos_quad {β : Type} (R : RegCSP β) [NumEnc R.graph.V] [NumEnc R.graph.D] {B : ℕ} (p : R.Dart) (y : BooleanAnalysis.Cube (Tester.nOf B * Tester.nOf B)) : NumEnc.enc (Sum.inr (Sum.inr (p, y))) = NumEnc.card R.graph.V * NumEnc.card (BooleanAnalysis.Cube B) + (NumEnc.card R.Dart * NumEnc.card (BooleanAnalysis.Cube (Tester.nOf B)) + (NumEnc.enc p * NumEnc.card (BooleanAnalysis.Cube (Tester.nOf B * Tester.nOf B)) + NumEnc.enc y))

A position in a dart's quadratic table, after the linear ones.

theorem Complexity.RegCSP.enc_dart {β : Type} (R : RegCSP β) [NumEnc R.graph.V] [NumEnc R.graph.D] (p : R.Dart) : NumEnc.enc p = NumEnc.enc p.1 * NumEnc.card R.graph.D + NumEnc.enc p.2

A dart's number splits into its vertex and its label.