CoqEAL toomcook — the evaluate–multiply–interpolate core

Toom-Cook multiplication (which Karatsuba is the two-way case of) multiplies polynomials by splitting each into parts, evaluating at enough points, multiplying the values pointwise, and interpolating the product back. The soundness of the evaluate-multiply step is that evaluation is a ring homomorphism: (p * q)(t) = p(t) · q(t). Interpolation — the unique polynomial of bounded degree through the sampled points — recovers p * q, so the pointwise products at enough points determine the product exactly. This file proves the evaluate–multiply identity and the three-point case for linear polynomials; the general algorithm is not formalized here.

theorem Transfer.Examples.CoqEAL.ToomCook.eval_product (p q : Polynomial ℤ) (t : ℤ) : Polynomial.eval t (p * q) = Polynomial.eval t p * Polynomial.eval t q

The evaluate–multiply core of Toom-Cook. Evaluation is multiplicative, so a product's value at a point is the product of the values — what lets Toom-Cook multiply pointwise after sampling.