Implement generic fast polynomial multiplication

[kim-em]

Summary

• add proof-carrying schoolbook and Karatsuba multiplication plans
• implement genuine three-product recursion, specialized squaring, and skew-operand blocking
• add positive-length cyclic and negacyclic reference folds with checked zero-length forms
• add guarded polynomial/truncated-series reversal bridges
• add always-run conformance coverage for cutoff, odd split, skew, slice, reversal, cyclic, and negacyclic cases
• register Mathlib-free scientific benchmarks for schoolbook, balanced Karatsuba, Karatsuba squaring, and 64:1 skew multiplication
• correct three unsound signatures/statements discovered while implementing the merged SPEC

Spec corrections

• zero-extended reversal must guard indices past f.size
• MulPlan/DivPlan/GcdStep must derive the coefficient zero from the ring rather than accept an unrelated Zero
• DivPlan.ofMonic also needs q ≠ 0, since the zero polynomial is monic in a degenerate commutative ring

Verification

• lake build HexPolyFast hexpolyfast_bench conformance/HexPolyFast/Conformance.lean
• .lake/build/bin/hexpolyfast_bench list
• .lake/build/bin/hexpolyfast_bench verify
• python3 scripts/ci/check_benches_mathlib_free.py
• python3 scripts/bench/check_factor_sweep_freshness.py
• python3 scripts/check_dag.py
• source header and line-count lints
• git diff --check

This PR is the generic multiplication slice. It intentionally does not add semantic wrappers for later milestones: reciprocal/division must use planned clipped products, half-gcd must contain real grouped recursion, and multipoint evaluation must use the reusable remainder tree before those APIs land.