Recursive Karatsuba on CPolynomial R

This file extends the one-level Karatsuba step of Karatsuba.lean to the full recursion. Where karatsubaMul takes the four already-split halves as explicit arguments, karatsubaRec is a binary multiply CPolynomial R → CPolynomial R → CPolynomial R that splits each input itself, recurses on the three Karatsuba subproducts, and recombines.

Termination via fuel

Rather than a well-founded recursion on a decreasing degree measure (which would require carrying split-size proofs through every recursive call), karatsubaRec takes an explicit fuel : ℕ and bottoms out in the schoolbook product p * q at fuel = 0. This is the standard structurally-recursive presentation and is sufficient for the algebraic-correctness statement, which is the point of the CoqEAL refinement: for every fuel value, karatsubaRec fuel p q denotes the true product p · q.

The split

The high part hiPart k p drops the k lowest coefficients (divX iterated k times); the low part is then defined as loPart k p := p − Xᵏ · hiPart k p. With this definition the split–recompose identity

  loPart k p + Xᵏ · hiPart k p = p

is a one-line commutative-ring fact ((p − Xᵏ·h) + Xᵏ·h = p), needing no coefficient reasoning and no appeal to a CompPoly division-with-remainder lemma (CompPoly only provides divByMonic/modByMonic over a Field, whereas this development is over a CommRing). The split point k does not affect correctness — only performance — so karatsubaRec is correct for any choice; we pick the balanced ⌊max(deg p, deg q)/2⌋ + 1.

Correctness

karatsubaRec_eq : (karatsubaRec fuel p q).toPoly = p.toPoly * q.toPoly is by induction on fuel. The base case is toPoly_mul. The step case rewrites the three recursive subproducts to true products via the induction hypothesis, then discharges the recombination — recompose both inputs and expand — by transferring across CPolynomial.ringEquiv to Mathlib Polynomial R, exactly as karatsubaMul_eq does for the one-level step.

Registry entry

karatsubaRec_repr is tagged @[transfer] in the refine direction (p * q ↦ karatsubaRec fuel p q), registering recursive Karatsuba as a refinement of the schoolbook product, mirroring karatsuba_repr for the one-level step. Because the recursion carries a fuel argument that appears only on the right, the rewrite is applied with the fuel supplied (rw [karatsubaRec_repr fuel]) rather than via bare repr_transfer.

noncomputable def Transfer.Examples.CoqEAL.Karatsuba.hiPart {R : Type u_1} [CommRing R] (k : ℕ) (p : CompPoly.CPolynomial R) : CompPoly.CPolynomial R

High part of a split at degree k. Drops the k lowest coefficients by iterating divX (pseudo-division by X) k times.

Equations

• Transfer.Examples.CoqEAL.Karatsuba.hiPart k p = CompPoly.CPolynomial.divX^[k] p

noncomputable def Transfer.Examples.CoqEAL.Karatsuba.loPart {R : Type u_1} [CommRing R] [BEq R] [LawfulBEq R] [Nontrivial R] (k : ℕ) (p : CompPoly.CPolynomial R) : CompPoly.CPolynomial R

Low part of a split at degree k, defined so that recomposition is a ring identity: p = loPart k p + Xᵏ · hiPart k p.

Equations

• Transfer.Examples.CoqEAL.Karatsuba.loPart k p = p - CompPoly.CPolynomial.X ^ k * Transfer.Examples.CoqEAL.Karatsuba.hiPart k p

theorem Transfer.Examples.CoqEAL.Karatsuba.loPart_add_hiPart {R : Type u_1} [CommRing R] [BEq R] [LawfulBEq R] [Nontrivial R] (k : ℕ) (p : CompPoly.CPolynomial R) : loPart k p + CompPoly.CPolynomial.X ^ k * hiPart k p = p

Split–recompose identity. Recomposing the low and high parts at any degree k returns the original polynomial. By construction loPart is the complement of Xᵏ · hiPart, so this is a commutative-ring fact — no coefficient reasoning required.

noncomputable def Transfer.Examples.CoqEAL.Karatsuba.splitPoint {R : Type u_1} [CommRing R] (p q : CompPoly.CPolynomial R) : ℕ

A reasonable balanced split point: half the larger degree, plus one (so a nonconstant input is split nontrivially). Correctness is independent of this choice.

Equations

• Transfer.Examples.CoqEAL.Karatsuba.splitPoint p q = max p.natDegree q.natDegree / 2 + 1

noncomputable def Transfer.Examples.CoqEAL.Karatsuba.karatsubaRec {R : Type u_1} [CommRing R] [BEq R] [LawfulBEq R] [Nontrivial R] : ℕ → CompPoly.CPolynomial R → CompPoly.CPolynomial R → CompPoly.CPolynomial R

Recursive Karatsuba multiplication with explicit fuel.

At fuel = 0 it is the schoolbook product. Otherwise it splits both inputs at splitPoint p q, recursively forms the three Karatsuba subproducts z₀ = plo·qlo, z₂ = phi·qhi, (plo+phi)·(qlo+qhi), and recombines as z₀ + Xᵏ·z₁ + X²ᵏ·z₂ with z₁ = (plo+phi)(qlo+qhi) − z₀ − z₂.

Equations

• One or more equations did not get rendered due to their size.
• Transfer.Examples.CoqEAL.Karatsuba.karatsubaRec 0 x✝¹ x✝ = x✝¹ * x✝

theorem Transfer.Examples.CoqEAL.Karatsuba.karatsubaRec_eq {R : Type u_1} [CommRing R] [BEq R] [LawfulBEq R] [Nontrivial R] (fuel : ℕ) (p q : CompPoly.CPolynomial R) : (karatsubaRec fuel p q).toPoly = p.toPoly * q.toPoly

Correctness of recursive Karatsuba. For every fuel value, karatsubaRec fuel p q denotes the true product p · q.

Induction on fuel: the base case is toPoly_mul; the step case rewrites the three recursive subproducts via the induction hypothesis and then discharges the recombination — recompose both inputs (loPart_add_hiPart) and expand — by transferring across CPolynomial.ringEquiv to Mathlib Polynomial R, where it is a ring identity.

theorem Transfer.Examples.CoqEAL.Karatsuba.karatsubaRec_repr {R : Type u_1} [CommRing R] [BEq R] [LawfulBEq R] [Nontrivial R] (fuel : ℕ) (p q : CompPoly.CPolynomial R) : p * q = karatsubaRec fuel p q

Registry entry (refinement direction). Tagged @[transfer] so that repr_transfer rewrites a plain CPolynomial product p · q to its recursive-Karatsuba form karatsubaRec fuel p q. Mirrors karatsuba_repr for the one-level step.