Base-digit reconstruction and exact monomial substitution

The division algorithm reconstructs each integer below h^m from exactly m digits. Substituting powers with weights h^i therefore recovers the distinct powers indexed by the original Fin K, with degree strictly below K even when K is smaller than h^m.

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

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

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

theorem Algebraic.Cutwidth.Extractor.Internal.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

theorem Algebraic.Cutwidth.Extractor.Internal.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)

theorem Algebraic.Cutwidth.Extractor.Internal.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

theorem Algebraic.Cutwidth.Extractor.Internal.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

theorem Algebraic.Cutwidth.Extractor.Internal.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

theorem Algebraic.Cutwidth.Extractor.Internal.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