Amplifying, logarithmically many times

AlgRound computes one round. Dinur's theorem runs logarithmically many, so this module iterates that function and bounds the size of what it writes: each round multiplies the edge count by a constant, so after n rounds the graph is edgeFactor ^ n times as large, and the ruler keeps n logarithmic.

Main definitions

• Complexity.gapFn — the amplified graph, as a string

Main results

• Complexity.numEdges_iterStep — a round's edge count, exactly
• Complexity.length_encGraph_iterStep_le — the size of what is written
• Complexity.gapFn_eq — it writes the amplifier's iterate

The sizes of an iterate

theorem Complexity.numEdges_iterStep (F : FinBase) (hd : 1 < F.deg) (G : ConstraintGraph DinurAlpha) (n : ℕ) : ((Dinur.step (F.toFamily hd) (qOf F hd) ⋯)^[n] G).numEdges = Dinur.edgeFactor (F.toFamily hd) (qOf F hd) ^ n * G.numEdges

theorem Complexity.one_le_edgeFactor (F : FinBase) (hd : 1 < F.deg) : 1 ≤ Dinur.edgeFactor (F.toFamily hd) (qOf F hd)

theorem Complexity.numVerts_iterStep_le (F : FinBase) (hd : 1 < F.deg) (G : ConstraintGraph DinurAlpha) (n : ℕ) : ((Dinur.step (F.toFamily hd) (qOf F hd) ⋯)^[n] G).numVerts ≤ G.numVerts + Dinur.vertFactor (F.toFamily hd) (qOf F hd) * (Dinur.edgeFactor (F.toFamily hd) (qOf F hd) ^ n * G.numEdges)

theorem Complexity.size_mono {V V' E E' C : ℕ} (h : V' ≤ V) (hE : E' ≤ E) : 2 * V' + 4 + E' * (8 * V' + 4 * C + 10) ≤ 2 * V + 4 + E * (8 * V + 4 * C + 10)

theorem Complexity.length_encGraph_iterStep_le (F : FinBase) (hd : 1 < F.deg) (G : ConstraintGraph DinurAlpha) (n : ℕ) : (encGraph ((Dinur.step (F.toFamily hd) (qOf F hd) ⋯)^[n] G)).length ≤ 2 * (G.numVerts + Dinur.vertFactor (F.toFamily hd) (qOf F hd) * (Dinur.edgeFactor (F.toFamily hd) (qOf F hd) ^ n * G.numEdges)) + 4 + Dinur.edgeFactor (F.toFamily hd) (qOf F hd) ^ n * G.numEdges * (8 * (G.numVerts + Dinur.vertFactor (F.toFamily hd) (qOf F hd) * (Dinur.edgeFactor (F.toFamily hd) (qOf F hd) ^ n * G.numEdges)) + 4 * Fintype.card (DinurAlpha → DinurAlpha → Bool) + 10)

The size of what a round writes.

theorem Complexity.length_encGraph_iterStep_le' (F : FinBase) (hd : 1 < F.deg) (G : ConstraintGraph DinurAlpha) (n r B : ℕ) (hn : n ≤ r) (hB : Dinur.edgeFactor (F.toFamily hd) (qOf F hd) ^ r ≤ B) : (encGraph ((Dinur.step (F.toFamily hd) (qOf F hd) ⋯)^[n] G)).length ≤ 2 * (G.numVerts + Dinur.vertFactor (F.toFamily hd) (qOf F hd) * (B * G.numEdges)) + 4 + B * G.numEdges * (8 * (G.numVerts + Dinur.vertFactor (F.toFamily hd) (qOf F hd) * (B * G.numEdges)) + 4 * Fintype.card (DinurAlpha → DinurAlpha → Bool) + 10)

The size of what a round writes, in terms of a bound on the growth factor, so that one bound serves every round of the iteration.

theorem Complexity.transform_amplifier (F : FinBase) (hd : 1 < F.deg) : (Dinur.amplifier (F.toFamily hd)).transform = Dinur.step (F.toFamily hd) (qOf F hd) ⋯

The amplifier's round is the round the algorithm computes.

theorem Complexity.iter_amplifier (F : FinBase) (hd : 1 < F.deg) (G : ConstraintGraph DinurAlpha) (k : ℕ) : (Dinur.amplifier (F.toFamily hd)).iter k G = (Dinur.step (F.toFamily hd) (qOf F hd) ⋯)^[k] G

So the amplifier's iterate is the algorithm's.

theorem Complexity.length_encGraph_iterStep_le'' (F : FinBase) (hd : 1 < F.deg) (G : ConstraintGraph DinurAlpha) (n r B V m : ℕ) (hn : n ≤ r) (hB : Dinur.edgeFactor (F.toFamily hd) (qOf F hd) ^ r ≤ B) (hV : G.numVerts ≤ V) (hm : G.numEdges ≤ m) : (encGraph ((Dinur.step (F.toFamily hd) (qOf F hd) ⋯)^[n] G)).length ≤ 2 * (V + Dinur.vertFactor (F.toFamily hd) (qOf F hd) * (B * m)) + 4 + B * m * (8 * (V + Dinur.vertFactor (F.toFamily hd) (qOf F hd) * (B * m)) + 4 * Fintype.card (DinurAlpha → DinurAlpha → Bool) + 10)

The size of what a round writes, from numeric bounds alone: a caller supplies bounds on the graph it starts from and on the growth factor.

The iteration

noncomputable def Complexity.gapFn (F : FinBase) (hd : 1 < F.deg) (init ruler : List Bool → List Bool) (z : List Bool) : List Bool

The amplified graph, as a string: as many rounds as the ruler is long.

Equations

• Complexity.gapFn F hd init ruler z = (Complexity.roundFn F hd)^[(ruler z).length] (init z)

theorem Complexity.gapFn_eq (F : FinBase) (hd : 1 < F.deg) {init ruler : List Bool → List Bool} {z : List Bool} {G : ConstraintGraph DinurAlpha} (h : init z = encGraph G) : gapFn F hd init ruler z = encGraph ((Dinur.step (F.toFamily hd) (qOf F hd) ⋯)^[(ruler z).length] G)

What it writes: the amplifier's iterate on whatever graph the start writes.

theorem Complexity.gapFn_mem_FP (F : FinBase) (hd : 1 < F.deg) {init ruler width : List Bool → List Bool} (hinit : init ∈ FP) (hruler : ruler ∈ FP) (hwidth : width ∈ FP) (hinitG : ∀ (z : List Bool), ∃ (G : ConstraintGraph DinurAlpha), init z = encGraph G) (hbound : ∀ (z : List Bool) (G : ConstraintGraph DinurAlpha), init z = encGraph G → ∀ n ≤ (ruler z).length, (encGraph ((Dinur.step (F.toFamily hd) (qOf F hd) ⋯)^[n] G)).length ≤ (width z).length) : gapFn F hd init ruler ∈ FP

And writing it is polynomial-time.