The seeded polynomial neighbor graph

The Guruswami--Umans--Vadhan graph retains the seed and evaluates the first m source powers with exponents h^i, reduced modulo a supplied polynomial. The graph is defined for arbitrary h; the characteristic-power choice gives the linear condenser map. These semantic definitions do not choose a field, choose a modulus, or supply an encoded evaluator.

noncomputable def Algebraic.Cutwidth.Extractor.polynomialNeighbor {F : Type u_1} [CommRing F] (E : Polynomial F) (h m : ℕ) (f : Polynomial F) (y : F) : F × (Fin m → F)

A seeded neighbor in the polynomial graph of GUV (2009), Section 3.1.

Equations

• Algebraic.Cutwidth.Extractor.polynomialNeighbor E h m f y = (y, fun (i : Fin m) => Polynomial.eval y (f ^ h ^ ↑i %ₘ E))

noncomputable def Algebraic.Cutwidth.Extractor.polynomialNeighborSet {F : Type u_1} [CommRing F] [Fintype F] (E : Polynomial F) (h m : ℕ) (P : Finset (Polynomial F)) : Finset (F × (Fin m → F))

All seeded polynomial neighbors reached from a finite source set.

Equations

• Algebraic.Cutwidth.Extractor.polynomialNeighborSet E h m P = P.biUnion fun (f : Polynomial F) => Finset.image (Algebraic.Cutwidth.Extractor.polynomialNeighbor E h m f) Finset.univ