perf(hex-int-factor): complete decomposed Phase-4 evidence (#9864)

* perf(hex-int-factor): complete phase 4 benchmark surface

* perf(hex-int-factor): record phase 4 measurements

* perf(hex-int-factor): document phase 4 acceptance

Cost-model derivation: balanced rho uses the O(n^(1/4)) expected iteration bound; fixed-bound word routes are constant and direct-Nat p-1/ECM use a quadratic operand-cost bound. Replay, entry products, square divisors, and totient use quadratic widening-product bounds; order and primitive-root search use linear candidate bounds. Power forms use the conservative 2^n input-value bound, cyclotomic recursion is quadratic, and sigma exponentiation uses n log n.

* docs(hex-int-factor): correct comparator contract

PARI factor does not expose a mode restricted to Hex's trial-division-plus-rho portfolio, so an external ratio cannot diagnose dispatch or rho by itself. Require same-input internal controls for those claims and keep PARI/GMP-ECM as explicitly portfolio-mismatched informational comparisons.

* docs(hex-int-factor): set balanced policy budget

Use the existing Phase-4 one-second soft ceiling at the 80-bit top rung as the independent absolute criterion for deciding whether the current balanced route requires SQUFOF work.

* docs(hex-int-factor): make internal controls falsifiable

The table control has an explicit 1.25 ratio, while the balanced control uses the dispatcher's exact rho allocation, rejects failures, normalizes outputs, and has an explicit factor-of-two ratio. The comparator contract now reports every GMP-ECM rung with eligibility labels, scopes each endpoint, and leaves SQUFOF to a genuine within-Lean prototype comparison.

* docs(hex-int-factor): compare complete rho pipeline

Replace the mismatched complete-factorization/direct-split ratio with a preregistered comparison between default and rho-only route policies through the same completion and certificate path. Keep direct rho as the independent 2^(bits/4) scaling and profiling target.

* perf(hex-int-factor): measure complete route policy

Thread a private split policy through the production search so the diagnostic rho-only arm retains the exact public preprocessing, random-state progression, recursive certificate construction, and checked-factorization acceptance while disabling only smooth fallback after rho exhaustion.

Use canonical full-factorization encodings for the seven balanced fixed pairs and retain raw rho solely as a 2^(bits/4) scaling target. Preregister per-target fixed ceilings and expected hashes, prevent fixed-term lifting, cover the full default-fuel schedule, and add the 1-through-10 kernel replay ladder ending at a 61-bit Pocklington certificate.

The replay n^2 model follows one bounded guarded multiplication per exponent step on a widening accumulator. The square-divisor n^2 model follows sequential multiplication of n fixed-exponent entries into a linearly widening accumulator; its constant 8192-run loop clears the subprocess floor without changing the model. Sigma entry and totient ladders likewise sum linearly widening fixed-entry products, while sigma exponent uses the n log n surrogate for its growing exact quotient. Raw balanced rho uses the expected 2^(bits/4) cycle cost for factors of half the input width, and order uses one modular multiplication per scanned exponent.

Run table trial division before perfect-power root search and classify fully table-factored powers by the gcd of their multiplicities, removing redundant root searches from the dominant small-dispatch batch without changing its route classification.

* bench(hex-int-factor): collect honest phase 4 evidence

Add per-rung closed-term-safe ECM anchors with literal expected hashes and absolute ceilings. Replace the obsolete collector registrations with the complete normal/forced policy pairs and validate every harness verdict, expected hash, internal ratio, control audit, and default-fuel result before writing an artifact.

Use the same 256-input GMP-ECM subprocess shape for the factor-of-15 protocol control and every shared rung. Pass sigma 7, B1 1000, and B2 1 explicitly, so stage 2 is disabled by B2 < B1. Preserve no-factor outcomes as results rather than misreporting them as protocol failures, and mark ratio eligibility solely from the preregistered overhead-fraction rule.

* bench(hex-int-factor): clear pinned spawn floor

Double the constant square-divisor hot loop so its upper three rungs clear the unchanged ten-times subprocess floor even when pinned spawn overhead approaches 200 ms. This does not change the n^2 model, schedule, tolerance, or fixtures. Surface captured benchmark stdout and stderr when the collector rejects a child run.

* bench(hex-int-factor): admit final square rung

Raise only the per-call safety cap from 60 to 120 seconds so the already-declared 1024-entry hot-loop rung completes under single-CPU affinity. Keep the n^2 model, 0.20 tolerance, schedule, subprocess filter, and fixtures unchanged.

* bench(hex-int-factor): enforce evidence budgets

* fix(bench): accept matching hash status

* fix(bench): keep control audit untimed

* fix(bench): capture comparator version stream

* docs(hex-int-factor): record corrected phase 4 evidence

* bench(hex-int-factor): decompose phase 4 evidence

* bench(hex-int-factor): record decomposed native evidence

* bench(hex-int-factor): record kernel replay evidence

* bench(hex-int-factor): expose mode 3 profile runners

Cost-model derivation: runSmooth performs n copies of one fixed 80-bit unbalanced rho split, so its repetition parameter is linear. runPower performs n copies of one fixed exponent-80 power factorization, so its repetition parameter is also linear. These registrations are attribution-only and do not model operand-size scaling.

* docs(hex-int-factor): report decomposed phase 4 evidence

* docs(hex-int-factor): record five clean profiles

* bench(hex-int-factor): address phase 4 review

Cost-model derivation: the attribution runner repeats one fixed 80-bit ECM stage-1 call, so its declared work is linear in the repetition count.

* docs(hex-int-factor): refresh phase 4 evidence

* docs(hex-int-factor): commit five profile summaries

* test(bench): exempt int-factor proof target from sweep

---------

Co-authored-by: Kim Morrison <kim@lean-fro.org>

Author: kim-em

HexIntFactor/SPEC/hex-int-factor.md

@@ -295,6 +295,13 @@ prerequisite, specified there and sited in hex-basic.
 
 ### 0. Structural reductions, always applied
 
+The dispatcher removes powers of two first, then runs table trial division.
+When the table completely factors the odd cofactor, the gcd of the recovered
+multiplicities identifies a perfect power without a second root scan. Only a
+residual above the table reaches the general perfect-power detector. This
+ordering keeps the dominant small-input path linear in the committed table
+while preserving the same factorization and structural-route result.
+
 - **Powers of two**, by a dedicated trailing-zero count followed by one
   right shift. For positive `n`, the isolated lowest set bit is
   `n XOR (n AND (n - 1))`, so its `log₂` is exactly the multiplicity of two.
@@ -309,6 +316,8 @@ prerequisite, specified there and sited in hex-basic.
   full structural pipeline is reapplied to every popped search-stack entry,
   including recursive cofactors produced by a split; its exponent is multiplied
   by the entry's accumulated multiplicity before the result is merged.
+  On a table-complete input the recovered prime-power multiplicities supply
+  `k` directly; otherwise the general detector runs after table division.
   Strongly recommended rather than mathematically required: an earlier draft
   claimed Pollard `p − 1` and ECM "fail on prime powers, because the
   group they work in has no distinct primes to separate", and that is
@@ -319,7 +328,8 @@ prerequisite, specified there and sited in hex-basic.
   reasons to do it first.
 - **Small primes**, by trial division against hex-primality's
   `primeTable`. This is where most inputs finish and it is the only
-  route whose cost is predictable.
+  route whose cost is predictable. It precedes the general perfect-power root
+  search on the odd cofactor.
 
 ### 1. Pollard rho with Brent's cycle detection
 
@@ -1220,30 +1230,37 @@ Families:
   times the direct-trial median. This internal control, rather than an
   external system with a different portfolio, determines whether dispatch
   overhead is invisible on the case that dominates call volume.
-- **Balanced semiprimes** at 32, 48, 64, and 80 bits. Report `factor?` and
-  `Internal.rhoSplitCountedWith?` on the same ladder and seed. The direct arm
-  receives `defaultPrimeCertBudget.rhoRestarts` and `.rhoSteps`, matching the
-  public dispatcher's allocation. Output-agreeing wrappers return the least
-  factor, reject an error rather than hashing its attempt count, and admit a
-  ratio only when both arms succeeded. The public-dispatch median must be at
-  most twice the matched direct-rho median at every admitted rung. This is the
-  internal Route-1 control for dispatch and certificate construction; rho's
-  own two-sided registration and profile diagnose its scaling and hot path.
-  These controls and their 80-bit top rung are Phase-4 obligations; the
-  smaller pre-Phase-4 registrations do not satisfy them.
+- **Balanced semiprimes** at 32, 40, 48, 56, 64, 72, and 80 bits. Report three
+  distinct surfaces on the same five-seed ladder: the full public `factor?`
+  pipeline; direct `Internal.rhoSplitCountedWith?`, which returns only one
+  normalized divisor; and completion from that precomputed divisor and exact
+  advanced random state through factorization of both sides, canonical merge,
+  and final `checkFactorization` acceptance. The direct-rho target alone has
+  the two-sided `2^(bits/4)` model and profile. The other two are fixed targets
+  because certificate construction dominates different lower rungs. Their
+  output hashes must agree, but `full / rho` and
+  `full / (rho + completion)` are explanatory decompositions rather than
+  acceptance thresholds. Rho-first dispatch and rho-first dispatch with its
+  smooth fallback disabled are not distinct algorithms and are not compared.
 - **Smooth `p − 1` semiprimes** at the same sizes. Route 2; the base is
   fixed so the benchmark measures the specified stage-1 success case.
-- **`b^n ± 1`**, with and without the cyclotomic split, which is the
-  measurement that justifies the split existing.
+- **`b^n ± 1`**, with and without the cyclotomic split, on identical
+  target-derived seeds and canonical outputs for exponents through 80. Seven
+  fixed repeats must show `split / generic ≤ 0.98`, or the split must prevent a
+  generic failure on the admitted family, to justify the factorization route.
+  Otherwise that route is removed; the independently checked split constructor
+  is a separate API.
 - **Unbalanced semiprimes**, a small factor times a large one, where
   ECM is expected to win and rho is expected to as well -- reported
   together, because a route that never wins on any family should be
   removed rather than kept.
 - **Certificate replay**, `checkFactorization` in the kernel on
   factorizations with `k` from `1` to `10` and factors up to `64` bits.
-- **Order and primitive root**, primes up to `64` bits, reported
-  separately from the factorization of `p − 1` they depend on, so the
-  check's cost is visible next to the search's.
+- **Order and primitive root**, a scan ladder through `1048589` plus fixed
+  50- and 61-bit primes whose order for base 3 is short, reported separately
+  from the factorization of `p - 1` they depend on. The two tracks expose both
+  the reference scan cost and downstream operand-size behavior without
+  pretending a linear scan is feasible for an arbitrary 64-bit order.
 - **Generalized divisor sums**, with one ladder growing a prime-power
   exponent through multi-million-bit output and one growing the number
   of certified prime-power entries. Per-rung preparation constructs or
@@ -1255,7 +1272,7 @@ Families:
 
 **Comparators.** PARI `factor` via cypari2 is **informational**:
 PARI dispatches among trial division, SQUFOF, Pollard-Brent rho,
-`p − 1`, and MPQS with tuned crossovers, and this library specifies
+`p - 1`, and MPQS with tuned crossovers, and this library specifies
 neither SQUFOF nor MPQS, so a required ratio would check an algorithm
 that does not exist here. PARI does not expose a benchmark mode that restricts
 `factor` to Hex's trial-division-plus-rho portfolio, so its selected route must
@@ -1292,6 +1309,13 @@ missing portfolio.
 No advance claim is made on anything the quadratic sieve would reach,
 because nothing here reaches it.
 
+The proof-track replay is measured outside lean-bench with rotated paired
+fresh-module builds. A baseline imports the shared replay input; ten candidate
+modules add one `decide +kernel` theorem each for `k = 1..10`, with the final
+case containing a 61-bit Pocklington-certified factor. Compiled profiles cover
+one representative of every `libraries.yml` Phase-4 input family; proof-track
+fresh builds do not create an additional compiled-profile family.
+
 ## The Mathlib layer
 
 ```lean
@@ -1453,7 +1477,7 @@ Neither `HexPrimality` nor `HexIntFactor` is in `libraries.yml` yet, so
 the dependency claims above are draft prose rather than repository
 state until those entries land.
 
-## Open questions
+## Deferred question
 
 - **The default fuel schedule.** Stated above as a function of bit
   length and not fixed. It should be set so that the 80-bit balanced

HexIntFactor/Small.lean

@@ -137,25 +137,48 @@ def SmallCandidate.scale (candidate : SmallCandidate) (multiplier : Nat) :
   { factors := candidate.factors.map fun entry =>
       { entry with exponent := entry.exponent * multiplier }
     residualBase := candidate.residualBase
-    residualExponent := candidate.residualExponent * multiplier
+    residualExponent := if candidate.residualBase = 1 then 1
+      else candidate.residualExponent * multiplier
     route := candidate.route }
 
-/-- Apply perfect-power reduction before table trial division to an odd
-cofactor. -/
+private def exponentGcd : List PrimePower → Nat
+  | [] => 0
+  | entry :: entries =>
+      entries.foldl (fun common next => Nat.gcd common next.exponent)
+        entry.exponent
+
+/-- Apply table trial division and perfect-power reduction to an odd cofactor.
+A complete table factorization exposes perfect powers directly through the gcd
+of its multiplicities, avoiding a redundant root search on the dominant small
+dispatch path while preserving the structural route classification. -/
 private def oddCandidate (n : Nat) : SmallCandidate :=
-  match perfectPower? n with
-  | some (base, exponent) =>
-      let out := trialFactors base
-      { factors := out.1.map fun e => { e with exponent := e.exponent * exponent }
-        residualBase := out.2
-        residualExponent := exponent
+  let out := trialFactors n
+  if out.2 = 1 then
+    let exponent := exponentGcd out.1
+    if 1 < exponent then
+      { factors := out.1
+        residualBase := 1
+        residualExponent := 1
         route := .perfectPower }
-  | none =>
-      let out := trialFactors n
+    else
       { factors := out.1
-        residualBase := out.2
+        residualBase := 1
         residualExponent := 1
         route := .trial }
+  else
+    match perfectPower? n with
+    | some (base, exponent) =>
+        let baseOut := trialFactors base
+        { factors := baseOut.1.map fun e =>
+            { e with exponent := e.exponent * exponent }
+          residualBase := baseOut.2
+          residualExponent := exponent
+          route := .perfectPower }
+    | none =>
+        { factors := out.1
+          residualBase := out.2
+          residualExponent := 1
+          route := .trial }
 
 /-- Remove the full power of two, then apply perfect-power reduction and table
 trial division to the odd cofactor. -/

bench/HexBench/IntFactorKernel.lean

@@ -53,6 +53,25 @@ private def orderTwoModSeven : OrderCert :=
 private def corruptOrder : OrderCert :=
   ⟨2, 7, 2, ⟨2, [⟨1, .small 2⟩]⟩⟩
 
+/- The final entry is a 61-bit prime, so this 1-through-10 ladder exercises
+both table leaves and an above-table Pocklington certificate while keeping the
+factor subjects in canonical ascending order. -/
+private def cert61 : PrimeCert :=
+  .pock 1945555039024054273
+    [(891154892214722695, 55, .small 2),
+     (110189291828549774, 2, .small 3)]
+
+private def replayCerts : List PrimeCert :=
+  [.small 2, .small 3, .small 5, .small 7, .small 11,
+   .small 13, .small 17, .small 19, .small 23, cert61]
+
+private def replayFactors (count : Nat) : List PrimePower :=
+  (replayCerts.take count).map fun cert => ⟨1, cert⟩
+
+private def replayCase (count : Nat) : Factorization :=
+  let factors := replayFactors count
+  ⟨(factors.map (·.prime)).prod, factors⟩
+
 theorem factorizationValid : checkFactorization raw360 = true := by
   decide +kernel
 
@@ -62,6 +81,36 @@ theorem factorizationCorrupt : checkFactorization corruptProduct = false := by
 theorem factorizationPocklington : checkFactorization rawPock7 = true := by
   decide +kernel
 
+theorem replay1 : checkFactorization (replayCase 1) = true := by
+  decide +kernel
+
+theorem replay2 : checkFactorization (replayCase 2) = true := by
+  decide +kernel
+
+theorem replay3 : checkFactorization (replayCase 3) = true := by
+  decide +kernel
+
+theorem replay4 : checkFactorization (replayCase 4) = true := by
+  decide +kernel
+
+theorem replay5 : checkFactorization (replayCase 5) = true := by
+  decide +kernel
+
+theorem replay6 : checkFactorization (replayCase 6) = true := by
+  decide +kernel
+
+theorem replay7 : checkFactorization (replayCase 7) = true := by
+  decide +kernel
+
+theorem replay8 : checkFactorization (replayCase 8) = true := by
+  decide +kernel
+
+theorem replay9 : checkFactorization (replayCase 9) = true := by
+  decide +kernel
+
+theorem replay10 : checkFactorization (replayCase 10) = true := by
+  decide +kernel
+
 theorem orderValid : checkOrder orderTwoModSeven = true := by
   decide +kernel