A composed edge's record #
An edge of the composed graph carries three numbers: its two endpoints and the code of its constraint. The first endpoint is arithmetic in the edge number; the second is a position, laid out by kind — an encoding block, a linear table or a quadratic one — and the third is the code the tester's verdict names.
This module writes the position's layout out as an algorithm.
Main definitions #
Complexity.posBlk— a position's number, from its kind, block and cubeComplexity.tailBlk— an edge's first endpointComplexity.kindBlk,Complexity.blockBlk— which kind of block the second endpoint lies in, and which blockComplexity.headBlk— the second endpoint itselfComplexity.edgeRule,Complexity.stepFn— one edge's record, and the graph a round produces
Main results #
Complexity.posBlk_eq— it isRegCSP.posNumComplexity.posBlk_mem_FP— and it is computed in polynomial timeComplexity.tailBlk_eq,Complexity.tailBlk_mem_FP— likewise for the first endpoint
noncomputable def
Complexity.posBlk
(cardB cardN cardNN cardD : ℕ)
(cardV kind block cube : List Bool)
:
A position's number, from its kind, the block it lies in and the cube inside
that block. Kind 0 is an encoding block, kind 1 a dart's linear table, and
anything else a dart's quadratic table.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Complexity.posBlk_eq
(cardB cardN cardNN cardD k b c : ℕ)
(cardV kind block cube : List Bool)
(hk : kind.length = k)
(hb : block.length = b)
(hc : cube = List.replicate c true)
:
posBlk cardB cardN cardNN cardD cardV kind block cube = List.replicate (RegCSP.posNum cardV.length cardD cardB cardN cardNN k b c) true
The layout computes the position's number.
The first endpoint #
theorem
Complexity.tailBlk_eq
{α : Type}
[Fintype α]
[DecidableEq α]
(posF : ℕ)
(r : Round)
(G : ConstraintGraph α)
{w : List Bool}
{t zN : ℕ}
(hg : pairFst w = encGraph G)
(ht : testFn r w = List.replicate t true)
(hz : randFn r w = List.replicate zN true)
:
The first endpoint's algorithm computes it.
Which block the second endpoint lies in #
The kind of block a read lands in.
Equations
Instances For
theorem
Complexity.kindBlk_eq
{w : List Bool}
{i : ReadIdx}
(hi : readFn w = List.replicate (NumEnc.enc i) true)
:
The kind is the read's.
noncomputable def
Complexity.blockBlk
(F : FinBase)
(pol : Polynomial ℕ)
(r : Round)
(w : List Bool)
:
The block the second endpoint lies in: the dart's tail for the first input read, its head for the second, and the dart itself otherwise.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Complexity.blockBlk_eq
{β : Type}
[Fintype β]
[DecidableEq β]
[Nonempty β]
{R : RegCSP β}
[NumEnc R.graph.V]
[NumEnc R.graph.D]
(F : FinBase)
(pol : Polynomial ℕ)
(r : Round)
{w : List Bool}
(p : R.Dart)
(i : ReadIdx)
(hread : readFn w = List.replicate (NumEnc.enc i) true)
(hv : vertFn r w = List.replicate (NumEnc.enc p.1) true)
(ht : testFn r w = List.replicate (NumEnc.enc p) true)
(hrot :
pairFst (killedRotFn F pol r.deg r.P r.T r.q (killArg r w)) = List.replicate (NumEnc.enc (R.graph.rot p).1) true)
:
The block is the one the read asks for.
The second endpoint #
How many vertices the powered graph has: twice the input's edge count.
Equations
Instances For
theorem
Complexity.vertCount_eq
{α : Type}
[Fintype α]
[DecidableEq α]
(G : ConstraintGraph α)
{w : List Bool}
(hg : pairFst w = encGraph G)
:
noncomputable def
Complexity.headBlk
{α : Type}
[Fintype α]
[DecidableEq α]
(F : FinBase)
(pol : Polynomial ℕ)
(r : Round)
(cardB cardN cardNN : ℕ)
{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)
:
An edge's second endpoint.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Complexity.headBlk_mem_FP
{α : Type}
[Fintype α]
[DecidableEq α]
(F : FinBase)
(pol : Polynomial ℕ)
(r : Round)
(cardB cardN cardNN : ℕ)
{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)
:
theorem
Complexity.headBlk_eq
{α : Type}
[Fintype α]
[DecidableEq α]
(F : FinBase)
(pol : Polynomial ℕ)
(r : Round)
(cardB cardN cardNN : ℕ)
{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}
{V k b c : ℕ}
(hV : vertCount w = List.replicate V true)
(hk : kindBlk w = List.replicate k true)
(hb : blockBlk F pol r w = List.replicate b true)
(hc : cubeFn F pol r dflt encβ w = List.replicate c true)
:
headBlk F pol r cardB cardN cardNN dflt encβ w = List.replicate (RegCSP.posNum V r.cD cardB cardN cardNN k b c) true
The second endpoint's algorithm computes its number.
The label encoding, without the graph #
The encoding of a powered label, at a type that does not mention the graph.
Equations
- Complexity.encPre E T σ = Complexity.basisVec (Fin.cast ⋯ ((Fintype.equivFin (Complexity.PreWalk E T → Complexity.DinurAlpha)) σ))
Instances For
It is the encoding the round uses.
The round's constants #
The constants of a Dinur round at killing rate q, over the expander family
a finite base generates. The alphabet's constraint count and the tester's string
count are supplied, so that they carry the caller's own instances.
Equations
- Complexity.dinurRound F hd q C cZ = { deg := (F.toFamily hd).degree, P := 2 + 2 * (F.toFamily hd).degree, T := Complexity.powT Complexity.Dinur.K q, q := q, C := C, cZ := cZ }
Instances For
theorem
Complexity.dinurRound_P
(F : FinBase)
(hd : 1 < F.deg)
(q C cZ : ℕ)
(G : ConstraintGraph DinurAlpha)
:
@[simp]
@[simp]
@[simp]
The round's output #
noncomputable def
Complexity.edgeRule
{α : Type}
[Fintype α]
[DecidableEq α]
(F : FinBase)
(pol : Polynomial ℕ)
(r : Round)
(posF cardB cardN cardNN : ℕ)
{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)
:
One edge's record: its two endpoints and the code of its constraint.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Complexity.edgeRule_mem_FP
{α : Type}
[Fintype α]
[DecidableEq α]
(F : FinBase)
(pol : Polynomial ℕ)
(r : Round)
(posF cardB cardN cardNN : ℕ)
{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)
:
noncomputable def
Complexity.stepFn
{α : Type}
[Fintype α]
[DecidableEq α]
(F : FinBase)
(pol : Polynomial ℕ)
(r : Round)
(vertF edgeF posF cardB cardN cardNN : ℕ)
{E : ExpanderFamily}
{B : ℕ}
(dflt : StepKey E r.T r.q B (Fintype.card (α → α → Bool)))
(encβ : (PreWalk E r.T → α) → BooleanAnalysis.Cube B)
:
The graph a round produces, from the graph it is given.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Complexity.countBlk_eq
{α : Type}
[Fintype α]
[DecidableEq α]
(G : ConstraintGraph α)
(c : ℕ)
:
A count block is a constant multiple of the input's edge count.
theorem
Complexity.stepFn_mem_FP
{α : Type}
[Fintype α]
[DecidableEq α]
(F : FinBase)
(pol : Polynomial ℕ)
(r : Round)
(vertF edgeF posF cardB cardN cardNN : ℕ)
{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)
:
theorem
Complexity.stepFn_eq
(F : FinBase)
(pol : Polynomial ℕ)
(hd : 1 < F.deg)
(G : ConstraintGraph DinurAlpha)
(r : Round)
(hq : 0 < r.q)
(vertF edgeF posF cardB cardN cardNN : ℕ)
(hrD : r.cD = NumEnc.card ((G.preprocess (F.toFamily hd)).killedPow r.q r.T hq).graph.D)
(hrZ : r.cZ = 2 ^ Tester.ROf (Dinur.bits (F.toFamily hd) r.T))
(hdeg : r.deg = (F.toFamily hd).degree)
(hP : r.P = G.preDeg (F.toFamily hd))
(hC : r.C = Fintype.card (DinurAlpha → DinurAlpha → Bool))
(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)
(hvertF :
(RegCSP.compose (Dinur.enc (F.toFamily hd) G r.T)
((G.preprocess (F.toFamily hd)).killedPow r.q r.T hq)).toGraph.numVerts = vertF * G.numEdges)
(hedgeF :
(RegCSP.compose (Dinur.enc (F.toFamily hd) G r.T)
((G.preprocess (F.toFamily hd)).killedPow r.q r.T hq)).toGraph.numEdges = edgeF * G.numEdges)
(hcardB : cardB = NumEnc.card (BooleanAnalysis.Cube (Dinur.bits (F.toFamily hd) r.T)))
(hcardN : cardN = NumEnc.card (BooleanAnalysis.Cube (Tester.nOf (Dinur.bits (F.toFamily hd) r.T))))
(hcardNN :
cardNN = NumEnc.card
(BooleanAnalysis.Cube
(Tester.nOf (Dinur.bits (F.toFamily hd) r.T) * Tester.nOf (Dinur.bits (F.toFamily hd) r.T))))
(hposF : Fintype.card ((G.preprocess (F.toFamily hd)).killedPow r.q r.T hq).Pos = G.numEdges * posF)
(dflt :
StepKey (F.toFamily hd) r.T r.q (Dinur.bits (F.toFamily hd) r.T) (Fintype.card (DinurAlpha → DinurAlpha → Bool)))
:
One round of amplification, computed. The algorithm's output is the graph the round produces.