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

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