One round, uniformly

AlgEdge.stepFn_eq computes a round of amplification for a graph whose sizes match the constants it is given. Iterating a round needs more: one function that is right for every graph. This module supplies the constants that do not depend on the graph — the walk length, the degree, the tester's counts — and specialises the round to them.

The one fact that makes this possible is that the encoding a round composes with does not depend on the graph either: the walks it is defined on are PreWalk E T, whose type is fixed by the expander family alone.

Main definitions

• Complexity.roundOf — the round's constants
• Complexity.roundFn — the round, as one FP function

Main results

• Complexity.roundFn_eq — it computes a round of amplification, for every graph

The constants

noncomputable def Complexity.qOf (F : FinBase) (hd : 1 < F.deg) : ℕ

The killing rate a round uses.

Equations

• Complexity.qOf F hd = Complexity.Dinur.q₀ (F.toFamily hd)

theorem Complexity.qOf_pos (F : FinBase) (hd : 1 < F.deg) : 0 < qOf F hd

noncomputable def Complexity.walkLen (F : FinBase) (hd : 1 < F.deg) : ℕ

The walk length a round uses.

Equations

• Complexity.walkLen F hd = Complexity.powT Complexity.Dinur.K (Complexity.qOf F hd)

noncomputable def Complexity.cZOf (F : FinBase) (hd : 1 < F.deg) : ℕ

How many random strings the tester has.

Equations

• Complexity.cZOf F hd = 2 ^ Complexity.Tester.ROf (Complexity.Dinur.bits (F.toFamily hd) (Complexity.walkLen F hd))

noncomputable def Complexity.cRel : ℕ

How many constraints the alphabet has.

Equations

• Complexity.cRel = Fintype.card (Complexity.DinurAlpha → Complexity.DinurAlpha → Bool)

theorem Complexity.cRel_eq : cRel = Fintype.card (DinurAlpha → DinurAlpha → Bool)

theorem Complexity.cRel_pos : 0 < cRel

noncomputable def Complexity.roundOf (F : FinBase) (hd : 1 < F.deg) : Round

The round's constants.

Equations

• Complexity.roundOf F hd = Complexity.dinurRound F hd (Complexity.qOf F hd) Complexity.cRel (Complexity.cZOf F hd)

theorem Complexity.roundOf_q (F : FinBase) (hd : 1 < F.deg) : (roundOf F hd).q = qOf F hd

theorem Complexity.roundOf_T (F : FinBase) (hd : 1 < F.deg) : (roundOf F hd).T = walkLen F hd

theorem Complexity.roundOf_C (F : FinBase) (hd : 1 < F.deg) : (roundOf F hd).C = cRel

theorem Complexity.roundOf_cZ (F : FinBase) (hd : 1 < F.deg) : (roundOf F hd).cZ = cZOf F hd

theorem Complexity.roundOf_deg (F : FinBase) (hd : 1 < F.deg) : (roundOf F hd).deg = (F.toFamily hd).degree

theorem Complexity.roundOf_P (F : FinBase) (hd : 1 < F.deg) (G : ConstraintGraph DinurAlpha) : (roundOf F hd).P = G.preDeg (F.toFamily hd)

theorem Complexity.roundOf_cQ (F : FinBase) (hd : 1 < F.deg) : (roundOf F hd).cQ = qOf F hd ^ walkLen F hd

noncomputable def Complexity.dfltKey (F : FinBase) (hd : 1 < F.deg) : StepKey (F.toFamily hd) (roundOf F hd).T (roundOf F hd).q (Dinur.bits (F.toFamily hd) (roundOf F hd).T) (Fintype.card (DinurAlpha → DinurAlpha → Bool))

A key to fall back on, for arguments that name no edge.

Equations

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

noncomputable def Complexity.encOf (F : FinBase) (hd : 1 < F.deg) : (PreWalk (F.toFamily hd) (roundOf F hd).T → DinurAlpha) → BooleanAnalysis.Cube (Dinur.bits (F.toFamily hd) (roundOf F hd).T)

The encoding a round composes with. It is written at a graph, but does not depend on it: the walks are those of the expander family.

Equations

• Complexity.encOf F hd = Complexity.Dinur.enc (F.toFamily hd) (Complexity.baseCSP []) (Complexity.roundOf F hd).T

theorem Complexity.encOf_eq (F : FinBase) (hd : 1 < F.deg) (G : ConstraintGraph DinurAlpha) : encOf F hd = Dinur.enc (F.toFamily hd) G (roundOf F hd).T

The round

noncomputable def Complexity.roundFn (F : FinBase) (hd : 1 < F.deg) : List Bool → List Bool

A round of amplification, as one function.

Equations

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

theorem Complexity.roundOf_cQ_pos (F : FinBase) (hd : 1 < F.deg) : 0 < (roundOf F hd).cQ

theorem Complexity.roundOf_cD_pos (F : FinBase) (hd : 1 < F.deg) : 0 < (roundOf F hd).cD

theorem Complexity.roundOf_cZ_pos (F : FinBase) (hd : 1 < F.deg) : 0 < (roundOf F hd).cZ

theorem Complexity.roundOf_C_pos (F : FinBase) (hd : 1 < F.deg) : 0 < (roundOf F hd).C

theorem Complexity.roundFn_mem_FP (F : FinBase) (hd : 1 < F.deg) : roundFn F hd ∈ FP

theorem Complexity.roundFn_eq (F : FinBase) (hd : 1 < F.deg) (G : ConstraintGraph DinurAlpha) : roundFn F hd (encGraph G) = encGraph (Dinur.step (F.toFamily hd) (qOf F hd) ⋯ G)

The round computes a round of amplification, for every graph.