Exact substitution for the first GUV interpolation monomials

For every j < K ≤ h^m, the first m base-h digits reconstruct j. Their sum is at most m * (h - 1). Consequently substituting Z^(h^i) into the associated monomial gives exactly Z^j.

For a coefficient array indexed by Fin K, the substituted polynomial has degree less than K and is nonzero precisely when some coefficient is nonzero. The coefficient ring can be a quotient by the extension modulus, so this is the nonvanishing step used after reduction of the interpolation coefficients. No field or characteristic assumption is required by this layer.

This is the base-h monomial indexing in Guruswami, Umans, and Vadhan, Unbalanced Expanders and Randomness Extractors from Parvaresh--Vardy Codes (2009), Section 3.1, proof of Theorem 3.3: https://salil.seas.harvard.edu/sites/g/files/omnuum4266/files/salil/files/acm2009.pdf. The bounds retain the given K, including when K < h^m.

theorem Algebraic.Cutwidth.Extractor.monomialDigit_lt {h j m : ℕ} (positive : 0 < h) (i : Fin m) : monomialDigit h j i < h

Each digit is below a positive base.

theorem Algebraic.Cutwidth.Extractor.sum_monomialDigit_mul_pow {h j m : ℕ} (bound : j < h ^ m) : ∑ i : Fin m, monomialDigit h j i * h ^ ↑i = j

The first m digits reconstruct every integer below h^m.

theorem Algebraic.Cutwidth.Extractor.sum_monomialDigit_le {h j m : ℕ} (positive : 0 < h) : ∑ i : Fin m, monomialDigit h j i ≤ m * (h - 1)

The total exponent of every digit monomial is at most m * (h - 1).

theorem Algebraic.Cutwidth.Extractor.digitMonomial_pow {R : Type u_1} [CommMonoid R] {h j m : ℕ} (bound : j < h ^ m) (u : R) : (digitMonomial h j fun (i : Fin m) => u ^ h ^ ↑i) = u ^ j

Substituting powers with weights h^i recovers exactly the power indexed by the encoded integer. This holds in any commutative monoid.

theorem Algebraic.Cutwidth.Extractor.digitMonomial_substitution {R : Type u_1} [CommSemiring R] {h K m : ℕ} (bound : K ≤ h ^ m) (a : Fin K → R) : (∑ j : Fin K, Polynomial.C (a j) * digitMonomial h ↑j fun (i : Fin m) => Polynomial.X ^ h ^ ↑i) = ∑ j : Fin K, (Polynomial.monomial ↑j) (a j)

Substitution in the first K monomials preserves their distinct indices as univariate powers, without replacing K by h^m.

theorem Algebraic.Cutwidth.Extractor.fin_monomial_sum_eq_ofFn {R : Type u_1} [Semiring R] [DecidableEq R] {K : ℕ} (a : Fin K → R) : ∑ j : Fin K, (Polynomial.monomial ↑j) (a j) = (Polynomial.ofFn K) a

The resulting monomial sum is the polynomial with coefficient array a.

theorem Algebraic.Cutwidth.Extractor.fin_monomial_sum_coeff {R : Type u_1} [Semiring R] {K : ℕ} (a : Fin K → R) (j : Fin K) : (∑ i : Fin K, (Polynomial.monomial ↑i) (a i)).coeff ↑j = a j

Each coefficient survives at its own exponent index.

theorem Algebraic.Cutwidth.Extractor.fin_monomial_sum_degree_lt {R : Type u_1} [Semiring R] {K : ℕ} (a : Fin K → R) : (∑ j : Fin K, (Polynomial.monomial ↑j) (a j)).degree < ↑K

The first K powers give degree strictly below K, including K = 0.

theorem Algebraic.Cutwidth.Extractor.fin_monomial_sum_ne_zero_iff {R : Type u_1} [Semiring R] {K : ℕ} (a : Fin K → R) : ∑ j : Fin K, (Polynomial.monomial ↑j) (a j) ≠ 0 ↔ ∃ (j : Fin K), a j ≠ 0

A coefficient surviving reduction makes the substituted polynomial nonzero.