perf(modarith): lazy-reduction ZMod64 matrix multiply kernel (remainder of #8639, contingent on #8647)

[kim-em]

Tracks the surviving deliverable of #8639 (perf(modarith): Barrett-context + lazy-reduction convolution kernels for FpPoly/matrix over ZMod64), which is being closed because its primary half was executed with a measured negative result:

• feat(polyfp): proven packed lazy-reduction FpPoly multiply (dormant) #8644 (feat(polyfp): proven packed lazy-reduction FpPoly multiply (dormant)) built the FpPoly lazy-reduction convolution kernel (lean_hex_fp_convolve, 128-bit accumulation, one reduction per output coefficient, value-correspondence proof). It is ~7x faster on a raw large-by-large multiply but flat (~1.00x) end-to-end on hexpolyfp_bench and the BZ factor sweep: the finite-field polynomial workloads are reduction-bound (modByMonic), not multiply-bound. It landed as dormant, tested infrastructure.
• doc(polyfp): record that packed modByMonic is not the FpPoly lever #8646 (doc(polyfp): record that packed modByMonic is not the FpPoly lever) then disproved the follow-up hypothesis that the reduction side would pay: packed and native-extern modByMonic are flat to ~3% slower.

Surviving piece: ZMod64 matrix multiply. The O(n^3) dot-product accumulation in matrix multiply / row reduction still reduces per term. With p < 2^31 (from #8638) each product is < 2^62, so a 128-bit accumulate-and-reduce (or Barrett-context) kernel reducing once per output entry is well-defined. Wiring would be @[csimp]/extern-equal to the reference multiply with a value-correspondence proof, byte-identical outputs, conformance unchanged.

Precondition: do not build this until #8647 reports the remaining cost shares. Matrix nullspace under Berlekamp.fixedSpaceKernel was only ~8% of the deg-24 RELIFT_PROFILE=prime profile even before the ~1.6-2.3x scalar speedup of #8633, and the FpPoly results above show raw-kernel wins can be invisible end-to-end. If #8647 finds the share immaterial, close this issue without implementation.

🤖 Prepared with Claude Code