diff --git a/HexIntFactorMathlib/SPEC/hex-int-factor-mathlib.md b/HexIntFactorMathlib/SPEC/hex-int-factor-mathlib.md
new file mode 100644
index 0000000000..f7c7a56596
--- /dev/null
+++ b/HexIntFactorMathlib/SPEC/hex-int-factor-mathlib.md
@@ -0,0 +1,69 @@
+# hex-int-factor-mathlib (depends on hex-int-factor + hex-primality-mathlib + Mathlib)
+
+## Correspondence-only classification
+
+This library is a `correspondence-only-layer`.
+
+Computational conformance owner: `HexIntFactor`
+Computational performance owner: `HexIntFactor`
+
+The companion proves that checked `HexIntFactor` data agrees with Mathlib's
+factorization, divisor, squarefree, totient, and multiplicative-order APIs. It
+does not search for factors or orders, replay a certificate, reify syntax, run
+a tactic, or install a decision procedure. All transported values are computed
+by `HexIntFactor`; this layer supplies proofs that identify those values with
+their Mathlib counterparts.
+
+## Factorization correspondences
+
+`HexIntFactorMathlib.Factorization` transports the core checker facts and
+arithmetic operations:
+
+- `factorization_entry`, `factorization_eq`, and
+  `CheckedFactorization.factorization_eq` identify checked multiplicities with
+  `Nat.factorization`;
+- `factorization_absent` pins zero multiplicity outside the listed prime
+  support;
+- `factors_eq` and `CheckedFactorization.primeFactorsList_eq` identify the
+  canonical expanded prime list;
+- `divisors_eq`, `divisors_list_eq`, and `numDivisors_eq_card` identify the
+  checked divisor enumeration and count;
+- `totient_eq`, `sigma_eq`, `primeFactors_eq`, and `radical_eq` transport the
+  corresponding arithmetic functions; and
+- `isSquarefree_iff_squarefree`, `squarefreePart_mathlib`, and
+  `squareDivisor_mathlib` transport the square-decomposition facts.
+
+Their computational coverage lives in
+`conformance/HexIntFactor/Conformance.lean`: complete-certificate acceptance
+and rejection, canonical factor support and multiplicity, divisor enumeration,
+generalized divisor sums, totient, radical, and squarefree decomposition all
+have typical, edge, and adversarial checks. The required PARI/python-flint
+oracle independently recomputes factorization and the transported arithmetic
+values from the original inputs.
+
+The private expanded-list helpers occur only in theorem statements and proofs.
+They are normal forms for correspondence, not a separately advertised runtime
+surface.
+
+## Order correspondences
+
+`HexIntFactorMathlib.Order` proves:
+
+- `orderOf_unitOfCoprime`, relating the core natural-number order to Mathlib's
+  order of the corresponding unit;
+- `orderOf_natCast`, including the nonunit case; and
+- `orderOf_eq`, specializing the correspondence to an accepted `OrderCert`.
+
+The transported `Hex.Nat.orderOf` computation is covered by the
+`HexPrimality` conformance suite. `HexIntFactor` conformance separately covers
+accepted, malformed, and nonminimal order certificates, primitive-root
+testing and bounded search, and Carmichael values and laws. This companion
+contains no bridge-local executable operation to test independently.
+
+## Boundary
+
+The public umbrella imports only the two correspondence modules. The library
+owns no conformance source, compiled benchmark, proof-probe root, oracle
+wrapper, executable checker, reifier, tactic, or global instance. It therefore
+has no ordinary Phase-3 conformance target and no separate Phase-4 runtime
+surface.
diff --git a/conformance-fixtures/HexIntFactor/intfactor.jsonl b/conformance-fixtures/HexIntFactor/intfactor.jsonl
index 131237fbad..30c95d4947 100644
--- a/conformance-fixtures/HexIntFactor/intfactor.jsonl
+++ b/conformance-fixtures/HexIntFactor/intfactor.jsonl
@@ -87,21 +87,21 @@
 {"kind":"factor","lib":"HexIntFactor","case":"factor/below100/49","n":49}
 {"kind":"result","lib":"HexIntFactor","case":"factor/below100/49","op":"factor","value":[[7,2]]}
 {"kind":"divisorfn","lib":"HexIntFactor","case":"divisorfn/1","n":1}
-{"kind":"result","lib":"HexIntFactor","case":"divisorfn/1","op":"divisorfn","value":{"tau":1,"sigma0":1,"sigma1":1,"sigma2":1,"phi":1,"rad":1,"sqfpart":1,"sqdiv":1}}
+{"kind":"result","lib":"HexIntFactor","case":"divisorfn/1","op":"divisorfn","value":{"divisors":[1],"tau":1,"sigma0":1,"sigma1":1,"sigma2":1,"phi":1,"rad":1,"sqfpart":1,"sqdiv":1}}
 {"kind":"divisorfn","lib":"HexIntFactor","case":"divisorfn/2","n":2}
-{"kind":"result","lib":"HexIntFactor","case":"divisorfn/2","op":"divisorfn","value":{"tau":2,"sigma0":2,"sigma1":3,"sigma2":5,"phi":1,"rad":2,"sqfpart":2,"sqdiv":1}}
+{"kind":"result","lib":"HexIntFactor","case":"divisorfn/2","op":"divisorfn","value":{"divisors":[1,2],"tau":2,"sigma0":2,"sigma1":3,"sigma2":5,"phi":1,"rad":2,"sqfpart":2,"sqdiv":1}}
 {"kind":"divisorfn","lib":"HexIntFactor","case":"divisorfn/4","n":4}
-{"kind":"result","lib":"HexIntFactor","case":"divisorfn/4","op":"divisorfn","value":{"tau":3,"sigma0":3,"sigma1":7,"sigma2":21,"phi":2,"rad":2,"sqfpart":1,"sqdiv":2}}
+{"kind":"result","lib":"HexIntFactor","case":"divisorfn/4","op":"divisorfn","value":{"divisors":[1,2,4],"tau":3,"sigma0":3,"sigma1":7,"sigma2":21,"phi":2,"rad":2,"sqfpart":1,"sqdiv":2}}
 {"kind":"divisorfn","lib":"HexIntFactor","case":"divisorfn/12","n":12}
-{"kind":"result","lib":"HexIntFactor","case":"divisorfn/12","op":"divisorfn","value":{"tau":6,"sigma0":6,"sigma1":28,"sigma2":210,"phi":4,"rad":6,"sqfpart":3,"sqdiv":2}}
+{"kind":"result","lib":"HexIntFactor","case":"divisorfn/12","op":"divisorfn","value":{"divisors":[1,2,3,4,6,12],"tau":6,"sigma0":6,"sigma1":28,"sigma2":210,"phi":4,"rad":6,"sqfpart":3,"sqdiv":2}}
 {"kind":"divisorfn","lib":"HexIntFactor","case":"divisorfn/72","n":72}
-{"kind":"result","lib":"HexIntFactor","case":"divisorfn/72","op":"divisorfn","value":{"tau":12,"sigma0":12,"sigma1":195,"sigma2":7735,"phi":24,"rad":6,"sqfpart":2,"sqdiv":6}}
+{"kind":"result","lib":"HexIntFactor","case":"divisorfn/72","op":"divisorfn","value":{"divisors":[1,2,3,4,6,8,9,12,18,24,36,72],"tau":12,"sigma0":12,"sigma1":195,"sigma2":7735,"phi":24,"rad":6,"sqfpart":2,"sqdiv":6}}
 {"kind":"divisorfn","lib":"HexIntFactor","case":"divisorfn/360","n":360}
-{"kind":"result","lib":"HexIntFactor","case":"divisorfn/360","op":"divisorfn","value":{"tau":24,"sigma0":24,"sigma1":1170,"sigma2":201110,"phi":96,"rad":30,"sqfpart":10,"sqdiv":6}}
+{"kind":"result","lib":"HexIntFactor","case":"divisorfn/360","op":"divisorfn","value":{"divisors":[1,2,3,4,5,6,8,9,10,12,15,18,20,24,30,36,40,45,60,72,90,120,180,360],"tau":24,"sigma0":24,"sigma1":1170,"sigma2":201110,"phi":96,"rad":30,"sqfpart":10,"sqdiv":6}}
 {"kind":"divisorfn","lib":"HexIntFactor","case":"divisorfn/248832","n":248832}
-{"kind":"result","lib":"HexIntFactor","case":"divisorfn/248832","op":"divisorfn","value":{"tau":66,"sigma0":66,"sigma1":745108,"sigma2":92875849430,"phi":82944,"rad":6,"sqfpart":3,"sqdiv":288}}
+{"kind":"result","lib":"HexIntFactor","case":"divisorfn/248832","op":"divisorfn","value":{"divisors":[1,2,3,4,6,8,9,12,16,18,24,27,32,36,48,54,64,72,81,96,108,128,144,162,192,216,243,256,288,324,384,432,486,512,576,648,768,864,972,1024,1152,1296,1536,1728,1944,2304,2592,3072,3456,3888,4608,5184,6912,7776,9216,10368,13824,15552,20736,27648,31104,41472,62208,82944,124416,248832],"tau":66,"sigma0":66,"sigma1":745108,"sigma2":92875849430,"phi":82944,"rad":6,"sqfpart":3,"sqdiv":288}}
 {"kind":"divisorfn","lib":"HexIntFactor","case":"divisorfn/1296000","n":1296000}
-{"kind":"result","lib":"HexIntFactor","case":"divisorfn/1296000","op":"divisorfn","value":{"tau":160,"sigma0":160,"sigma1":4813380,"sigma2":2624308792820,"phi":345600,"rad":30,"sqfpart":10,"sqdiv":360}}
+{"kind":"result","lib":"HexIntFactor","case":"divisorfn/1296000","op":"divisorfn","value":{"divisors":[1,2,3,4,5,6,8,9,10,12,15,16,18,20,24,25,27,30,32,36,40,45,48,50,54,60,64,72,75,80,81,90,96,100,108,120,125,128,135,144,150,160,162,180,192,200,216,225,240,250,270,288,300,320,324,360,375,384,400,405,432,450,480,500,540,576,600,640,648,675,720,750,800,810,864,900,960,1000,1080,1125,1152,1200,1296,1350,1440,1500,1600,1620,1728,1800,1920,2000,2025,2160,2250,2400,2592,2700,2880,3000,3200,3240,3375,3456,3600,4000,4050,4320,4500,4800,5184,5400,5760,6000,6480,6750,7200,8000,8100,8640,9000,9600,10125,10368,10800,12000,12960,13500,14400,16000,16200,17280,18000,20250,21600,24000,25920,27000,28800,32400,36000,40500,43200,48000,51840,54000,64800,72000,81000,86400,108000,129600,144000,162000,216000,259200,324000,432000,648000,1296000],"tau":160,"sigma0":160,"sigma1":4813380,"sigma2":2624308792820,"phi":345600,"rad":30,"sqfpart":10,"sqdiv":360}}
 {"kind":"order","lib":"HexIntFactor","case":"order/primitive/3mod7","base":3,"modulus":7}
 {"kind":"result","lib":"HexIntFactor","case":"order/primitive/3mod7","op":"order","value":6}
 {"kind":"order","lib":"HexIntFactor","case":"order/nonprimitive/2mod7","base":2,"modulus":7}
diff --git a/conformance/HexIntFactor/Conformance.lean b/conformance/HexIntFactor/Conformance.lean
index a2377db286..cf1a0fa3e3 100644
--- a/conformance/HexIntFactor/Conformance.lean
+++ b/conformance/HexIntFactor/Conformance.lean
@@ -6,7 +6,53 @@ Authors: Kim Morrison
 
 import HexIntFactor
 
-/-! Route-level and checker regression tests for integer factorization. -/
+/-!
+Core conformance for checked integer factorization, arithmetic consumers, and
+the factor-search routes.
+
+Oracle: PARI (via cypari2) independently recomputes factorization, divisor
+functions, orders, and cyclotomic values from the original inputs;
+python-flint independently recomputes every factorization
+(`scripts/oracle/intfactor_pari.py`).
+Mode: `required`
+Covered operations:
+- `checkFactorization`, `checkPartial`, `factor?`, `factorPartial?`, and the
+  explicitly budgeted `Internal.factorCountedWith?`
+- `defaultFuel`, structural reductions, table trial division, and exact-root
+  and perfect-power detection
+- `rhoSplit?`, `Internal.rhoSplitCountedWith?`, `pMinusOneFactor`,
+  `pMinusOneFactorCounted`, and `ecmStage1`
+- `intFactorSearch` and its checker-accepted complete/partial projection; the
+  registered elaborator extension is exercised in `PrimalityConformance.lean`
+- `powerTarget`, `cyclotomicSplit?`, `factorPowerWithRoute?`, and `factorPower?`
+- `divisors`, `numDivisors`, `sigmaEntry`, `sigma`, `totient`, `radical`,
+  `squarefreePart`, `squareDivisor`, and `isSquarefree`
+- `checkOrder`, `isPrimitiveRoot`, `primitiveRoot?`, `carmichaelPrimePower`,
+  and `carmichael`
+Covered properties:
+- accepted complete and partial certificates reconstruct their positive subject
+  with canonical positive prime-power entries
+- every successful split route returns a dynamically checked proper divisor
+- explicit nested budgets, route selection, retry accounting, random-state
+  advancement, and bounded failure reasons remain observable and distinct
+- cyclotomic parts multiply to the declared signed-power target and the public
+  projection preserves routed successes and failures
+- divisor enumeration is canonical, divisor functions satisfy their product
+  and sum laws, and square decomposition reconstructs the subject
+- accepted order certificates are minimal; primitive-root decisions agree with
+  exact order; Carmichael exponents annihilate units and contain their orders
+Covered edge cases:
+- zero and one subjects, empty factor lists, zero fuel, and invalid power forms
+- repeated, descending, composite, zero-exponent, wrong-product, and
+  attacker-sized factor entries
+- powers of two, nested perfect powers, recursive perfect-power cofactors, and
+  table-boundary residuals
+- rho exhaustion and all proper-factor / gcd-one / whole-modulus outcomes for
+  p-minus-one and ECM, on both word and arbitrary-precision backends
+- nonminimal order witnesses, modulus one, the prime two, non-generators, and
+  mixed two-adic/odd Carmichael factors
+- complete, partial, and zero-input primality-search projections
+-/
 
 open Hex Hex.Nat
 
@@ -18,6 +64,9 @@ private def raw12 : Factorization :=
 private def checked12 : CheckedFactorization 12 :=
   ⟨raw12, rfl, by decide⟩
 
+private def checked6 : CheckedFactorization 6 :=
+  ⟨⟨6, [⟨1, .small 2⟩, ⟨1, .small 3⟩]⟩, rfl, by decide⟩
+
 private def checked1 : CheckedFactorization 1 :=
   ⟨⟨1, []⟩, rfl, by decide⟩
 
@@ -33,6 +82,15 @@ private def checked30 : CheckedFactorization 30 :=
 private def checked3600 : CheckedFactorization 3600 :=
   ⟨⟨3600, [⟨4, .small 2⟩, ⟨2, .small 3⟩, ⟨2, .small 5⟩]⟩, rfl, by decide⟩
 
+private def checkedPrime2 : CheckedPrimeCert 2 :=
+  ⟨.small 2, rfl, by decide⟩
+
+private def checkedPrime7 : CheckedPrimeCert 7 :=
+  ⟨.small 7, rfl, by decide⟩
+
+private def checkedPrime13 : CheckedPrimeCert 13 :=
+  ⟨.small 13, rfl, by decide⟩
+
 private def checkedPow64 : CheckedFactorization (2 ^ 64) :=
   ⟨⟨2 ^ 64, [⟨64, .small 2⟩]⟩, rfl, by decide⟩
 
@@ -63,6 +121,11 @@ example {n : Nat} (F : CheckedPartialFactorization n) :
     (fun a b => a.prime < b.prime) :=
   checkPartial_sorted F.valid
 
+#guard checkPartial checkedPartial60.raw
+#guard checkPartial ⟨1, [], 1⟩
+#guard !checkPartial ⟨60, [⟨2, .small 2⟩], 7⟩
+#guard !checkPartial ⟨60, [⟨1, .small 3⟩, ⟨2, .small 2⟩], 5⟩
+
 #guard checkFactorization raw12
 #guard !checkFactorization ⟨12, [⟨1, .small 4⟩, ⟨1, .small 3⟩]⟩
 #guard !checkFactorization ⟨12, [⟨1, .small 2⟩, ⟨1, .small 3⟩]⟩
@@ -89,6 +152,7 @@ example {n : Nat} (F : CheckedPartialFactorization n) :
 -- `sigmaEntry` remains total even for uncertified `PrimePower` values.
 #guard sigmaEntry ⟨3, .small 0⟩ 1 == 1
 #guard sigmaEntry ⟨3, .small 1⟩ 1 == 4
+#guard sigmaEntry ⟨2, .small 3⟩ 0 == 3
 #guard sigma checked1 0 == 1
 #guard sigma checked12 0 == 6
 #guard sigma checked12 1 == 28
@@ -142,13 +206,17 @@ example :
 #guard ((List.range 36).filter fun a => Nat.Coprime a 36).length !=
   ((List.range 6).filter fun a => Nat.Coprime a 6).length *
     ((List.range 6).filter fun a => Nat.Coprime a 6).length
+#guard radical checked1 == 1
 #guard radical checked12 == 6
+#guard radical checked30 == 30
+#guard radical checked10800 == 30
 #guard squarefreePart checked1 == 1
 #guard squareDivisor checked1 == 1
 #guard squarefreePart checked12 == 3
 #guard squareDivisor checked12 == 2
 #guard squarefreePart checked30 == 30
 #guard squareDivisor checked30 == 1
+#guard isSquarefree checked1
 #guard isSquarefree checked30
 #guard squarefreePart checked3600 == 1
 #guard squareDivisor checked3600 == 60
@@ -158,17 +226,37 @@ example :
 #guard squarefreePart checkedPow64 == 1
 #guard squareDivisor checkedPow64 == 2 ^ 32
 #guard !isSquarefree checked12
+#guard !isSquarefree checked3600
+
+-- Search budgets remain bit-length scaled at the empty, ordinary, and
+-- arbitrary-precision boundaries.
+#guard defaultFuel 0 == 32
+#guard defaultFuel 12 == 44
+#guard defaultFuel (2 ^ 64) == 288
 
+#guard removePower 3 81 10 == (4, 1)
+#guard removePower 3 14 10 == (0, 14)
+#guard removePower 1 12 10 == (0, 12)
 #guard splitTwos 0 == (0, 0)
 #guard splitTwos 99 == (0, 99)
 #guard splitTwos (2 ^ 20) == (20, 1)
 #guard splitTwos (3 * 2 ^ 20) == (20, 3)
 #guard (trialFactors 0).1.isEmpty && (trialFactors 0).2 == 0
+#guard (trialFactors 12).1.map (fun e => (e.prime, e.exponent)) == [(2, 2), (3, 1)]
+#guard (trialFactors 12).2 == 1
+#guard (trialFactors 99991).1.map
+  (fun e => (e.prime, e.exponent)) == [(99991, 1)]
+#guard (trialFactors 99991).2 == 1
+#guard (trialFactors 100003).1.isEmpty && (trialFactors 100003).2 == 100003
+#guard (trialFactors 1000003).1.isEmpty && (trialFactors 1000003).2 == 1000003
+#guard (smallCandidate 97).route == .trial
 #guard (smallCandidate (2 ^ 20)).route == .twos
 #guard (smallCandidate (2 ^ 20)).factors.map
   (fun entry => (entry.prime, entry.exponent)) == [(2, 20)]
 #guard exactRoot? 65025 2 == some 255
 #guard exactRoot? 759375 5 == some 15
+#guard exactRoot? 65026 2 == none
+#guard exactRoot? 81 1 == none
 #guard perfectPower? (2 ^ 9973) == some (2, 9973)
 #guard (perfectPower? (2 ^ 10000)).isSome
 #guard perfectPower? (2 ^ 10009) == some (2, 10009)
@@ -244,6 +332,10 @@ private def pMinusOneWhole :=
 #guard pMinusOneWhole.attempts == 1
 #guard pMinusOneWhole.rand == Rand.ofSeed 13
 
+#guard ecmBackend 0 == .natural
+#guard ecmBackend (2 ^ 64 - 1) == .word
+#guard ecmBackend (2 ^ 64) == .natural
+
 #guard smoothBoundCap == 9999
 #guard smoothBoundCap < primeTableBound
 #guard smoothBound (primeTableBound + 1000) == smoothBoundCap
@@ -420,6 +512,31 @@ private def smoothCapTrace : Hex.Nat.Internal.SmoothSearch :=
   | .ok (d, _) => decide (1 < d) && decide (d < 91) && 91 % d == 0
   | .error _ => false)
 
+#guard (match rhoSplit? 91 (Rand.ofSeed 1) 0 with
+  | .error _ => true
+  | .ok _ => false)
+
+#guard (match rhoSplit? 97 (Rand.ofSeed 1) 16 with
+  | .error _ => true
+  | .ok _ => false)
+
+#guard (match Hex.Nat.Internal.rhoSplitCountedWith?
+    91 (Rand.ofSeed 1) 16 16 with
+  | .ok success =>
+      decide (1 < success.factor) && decide (success.factor < 91) &&
+        91 % success.factor == 0
+  | .error _ => false)
+
+#guard (match Hex.Nat.Internal.rhoSplitCountedWith?
+    91 (Rand.ofSeed 1) 0 16 with
+  | .error _ => true
+  | .ok _ => false)
+
+#guard (match Hex.Nat.Internal.rhoSplitCountedWith?
+    97 (Rand.ofSeed 1) 4 64 with
+  | .error _ => true
+  | .ok _ => false)
+
 #guard Hex.Nat.Internal.rhoRestartBudget 1000000 == 8
 #guard Hex.Nat.Internal.rhoRestartBudget 3 == 3
 
@@ -454,6 +571,9 @@ private def starvedInput : Nat := 1000003 * 1000033
 -- certificate work and the preceding split rather than dropping either.
 private def retainedCertInput : Nat := starvedInput * 1000037
 
+private def searchAllocation (factorFuel : Nat) : FactorSearchBudget :=
+  ⟨defaultPrimeCertBudget, 16, factorFuel⟩
+
 #guard (match factor? retainedCertInput (Rand.ofSeed 3) (fuel := 3) with
   | .error failure =>
       failure.stop == .incomplete &&
@@ -468,6 +588,44 @@ private def retainedCertInput : Nat := starvedInput * 1000037
   | .ok (F, _) => checkPartial F.raw && F.raw.residual == starvedInput
   | .error _ => false)
 
+#guard (match factorPartial? 12 (Rand.ofSeed 12) with
+  | .ok (F, _) => checkPartial F.raw && F.raw.residual == 1
+  | .error _ => false)
+
+#guard (match factorPartial? 0 (Rand.ofSeed 3) with
+  | .error failure => failure.stop == .zero && failure.attempts == 0
+  | .ok _ => false)
+
+#guard (match Hex.Nat.Internal.factorCountedWith? defaultPrimeCertBudget 16
+    12 (Rand.ofSeed 12) (defaultFuel 12) with
+  | .ok success => checkFactorization success.factorization.raw
+  | .error _ => false)
+
+#guard (match Hex.Nat.Internal.factorCountedWith? defaultPrimeCertBudget 16
+    0 (Rand.ofSeed 0) 0 with
+  | .error failure => failure.stop == .zero && failure.attempts == 0
+  | .ok _ => false)
+
+#guard (match Hex.Nat.Internal.factorCountedWith? defaultPrimeCertBudget 0
+    starvedInput (Rand.ofSeed 3) 0 with
+  | .error failure =>
+      failure.stop == .incomplete &&
+        match failure.snapshot with
+        | some saved => checkPartial saved.raw && saved.raw.residual == starvedInput
+        | none => false
+  | .ok _ => false)
+
+#guard let result :=
+    intFactorSearch (searchAllocation (defaultFuel 12)) 12 (Rand.ofSeed 12)
+  result.raw.factors == [(2, 2), (3, 1)] && result.raw.residual == 1
+
+#guard let result :=
+    intFactorSearch (searchAllocation 0) starvedInput (Rand.ofSeed 3)
+  result.raw.factors.isEmpty && result.raw.residual == starvedInput
+
+#guard let result := intFactorSearch (searchAllocation 0) 0 (Rand.ofSeed 0)
+  result.raw.factors.isEmpty && result.raw.residual == 0
+
 #guard (match factor? starvedInput (Rand.ofSeed 3) (fuel := 1) with
   | .error failure =>
       failure.stop == .incomplete && 0 < failure.attempts &&
@@ -477,7 +635,53 @@ private def retainedCertInput : Nat := starvedInput * 1000037
         | none => false
   | .ok _ => false)
 
-#guard checkOrder ⟨2, 7, 3, ⟨3, [⟨1, .small 3⟩]⟩⟩
+private def orderTwoModSeven : OrderCert :=
+  ⟨2, 7, 3, ⟨3, [⟨1, .small 3⟩]⟩⟩
+
+private def nonminimalOrder : OrderCert :=
+  ⟨2, 7, 6, checked6.raw⟩
+
+#guard checkOrder orderTwoModSeven
+#guard !checkOrder ⟨1, 1, 1, checked1.raw⟩
+#guard !checkOrder nonminimalOrder
+#guard checkOrder ⟨5, 8, 2, ⟨2, [⟨1, .small 2⟩]⟩⟩
+
+#guard isPrimitiveRoot checkedPrime2 checked1 1
+#guard isPrimitiveRoot checkedPrime7 checked6 3
+#guard !isPrimitiveRoot checkedPrime7 checked6 2
+#guard !isPrimitiveRoot checkedPrime7 checked6 7
+#guard isPrimitiveRoot checkedPrime13 checked12 2
+
+#guard (match primitiveRoot? checkedPrime2 checked1 1 with
+  | some (g, c) => g == 1 && c.raw.base == 1 && c.raw.modulus == 2 &&
+      c.raw.order == 1 && checkOrder c.raw
+  | none => false)
+
+#guard (primitiveRoot? checkedPrime7 checked6 0).isNone
+
+#guard (match primitiveRoot? checkedPrime7 checked6 2 with
+  | some (g, c) => g == 3 && c.raw.base == 3 && c.raw.modulus == 7 &&
+      c.raw.order == 6 && checkOrder c.raw
+  | none => false)
+
+#guard (match primitiveRoot? checkedPrime13 checked12 1 with
+  | some (g, c) => g == 2 && c.raw.order == 12 && checkOrder c.raw
+  | none => false)
+
+#guard carmichaelPrimePower ⟨1, .small 2⟩ == 1
+#guard carmichaelPrimePower ⟨6, .small 2⟩ == 16
+#guard carmichaelPrimePower ⟨3, .small 3⟩ == 18
+#guard carmichael checked1 == 1
+#guard carmichael checked30 == 4
+#guard carmichael checked64 == 16
+#guard carmichael checked10800 == 180
+#guard 7 ^ carmichael checked10800 % 10800 == 1
+#guard carmichael checked10800 % orderOf 7 10800 == 0
+
+#guard powerTarget 2 6 .minus == 63
+#guard powerTarget 2 6 .plus == 65
+#guard powerTarget 1 0 .minus == 0
+#guard powerTarget 1 0 .plus == 2
 
 #guard (match cyclotomicSplit? 2 6 .minus with
   | some parts => parts.map (·.value) == [1, 3, 7, 3]
@@ -486,6 +690,9 @@ private def retainedCertInput : Nat := starvedInput * 1000037
   | some parts => parts.map (·.value) == [5, 13]
   | none => false)
 
+#guard (cyclotomicSplit? 1 6 .minus).isNone
+#guard (cyclotomicSplit? 2 0 .plus).isNone
+
 -- The repeated factor `3` in the minus split is merged before checker replay.
 #guard (match factorPowerWithRoute? 2 6 .minus (Rand.ofSeed 1) with
   | .ok (F, _, route) =>
@@ -499,6 +706,19 @@ private def retainedCertInput : Nat := starvedInput * 1000037
         F.raw.factors.map (fun e => (e.prime, e.exponent)) == [(5, 1), (13, 1)]
   | .error _ => false)
 
+#guard (match factorPower? 2 6 .minus (Rand.ofSeed 1) with
+  | .ok (F, _) =>
+      F.raw.factors.map (fun e => (e.prime, e.exponent)) == [(3, 2), (7, 1)]
+  | .error _ => false)
+
+#guard (match factorPower? 2 0 .plus (Rand.ofSeed 1) with
+  | .ok (F, _) => F.raw.subject == 2 && checkFactorization F.raw
+  | .error _ => false)
+
+#guard (match factorPower? 100003 4 .minus (Rand.ofSeed 1) (fuel := 0) with
+  | .error failure => failure.stop == .incomplete
+  | .ok _ => false)
+
 -- A stopped continuation includes successful earlier-part work and remains
 -- exactly accounted, even when every charged search subtotal happens to be zero.
 #guard (match factorPowerWithRoute? 100003 4 .minus (Rand.ofSeed 1) (fuel := 0) with
diff --git a/conformance/HexIntFactor/EmitFixtures.lean b/conformance/HexIntFactor/EmitFixtures.lean
index 59d2573e6b..fde0c5e92f 100644
--- a/conformance/HexIntFactor/EmitFixtures.lean
+++ b/conformance/HexIntFactor/EmitFixtures.lean
@@ -29,6 +29,9 @@ private def powersJson (entries : List PrimePower) : String :=
   "[" ++ String.intercalate "," (entries.map fun e =>
     "[" ++ toString e.prime ++ "," ++ toString e.exponent ++ "]") ++ "]"
 
+private def natsJson (values : Array Nat) : String :=
+  "[" ++ String.intercalate "," (values.toList.map toString) ++ "]"
+
 private def rejected (context : String) : IO α :=
   throw <| IO.userError (context ++ ": factorization candidate rejected")
 
@@ -57,7 +60,8 @@ private def emitDivisorFns (tag : String) (n : Nat) : IO Unit := do
       | .rejected => rejected case
       | .zero | .incomplete => pure "null"
     | .ok (F, _) =>
-        pure <| "{\"tau\":" ++ toString (numDivisors F) ++
+        pure <| "{\"divisors\":" ++ natsJson (divisors F) ++
+        ",\"tau\":" ++ toString (numDivisors F) ++
         ",\"sigma0\":" ++ toString (sigma F 0) ++
         ",\"sigma1\":" ++ toString (sigma F 1) ++
         ",\"sigma2\":" ++ toString (sigma F 2) ++
diff --git a/conformance/HexIntFactor/PrimalityConformance.lean b/conformance/HexIntFactor/PrimalityConformance.lean
index 074e46d15e..e33df85202 100644
--- a/conformance/HexIntFactor/PrimalityConformance.lean
+++ b/conformance/HexIntFactor/PrimalityConformance.lean
@@ -9,7 +9,24 @@ module
 public meta import HexIntFactor
 public import HexIntFactor
 
-/-! Downstream conformance for the HexIntFactor primality-search adapter. -/
+/-!
+Downstream conformance for the HexIntFactor primality-search adapter.
+
+Oracle: none; this module checks the adapter against the independently
+checker-accepted HexIntFactor aggregate and the HexPrimality consumer boundary.
+Mode: `always`
+Covered operations:
+- `intFactorSearch`, `Internal.primeCertCountedUsing?`, and the registered
+  `HexIntFactor.PrimalityTactic.extension`
+Covered properties:
+- complete and partial aggregates preserve factors, residual, attempt totals,
+  and random state across the untrusted adapter boundary
+- extension dispatch resumes from the core route's terminal state and emitted
+  proof terms replay `checkPrime`
+Covered edge cases:
+- zero factor fuel, core exhaustion, an 81-bit perfect-power witness, and a
+  composite input with a stable Miller--Rabin diagnostic
+-/
 
 open Hex Hex.Nat
 
diff --git a/libraries.yml b/libraries.yml
index 1818c942cf..11bd2f042e 100644
--- a/libraries.yml
+++ b/libraries.yml
@@ -681,7 +681,7 @@ libraries:
   HexIntFactor:
     deps: [HexPrimality, HexArith, HexBasic]
     mathlib: false
-    done_through: 0
+    done_through: 3
     status: active
     phase4:
       comparators:
@@ -879,7 +879,8 @@ libraries:
   HexIntFactorMathlib:
     deps: [HexIntFactor, HexPrimalityMathlib]
     mathlib: true
-    done_through: 0
+    correspondence_only: true
+    done_through: 3
     status: active
   HexBerlekampZassenhausMathlib:
     deps: [HexBerlekampZassenhaus, HexBerlekampMathlib, HexHenselMathlib, HexPolyZMathlib, HexMatrixMathlib, HexLLLMathlib]
diff --git a/scripts/check_dag.py b/scripts/check_dag.py
index aaaa075770..5836902227 100644
--- a/scripts/check_dag.py
+++ b/scripts/check_dag.py
@@ -370,7 +370,10 @@ def check_correspondence_only(root: Path, libraries, lakefile: Path) -> list[str
                             f"{name} names computational conformance owner {owner} "
                             "without a core conformance module"
                         )
-                else:
+                # Phase 3 requires the owner declaration, while the owner's
+                # headline report becomes evidence only at the bridge's
+                # Phase-4 exit.
+                elif info.done_through >= 4:
                     owner_slug = Path(pascal_to_spec_path(owner)).stem
                     owner_report = root / "reports" / f"{owner_slug}-performance.md"
                     if not owner_report.is_file():
diff --git a/scripts/oracle/intfactor_pari.py b/scripts/oracle/intfactor_pari.py
index 86bd0ff263..bfe890cdc1 100644
--- a/scripts/oracle/intfactor_pari.py
+++ b/scripts/oracle/intfactor_pari.py
@@ -55,14 +55,16 @@ def _factors(pari, n: int) -> list[list[int]] | str:
     return answer
 
 
-def _divisor_functions(pari, n: int) -> dict[str, int]:
+def _divisor_functions(pari, n: int) -> dict[str, int | list[int]]:
     factors = _factors(pari, n)
     assert isinstance(factors, list)
+    divisors = [int(d) for d in pari.divisors(n)]
     radical = math.prod(p for p, _ in factors)
     sqfpart = math.prod(p for p, e in factors if e % 2 == 1)
     sqdiv = math.prod(p ** (e // 2) for p, e in factors)
     return {
-        "tau": len(pari.divisors(n)),
+        "divisors": divisors,
+        "tau": len(divisors),
         "sigma0": int(pari.sigma(n, 0)),
         "sigma1": int(pari.sigma(n)),
         "sigma2": int(pari.sigma(n, 2)),
diff --git a/scripts/test_check_dag.py b/scripts/test_check_dag.py
index 195eb50463..06300d2363 100644
--- a/scripts/test_check_dag.py
+++ b/scripts/test_check_dag.py
@@ -195,14 +195,17 @@ def test_registry_rejects_incompatible_classification(self) -> None:
                 with self.assertRaisesRegex(ValueError, message):
                     load_libraries(manifest)
 
-    def correspondence_tree(self, root: Path) -> OrderedDict[str, LibraryInfo]:
+    def correspondence_tree(
+        self, root: Path, *, bridge_phase: int = 4, owner_report: bool = True
+    ) -> OrderedDict[str, LibraryInfo]:
         (root / "lakefile.lean").write_text("", encoding="utf-8")
         core_conformance = root / "conformance" / "HexCore"
         core_conformance.mkdir(parents=True)
         (core_conformance / "Conformance.lean").write_text("", encoding="utf-8")
         reports = root / "reports"
         reports.mkdir()
-        (reports / "hex-core-performance.md").write_text("", encoding="utf-8")
+        if owner_report:
+            (reports / "hex-core-performance.md").write_text("", encoding="utf-8")
         spec_dir = root / "HexBridge" / "SPEC"
         spec_dir.mkdir(parents=True)
         (spec_dir / "hex-bridge.md").write_text(
@@ -215,12 +218,33 @@ def correspondence_tree(self, root: Path) -> OrderedDict[str, LibraryInfo]:
         return OrderedDict(
             HexCore=LibraryInfo("HexCore", (), False, 4, "active"),
             HexBridge=LibraryInfo(
-                "HexBridge", ("HexCore",), True, 4, "active",
+                "HexBridge", ("HexCore",), True, bridge_phase, "active",
                 correspondence_only=True,
             ),
         )
 
-    def test_repository_state_accepts_clean_classification(self) -> None:
+    def test_phase3_accepts_performance_owner_without_report(self) -> None:
+        with tempfile.TemporaryDirectory() as directory:
+            root = Path(directory)
+            libraries = self.correspondence_tree(
+                root, bridge_phase=3, owner_report=False
+            )
+            self.assertEqual(
+                check_correspondence_only(root, libraries, root / "lakefile.lean"), []
+            )
+
+    def test_phase4_rejects_performance_owner_without_report(self) -> None:
+        with tempfile.TemporaryDirectory() as directory:
+            root = Path(directory)
+            libraries = self.correspondence_tree(root, owner_report=False)
+            errors = check_correspondence_only(
+                root, libraries, root / "lakefile.lean"
+            )
+            self.assertTrue(
+                any("without a headline report" in error for error in errors), errors
+            )
+
+    def test_phase4_accepts_performance_owner_with_report(self) -> None:
         with tempfile.TemporaryDirectory() as directory:
             root = Path(directory)
             libraries = self.correspondence_tree(root)
diff --git a/status/hex-int-factor-mathlib.scaffolding-reviewed b/status/hex-int-factor-mathlib.scaffolding-reviewed
new file mode 100644
index 0000000000..44e20eba1f
--- /dev/null
+++ b/status/hex-int-factor-mathlib.scaffolding-reviewed
@@ -0,0 +1,24 @@
+HexIntFactorMathlib/SPEC/hex-int-factor-mathlib.md was authored in this package
+to record the existing public correspondence API and its runtime boundary.
+An independent Phase 2 skeptical reviewer then checked that explicit contract
+against the source, the Mathlib APIs it transports, and downstream needs after
+the checker projection, canonical factor-list, divisor, squarefree, and general
+order correspondence blockers were resolved. Both direct dependencies have
+completed Phase 1, and every implemented declaration has the intended
+signature and proof route.
+
+The review checked pointwise multiplicity and canonical prime-list agreement,
+zero multiplicity outside the listed prime support, checked-data corollaries,
+divisor enumeration and count, totient, generalized divisor sum, prime
+support, radical and squarefree transports, the general
+natural-order/unit-order correspondence, its nonunit case, and the checked
+certificate specialization. The bridge performs no factor or order search,
+replays no certificate, installs no competing decision instance, and owns no
+reifier, tactic, oracle wrapper, conformance target, benchmark, or proof probe.
+Its explicit correspondence-only classification names `HexIntFactor` as the
+computational conformance and performance owner.
+
+Every advertised declaration has its intended body and route. No data-level
+placeholder, duplicate instance, axiom, sorry, `native_decide`, forbidden
+scaffold wording, or untracked executable surface remains. Phase 3 and later
+acceptance are not attested by this token.
diff --git a/status/hex-int-factor.scaffolding-reviewed b/status/hex-int-factor.scaffolding-reviewed
new file mode 100644
index 0000000000..7ed1b5e6c3
--- /dev/null
+++ b/status/hex-int-factor.scaffolding-reviewed
@@ -0,0 +1,29 @@
+Phase 1 completion and an independent Phase 2 skeptical review were recorded
+against HexIntFactor/SPEC/hex-int-factor.md after all certificate, arithmetic,
+route, correspondence-boundary, and attempt-accounting blockers were resolved.
+Every direct dependency has completed Phase 1, and every implemented SPEC
+declaration has the intended signature and body.
+
+The review checked bounded complete and partial certificate replay, canonical
+prime support and multiplicity, factor-derived divisor functions, generalized
+divisor sums, totient and square decomposition, exact order certificates,
+primitive-root search, and Carmichael exponents. It also checked structural
+reductions on every recursive cofactor, complete perfect-power detection,
+table trial division, genuinely batched Brent rho, outcome-sensitive Pollard
+p-minus-one and ECM scheduling, corrected projective ECM arithmetic with a
+real word backend, single-pass cyclotomic splitting, checked aggregate
+acceptance, scoped rejection diagnostics, and exact successful and failing
+attempt totals.
+
+The current-main re-audit additionally checked the explicitly budgeted
+`factorCountedWith?` and rho adapters, the downstream `intFactorSearch`
+projection of checker-accepted complete and partial aggregates, and the
+versioned primality elaborator registration. The adapter remains an untrusted
+producer: its consumer constructs fresh prime certificates and accepts only
+after replaying `checkPrime`.
+
+Every advertised declaration has its intended body and route, and every search
+result crosses a complete or partial checker before entering the trusted API.
+No data-level placeholder, fake extern, native-type detour, axiom, sorry,
+`native_decide`, forbidden scaffold wording, or untracked implemented-surface
+gap remains. Phase 3 and later acceptance are not attested by this token.