feat(hex-roots): retune Phase-4 wall models and record inconclusive scientific run

[kim-em]

This PR retunes the 13 parametric bench registrations in bench/HexRoots/Bench.lean from pure exact-dyadic op-counts to wall-time models (the SPEC op-count contract times the family's working-bit-length B growth where that growth is asymptotically significant on the schedule), runs the Phase-4 scientific measurement on chungus2, and records it in reports/hexroots-performance.md, but does not claim Phase 4: 9 of the 13 registrations return inconclusive and two of the three SPEC time budgets fail, so libraries.yml keeps HexRoots.done_through: 3 and the report's Concerns section is non-empty. The five model expressions that changed are the whole-polynomial drivers and the compare group (runIsolateAll, runIsolate, runIsolateNk, runIsolatePellet, runIsolateNkThenPellet): the SPEC contract is O(n³·B²) bit operations, and with B = Θ(n) (target precision plus the seeded n·log‖p‖∞ term plus the Taylor coefficients' Θ(prec·n) denominator growth) folding into the schoolbook O(B²) growing-precision arithmetic this gives the n⁵ wall model; the other registrations keep their op-counts (n, n², t²) because their operands stay in the flat sub-word band across their schedules, with the reconciliation in each adjacent derivation comment and in the commit message.

The scientific run (commit b08a66cce522, AMD EPYC 9455, Lean 4.32.0-rc1, lean-bench 0.1.0) is consistent for runMahlerPrec, runNkWitnessCheck, runRefine1, and runIsolateNk, and inconclusive for the other nine; every verdict is reported verbatim in the report. The nine are benchmark-family/schedule/budget findings, not wrong-asymptotic implementation bugs, each diagnosed per registration in Concerns: the fixed non-integer Taylor centre's transition-band growth (~n^2.25, probed to n=1024), the startup-dominated microsecond band of the small-degree witness benches, the seeded family's degree-dependent (non-monotonic) root geometry, refineTo's Newton-doubling precision quantisation, and the compare group's narrow 5-rung range. The cross-strategy compare group passes its agreement gate (all three strategies agree on the strategy-invariant hash 0x6519358031d0ea70); on the integer-root family the Pellet route is the faster one (ratio pellet/nk 0.66 → 0.45 across degree). The python-flint fmpz_poly.complex_roots comparator (informational, run via scripts/bench/hexroots_flint_compare.py with the seeded coefficients byte-verified against the Lean generator) records hex/flint ratios of 315× to ~30000× on the seeded ladder, expected for an integer-certified isolator against a float engine; MPSolve is informational scheduled-only with its environment stated in the bench module docstring. SPEC time budgets: degree 10 @ prec 32 is met (0.137 s < 1 s), but degree 50 @ prec 64 takes 495.85 s (49.6× over the < 10 s target) and degree 100 @ prec 128 did not complete in a 19-minute window (> 19× the < 1 min target). Profiles (perf, one case per input family) confirm the derivations — GMP+allocation dominated for the growing-precision seeded-dense driver, own-code (Dyadic arithmetic) dominated for the sub-word wilkinson-linprod family, t-bit divrem dominated for refine-fixed — and satisfy the Attribution rule.

Helper defs not in the SPEC: scripts/bench/hexroots_flint_compare.py (the python-flint process-call comparator driver) and scripts/plots/hex-roots-comparator.py (the seeded-dense comparator-runtime plot generator). This PR also fixes a real bug in scripts/check_phase4.py: its changed-registration diff parser treated deleted ---comment lines (which render as --- … in the diff) as the --- a/<file> header and mis-counted them as context, inflating the reported line number of the following setup_benchmark so that a correctly-placed derivation comment was reported missing; the fix treats all in-hunk --prefixed lines as deletions.

🤖 Prepared with Claude Code

[kim-em]

Follow-up to the PR's Concerns: the two Phase-4 blocking findings are now tracked in #8750 (bench re-scaffolding for the nine inconclusive verdicts) and #8751 (deep-target time budgets; the SPEC-anticipated Graeffe deferral is the named candidate). The Codex review's two findings (polylog-suppression policy made explicit on the five n⁵ models; the flint comparator now fails loudly if the Lean seeded family's LCG literals drift) are addressed in the follow-up commits.