perf(number-field-tower): complete core Phase-4 scientific evidence

[kim-em]

library: HexNumberFieldTower
depends-on: #9664
depends-on: #9793

Current state

HexNumberFieldTower is recorded through Phase 3 and now has registrations, scientific exports, profiles, comparator evidence, and reports/hex-number-field-tower-performance.md.

The remaining Phase-4 defects are the findings formerly tracked by #9815:

• runTowerFactorLadder is inconclusive and its BHKS/Trager envelope does not cover the inclusive dominant phases; the cited factorization phase is only a small share while rational-polynomial gcd/resultant work dominates.
• fixed component cases are being treated as performance coverage without working the ordered rule or providing canonical mode-3 budgets.
• hash, protocol, and comparator anchors are not themselves performance evidence.

Phase 4 is also dependency-coupled to HexNumberField and HexBerlekampZassenhaus.

Deliverables

• For the realized Trager route, derive a mode-1 model or cite a bound covering the inclusive dominant executable phases for mode 2; otherwise establish a canonical mode-3 input and independently justified absolute budget.
• Work the ordered rule for each fixed component surface and distinguish performance coverage from correctness, hash, protocol, and comparator anchors.
• Exercise the real shift-retry and recursive relative-factorization paths.
• Refresh affected scientific evidence, inclusive profiles, and the Tower headline report.
• Leave the report with explicit modes and an empty Concerns section.
• Advance HexNumberFieldTower to Phase 4 only after perf(number-field): complete core Phase-4 scientific evidence #9664, chore: re-promote HexBerlekampZassenhaus after the restored Hensel gate #9793, and every tower-local gate pass.

This issue subsumes #9815.

Verification

• lake build HexNumberFieldTower
• lake exe hexnumberfieldtower_bench list
• lake exe hexnumberfieldtower_bench verify
• affected scientific runs and inclusive profiles
• Tower conformance/oracle path
• python3 scripts/check_phase4.py
• python3 scripts/check_dag.py
• full CI

[kim-em]

Reusable result from the HexNumberField Phase-4 work, which this issue will otherwise rediscover.

bench/HexNumberFieldTower/Bench.lean:766 still has the pattern that capped the NumberField ladders:

private def refinedOf? (p : ZPoly) (h : HasOnlySimpleRoots p) : ... :=
  let isolations ← isolate p h (separationDepth p : Int)

isolate refines every root of p at separation depth and requires the certified discs to be pairwise disjoint, in order to take the first one. Measured cost of that prelude on an idle chungus2, with the timed call itself in microseconds: 4.9 s at n = 16, 14.2 s at n = 20, 30.8 s at n = 24, 61 s at n = 28, over eleven minutes at n = 32. It bounds the ladder, not the operation, and it inflates verify — hexnumberfieldtower_bench is currently 45 s of the repo-wide bench-verify budget, third largest.

#9727 (closed, PR #9734) fixed this for HexNumberField by adding a HexRoots entry point that certifies a single atom directly:

HexRoots/IsolateAll.lean:82
@[expose] def isolateOne? (p : ZPoly) (atomPrec : Int) (seed : DyadicSquare)
    (strategy : AtomStrategy := .nkThenPellet) : Option (RefinedIsolation p)

seeded from an untrusted integer-Newton approximation. The certificate still says its region contains exactly one simple root; it just stops constructing and pairwise-separating the other n - 1. Worth adopting here before choosing this library's ladder ranges, since otherwise the ranges get chosen by fixture cost rather than by the operations being measured.

Two other transferable results from #9664, both of which cost real time to find:

• The arithmetic fixture there varied coefficient height with degree — ±(i + salt + 1) / (i + 2) has a reduced common denominator with Θ(n) bit length — so no fixed-height cost model could fit any ladder built on it. Check denseRatCoeffs or its equivalent here before trusting a verdict.
• verify builds every fixed rung's fixture, so per-rung comparator ladders are charged to the CI smoke budget. That budget hit its 360 s hard cap exactly during this work.

[kim-em]

The directive premise does not survive the ordered-mode check, so I am stopping rather than advancing Tower to Phase 4 on ineffective fixed caps.

Concrete evidence from a clean CPU-19 rerun at commit 605abcb5c, using five independent outer trials:

• runToPrimitiveLadder, original source-derived n³ full-basis model, schedule n = 2,3,4,5,6,9: inconclusive, β = +0.548. Median times were 13.374 µs, 46.288 µs, 99.725 µs, 229.157 µs, 338.607 µs, and 2.371 ms; top-rung spread was only 5.08%. This reproduces the earlier one-trial +0.521 result and rules out host noise as its explanation.
• The proposed replacement runToPrimitive fixed case used dimension 4 at 13.914 µs with a 1 s whole-child cap. LeanBench auto-tunes its batch after observing current speed, so that cap would not detect an operation regression until several orders of magnitude; dimension 4 is also not the top completed diagnostic rung. It is not the canonical hard input with a meaningful operation-specific ceiling required by SPEC/benchmarking.md mode 3.
• runTowerDivLadder likewise rejects the independently derived n² log n model through dimension 24 with β = +0.594, while the top body time is only 12.618 ms and the proposed fixed case was a sparse dimension-4 input at 79 µs. That fixed cap has the same mode-3 defect.
• Negation was recalibrated without the expensive relative-extension fixture: a validated one-level presentation gives the timed implementation the identical fixed-height dense coordinate array and reaches dimensions 4,6,8,12,16,24,32,48. Five-trial β is still −0.162, just outside the default gate. There is no hard negation input for an honest mode 3.
• Extending inversion alongside division reaches n = 8 cleanly but the n = 12 certified height-two fixture hits the child wall cap in all five trials, so its earlier narrow pass does not resolve the sibling divergence.

SPEC/benchmarking.md mandates filing/rollback when a declared mode fails, and mode 4 when neither an honest model/bound nor a canonical hard input exists. The requested empty Concerns section and done_through: 4 therefore cannot be justified without first correcting the toPrimitive wall-growth finding and resolving performance modes for division/negation (and the inversion calibration gap). Treating hash/protocol/comparator anchors or auto-tuned fixed batches as performance evidence would repeat the defect this issue is meant to remove.

I have closed PR #9889 and removed my assignment so #9665 remains claimable after the directive is updated. The clean diagnostic command was:

taskset -c 19 .lake/build/bin/hexnumberfieldtower_bench run \
  Hex.NumberTowerBench.runTowerNegLadder \
  Hex.NumberTowerBench.runTowerInvLadder \
  Hex.NumberTowerBench.runToPrimitiveLadder \
  --outer-trials 5 --export-file /tmp/hex-number-field-tower-opus-calibration-605abcb5-chungus2-cpu19.json