perf: complete HexIntFactor Phase-4 evidence with decomposed factorization costs

[kim-em]

Parent directive: #9619
depends-on: #9368

Goal

Complete the HexIntFactor Phase-4 package using measurements whose operands and work are explicit. Public factorization, raw rho splitting, and post-split completion are separate surfaces; no timing ratio between unequal APIs or identical route policies is a gate. PARI and GMP-ECM remain informational comparisons with explicitly different implementations.

This issue subsumes #9635. Final dependency-coupled counter recording remains in #9619 after both the local and primality gates are ready.

Preregistered measurement contract

Factorization decomposition

• Keep the deterministic output-agreeing table-range control: public factor? versus direct trialFactors over the committed uniform batch below 10^8; require complete canonical output agreement and public / direct <= 1.25 on the pinned scientific host.
• Measure the balanced 32, 40, 48, 56, 64, 72, and 80-bit five-seed family through three distinct surfaces:
  1. public factor?, including preprocessing, primality rejection, splitting, recursive completion, certificate construction, and checked acceptance;
  2. direct rhoSplitCountedWith?, returning only the normalized split, registered independently against the two-sided 2^(bits/4) model and profiled as the rho hot path;
  3. completion from the corresponding precomputed rho split and advanced generator state, factoring both sides, canonically merging them, and running checked-factorization acceptance.
• Report full, raw-rho, and completion timings separately. Derived full / raw and full / (raw + completion) values are explanatory observations only, with no acceptance threshold. Do not call rho-first dispatch versus rho-only-without-fallback a distinct algorithm comparison.
• Do not infer PARI's selected route or a SQUFOF requirement from timing. SQUFOF remains a separate product question requiring a within-Lean prototype.

Other native evidence

• Run GMP-ECM with curve sigma 7, B1 = 1000, and stage 2 disabled. Use the same persistent 256-input batch for operands and protocol control, subtract the measured floor, and interpret only rows with overhead at most 50% of raw time.
• Normalize every multi-seed Hex batch to one factorization before forming a PARI ratio. Verify PARI and GMP-ECM outputs, and preserve the exact declared comparator name PARI factor and GMP-ECM in the report and libraries.yml.
• Compare generic and cyclotomic power-form factorization on identical target-derived seeds and canonical complete-factorization outputs for exponents 12 through 80, including 72 and 80. Use at least seven repeats. Retain the split only if its aggregate median is at least 2% faster (split / generic <= 0.98) or it prevents a generic failure on the admitted family; otherwise remove the factorization route. The standalone checked cyclotomicSplit? constructor may remain independently useful.
• Measure every committed default-fuel table, balanced, smooth, ECM, and power-form case through 80 bits, including the direct-Nat regime; every case must succeed.
• Keep mode 1 only for independently derived tight models. A mode-2 result must cite a published bound covering the measured phase. Otherwise use mode 3, state plainly that asymptotic regression detection was given up, record attempted parameterizations/schedules and why they failed, and justify every absolute budget from the clean pinned-host baseline plus a stated margin.
• Fixed targets must use opaque runtime inputs and canonical expected hashes. Scientific budget assertions belong in the pinned-host collector, not inside benchmark bodies or lake exe ... verify.

Kernel and profile evidence

• Deliver actual kernel checkFactorization replay cases for k = 1..10, with the largest factor at least 61 bits, and measure them with a rotated fresh-module baseline/replay build protocol rather than reporting correctness alone.
• Profile one representative compiled case for each declared phase4.input_families entry:
  • table-and-balanced-semiprimes;
  • smooth-and-unbalanced-semiprimes;
  • power-forms;
  • certificate-replay-and-order;
  • generalized-divisor-sums.
• Every profile must pass calibration, retained-sample, off-thread-noise, and sensitivity diagnostics; report leaf categories, dominant inclusive paths, exact commands, hashes, tool versions, host, commit, and parameters.
• Audit HexIntFactorMathlib under chore: add explicit correspondence-only classification and seed current bridges #9368 and name HexIntFactor as performance owner if the bridge remains correspondence-only.

Acceptance

• reports/hex-int-factor-performance.md contains the complete benchmark table with exact harness verdict text, factorization decomposition, mode-3 conversion rationale and budget margins, comparator eligibility and per-call ratios, comparator trend narrative, five-family profile attribution, kernel fresh-build results, exact reproduction data, and Concerns.
• The replacement artifact validates every parametric verdict, fixed repeat/hash, canonical output equality, scientific budget, table threshold, successful default-fuel row, external output, and comparator eligibility calculation.
• Concerns: None is an output only if no contrary verdict, missing family, low-confidence profile, or unattributed dominant cost remains. Do not drop rungs, change seeds, loosen thresholds, or reclassify a result after measurement.

Verification

• lake exe hexintfactor_bench list
• lake exe hexintfactor_bench verify
• every scientific, external-comparison, kernel fresh-build, and profile command cited by the report
• Phase-4 artifact/contract checks, DAG, Mathlib-free bench, conformance targets, and full lake build
• fresh independent Claude Opus review while CI runs; address every substantive finding before merge

[kim-em]

Claimed for implementation on branch issue-9634 (pod session unavailable). I will first validate the directive premise against the current source and dependencies.