perf(bz): de-box the generic ZMod64 row-reduction/nullspace under fixedSpaceKernel

[kim-em]

Deboxes the generic Matrix.nullspace / row-reduction under Berlekamp.fixedSpaceKernel into a ZMod64-monomorphic kernel that stays in unboxed Array UInt64 end to end, with a correspondence theorem to the generic nullspace so the public factorization result is unchanged. This is the sole material lever surfaced by the #8647 measurement.

Evidence. Profiling RELIFT_PROFILE=prime under perf on current main (measurement report reports/bz-nullspace-inv-cost-shares.md, filed for #8647) shows the generic Matrix.nullspace + row-reduction under fixedSpaceKernel is now the single largest algorithmic share of the profile: ~15-22% (folded-stack inclusive ~21%, compiled-symbol self-time ~19%), a large relative rise over the earlier deg-24 ~8% baseline. It grew because #8633/#8638 made the field arithmetic word-fast while leaving the generic boxed linear-algebra machinery untouched.

The cost is representation, not arithmetic. ZMod64.mul/add are ~6% combined and already word-fast. What remains is the generic boxed Matrix R n m: boxed ZMod64 elements dispatched through the Lean.Grind.Ring R typeclass so every element op crosses a lean_apply_1/2 closure boundary (~26% of the profile), Array.ofFn-of-Array.ofFn matrix/vector construction (~11% higher-order machinery), boxed-cell allocation/refcount (~22% allocator), and List-based free-column extraction (freeColsList/filterTR_loop). These generic buckets are shared with the mod-p DensePoly.gcd sweep, so only part is nullspace-attributable, but the nullspace subtree itself is ~20%.

Not the packed kernel of #8634. #8634 (packed nullspace kernel) was tried and regressed because it materialized the boxed Matrix at its edges and paid the same per-multiply bignum allocation that #8633 later removed. The acceptance criterion here, stated negatively: no boxed Matrix R n m conversion anywhere on the hot path, before or after row-reduction. The packed Array UInt64 representation must flow from the Berlekamp matrix construction through echelon form, nullspace basis, and witness polynomial extraction with no pack/unpack boundary. The lever is boundary-free monomorphization, not "packed nullspace over a boxed matrix."

Not blocked on #8639. The Barrett-context / lazy-reduction kernels of #8639 specialize FpPoly multiply and ZMod64 matrix multiply; row-reduction is Gaussian elimination through the contextless per-element ZMod64.mul/add/inv, which #8639 does not optimize (its own text notes Barrett "does not help the contextless ZMod64.mul"). This kernel is independent of #8639 and can proceed now.

Out of scope. The ZMod64.inv/extGcd share (#8635) measured ~3% and is not currently material; it is recorded and closed in the #8647 report, not part of this issue. The FpPoly modByMonic reduction cost is tracked separately in #8642.

🤖 Prepared with Claude Code