perf(berlekamp): profile berlekampFactor mod-p sub-phases and attack the dominant one

[kim-em]

Measured. After #8684 ("perf(polyz): collapse defaultFactorCoeffBound to a closed-form central binomial", closing #8677) removed the Mignotte-bound cost, a grid probe of the classical tier (public Hex.ZPoly.factorClassical) shows the mod-p factorization inside prime selection is now the dominant cost:

input	deg	factorClassical	choosePrimeData? (mod-p)	share
split h2	6	686 us	276 us	40%
split h2	14	5168 us	1646 us	32%
split h2	22	16321 us	7689 us	47%
phi15	8	229 us	147 us	64%
SD3	8	480 us	240 us	50%
SD4	16	4605 us	2232 us	48%

choosePrimeData? (which computes the full mod-p factorization the lift consumes) is a consistent 30-47% across the split degree/height grid and 48-64% on the low-height adversarial families, scaling ~O(deg^3). It is not a single-benchmark artifact. The remaining ~40-65% is Hensel lifting + recombination + bignum coefficient arithmetic (grows with coefficient height; a separate follow-up).

This is row-reduction / gcd bound, NOT matrix multiplication. Do not reach for Strassen. #8699 ("perf(berlekamp): make the delayed-reduction Barrett base kernel beat the default", closing #8687) optimized the Strassen matrix-multiply base kernel; mulStrassen is unreferenced anywhere in the factorization stack (HexBerlekamp / HexBerlekampZassenhaus / HexPolyFp / HexRowReduce), so it does not touch this path. The mod-p cost lives in berlekampFactorsModP (HexBerlekampZassenhaus/PrimeSelection.lean:962) → Berlekamp.berlekampFactor (HexBerlekamp/Factor.lean:151), whose executable cost splits three ways:

1. Frobenius Q-matrix construction — berlekampMatrix / fixedSpaceMatrix (HexBerlekamp/Basic.lean) builds each column via FpPoly.powModMonic (FpPoly.frobeniusXMod f hmonic) f hmonic j (i.e. x^{p*j} mod f): deg columns of modular polynomial arithmetic.
2. Nullspace over F_p — Matrix.nullspace (fixedSpaceMatrix ...) (HexBerlekamp/Basic.lean:686), row reduction via HexRowReduce, ~O(deg^3) scalar ZMod64 ops.
3. Kernel -> factors splitting — DensePoly.gcd (EEA) over F_p.

Task. Profile berlekampFactor into these three sub-phases on the degree grid (deg 6-24) plus the adversarial families (phi15, SD3, SD4), identify which dominates, and land the optimization for the dominant sub-phase if a clear win exists; otherwise report the breakdown and propose the targeted follow-up. Likely shared lever if the cost is scalar-bound: ZMod64.mul / Barrett reduction underneath row reduction and gcd (distinct from PR #8699's matrix-kernel Barrett internals).

Measurement notes.

• Use a compiled lean_exe (or a new RELIFT_PROFILE arm in bench/HexBench/RecursiveReliftSpike.lean), not lake env lean --run — the mod-p path uses native ZMod64 externs the interpreter cannot link.
• factorClassical declines (returns none) on fully-split high-r inputs when the subset budget is exceeded, so measure sub-phases directly on the monic modular image, or use inputs where the classical path actually runs.
• Output/behaviour must be unchanged; the verified reference and @[csimp] boundaries stay intact (no sorry/axiom/native_decide). Keep check_benches_mathlib_free green.