Polynomial map for the linear GUV condenser

The source polynomial is repeatedly squared modulo a supplied polynomial. Evaluating every rth iterate gives the Parvaresh--Vardy neighbor map with exponent h = 2^r, omitting the seed coordinate. This is the map in Guruswami, Umans, and Vadhan (2009), Section 3.1, with the characteristic-power choice used by Cheraghchi (2010), Section 2.3.3, to obtain source linearity.

These definitions use Mathlib's noncomputable polynomial representation. They specify the algebraic map and its modular iteration. Condenser.Encoding and its correctness layer implement this map for the explicit binary fields; the expansion and flat lossless bounds are proved in separate condenser modules. No basis or irreducible polynomial is chosen in these general definitions. For a nonmonic modulus, Mathlib's %ₘ leaves the dividend unchanged; the degree guarantee requires monicity, and the eventual expansion proof also needs the construction's irreducibility hypotheses.

noncomputable def Algebraic.Cutwidth.Extractor.modularFrobenius {F : Type u_1} [CommRing F] (E : Polynomial F) : ℕ → Polynomial F → Polynomial F

Repeated modular squaring, starting with the reduced source polynomial. For monic E, every stored polynomial has degree less than E.degree.

Equations

• Algebraic.Cutwidth.Extractor.modularFrobenius E 0 x✝ = x✝ %ₘ E
• Algebraic.Cutwidth.Extractor.modularFrobenius E j.succ x✝ = Algebraic.Cutwidth.Extractor.modularFrobenius E j x✝ ^ 2 %ₘ E

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

The polynomial output coordinates of the GUV map for exponent 2^r. The seed y is not included in the output, matching the strong condenser convention. On source polynomials of degree less than a monic E, coordinate zero is f.eval y.

Equations

• Algebraic.Cutwidth.Extractor.polynomialCondenser E r m f y i = Polynomial.eval y (Algebraic.Cutwidth.Extractor.modularFrobenius E (r * ↑i) f)