diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 2cec43c90..20e5a3a8b 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -131,7 +131,7 @@ jobs:
       - name: Define the hex-dev cache + build target sets
         run: |
           echo "HEX_LIB_TARGETS=HexBasic HexArith HexPoly HexModArith HexGF2 HexPolyZ HexRoots HexPolyFp HexGFqRing HexGFqField HexBerlekamp HexHensel HexConway HexGFq HexBerlekampZassenhaus HexRealRoots HexMatrix HexRowReduce HexDeterminant HexBareiss HexGramSchmidt HexLLL HexMatrixMathlib HexGramSchmidtMathlib HexLLLMathlib HexBerlekampZassenhausMathlib HexRealRootsMathlib" >> "$GITHUB_ENV"
-          echo "HEX_EXE_TARGETS=hexarith_bench hexpoly_bench hexpolyz_bench hexpolyfp_bench hexmodarith_bench hexgf2_bench hexgfqring_bench hexgfqfield_bench hexgfq_bench hexhensel_bench hexberlekamp_bench hexbz_bench hexconway_bench hexmatrix_bench hexdeterminant_bench hexbareiss_bench hexgramschmidt_bench hexrealroots_bench hexlll_bench hexlll_provider_probe" >> "$GITHUB_ENV"
+          echo "HEX_EXE_TARGETS=hexarith_bench hexpoly_bench hexpolyz_bench hexpolyfp_bench hexmodarith_bench hexgf2_bench hexgfqring_bench hexgfqfield_bench hexgfq_bench hexhensel_bench hexberlekamp_bench hexbz_bench hexconway_bench hexmatrix_bench hexdeterminant_bench hexbareiss_bench hexgramschmidt_bench hexrealroots_bench hexroots_bench hexlll_bench hexlll_provider_probe" >> "$GITHUB_ENV"
       # Shared build. The libraries, bench exes, conformance #guard drivers, and
       # emit-fixture exes are all elaborated here so the two verification tails
       # below only *run* things, never rebuild them -- which is what lets the
@@ -207,7 +207,7 @@ jobs:
             hexgf2_bench hexgfqring_bench hexgfqfield_bench hexgfq_bench \
             hexhensel_bench hexberlekamp_bench hexbz_bench \
             hexconway_bench hexdeterminant_bench hexmatrix_bench \
-            hexrealroots_bench
+            hexrealroots_bench hexroots_bench
           touch "$RUNNER_TEMP/bench.ok"
       - name: Conformance oracles + BZ gates
         id: conformance
diff --git a/bench/HexRoots/Bench.lean b/bench/HexRoots/Bench.lean
new file mode 100644
index 000000000..abc253244
--- /dev/null
+++ b/bench/HexRoots/Bench.lean
@@ -0,0 +1,588 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+
+import HexRoots
+import LeanBench
+
+/-!
+Phase 4 benchmark registrations for `hex-roots`.
+
+This module is the Phase 4 benchmark root for the certified complex-root
+isolation API. It covers the exact Gaussian-dyadic primitives (`taylor`, the
+two atom-witness checks, the speculative Newton step), the separation-precision
+helper (`mahlerPrec`), the refinement primitives (`Component.refine1`,
+`Component.certify?`), the end-to-end drivers (`isolateAll?`, `isolate`), the
+refined-threading operation (`DyadicRootIsolation.refineTo?`), and the
+root-identity test (`RefinedIsolation.sameRoot`). It also registers the
+dual-route atom-certificate experiment as a `compare` group: `isolate` under
+`.nk`, `.pellet`, and `.nkThenPellet` on one shared deterministic domain,
+joined on a strategy-invariant projection of the isolation output.
+
+Two deterministic input families are used, each keyed by the benchmark
+parameter (its degree):
+
+* `seededPoly d` — a dense integer polynomial with coefficients in `[-10, 10]`
+  drawn from the same seed-`0xC0FFEE` LCG the conformance ci-tier fixtures use
+  (`conformance/HexRoots/EmitFixtures.lean`). Its roots are generically
+  irrational and distinct, so isolation exercises subdivision to the separation
+  depth rather than short-circuiting. Used by `taylor`, `mahlerPrec`, the
+  refinement primitives, and the two whole-polynomial drivers.
+* `linProdPoly d = ∏_{j=1}^{d} (X − j)` — a Wilkinson-shaped product of distinct
+  monic linear factors with the integer roots `1, …, d`. Newton recentres onto
+  an integer root exactly, so the certified centres are exact integers; this is
+  what makes the `compare` group's strategy-invariant hash agree across the
+  three strategies (the atoms' stored squares differ, but the integer-grid
+  projection of their centres does not). Also used for the witness-check and
+  Newton-step registrations, whose squares are centred on the integer root `1`
+  of the family.
+
+The declared complexity models are the textbook *exact-dyadic-operation counts*
+from `HexRoots/SPEC/hex-roots.md § Complexity contract`. They do not fold in the
+working bit-length `B = prec + n·log‖p‖∞`, which grows with the parameter; the
+scientific wall-time verdicts and their reconciliation against these op-count
+models are a scheduled-hardware concern (as for the other Phase 4 benches),
+not a merge-gating one. The `verify` smoke gate only exercises each
+registration at parameters `0` and `1`.
+
+Registrations (each with an adjacent cost-model derivation comment):
+
+* `runTaylor` — exact Taylor shift, `O(n²)`.
+* `runWitnessCheck`, `runNkWitnessCheck` — Pellet and Newton-Kantorovich atom
+  witnesses, `O(n²)` (Taylor shift dominates).
+* `runMahlerPrec` — separation precision, `O(n · log‖p‖∞)`.
+* `runNewtonSquare` — speculative Newton step, `O(n²)`.
+* `runRefine1`, `runCertify` — one subdivision round and one certification
+  attempt on a mid-refinement component, `O(n²)`.
+* `runIsolateAll` — `isolateAll?` at target `32`, `O(n³)`.
+* `runIsolate` — `isolate` to the `separationDepth` floor, `O(n³)`.
+* `runRefineTo` — `DyadicRootIsolation.refineTo?` from `≈32` to a parametric
+  target `t`, `O(t²)`.
+* `runSameRoot` — `RefinedIsolation.sameRoot`, a single dyadic comparison
+  (fixed benchmark, microseconds).
+* `runIsolateNk`, `runIsolatePellet`, `runIsolateNkThenPellet` — the `compare`
+  group over `linProdPoly`; all three must agree on the strategy-invariant hash.
+-/
+
+namespace Hex.RootsBench
+
+open Hex
+
+/-! ### Deterministic input families -/
+
+/-- The LCG step from `conformance/HexRoots/EmitFixtures.lean`
+(`6364136223846793005·s + 1442695040888963407 mod 2^64`, realised as `UInt64`
+wraparound). -/
+def lcgNext (s : UInt64) : UInt64 := 6364136223846793005 * s + 1442695040888963407
+
+/-- The seed-`0xC0FFEE` coefficient stream: `degree + 1` coefficients in
+`[-10, 10]` (constant term first), with the leading coefficient forced nonzero
+so the polynomial has the requested degree. Matches the ci-tier fixture
+generator. -/
+def seededCoeffs (degree : Nat) : Array Int := Id.run do
+  let mut s : UInt64 := 0xC0FFEE
+  let mut out : Array Int := Array.mkEmpty (degree + 1)
+  for _ in [0:degree + 1] do
+    s := lcgNext s
+    out := out.push (Int.ofNat (s.toNat % 21) - 10)
+  if out[degree]! == 0 then
+    out := out.set! degree 1
+  return out
+
+/-- A dense integer polynomial of degree `degree` with bounded pseudo-random
+coefficients (see `seededCoeffs`). -/
+def seededPoly (degree : Nat) : ZPoly := DensePoly.ofCoeffs (seededCoeffs degree)
+
+/-- The monic linear factor `X − root`. -/
+def linearFactor (root : Int) : ZPoly := DensePoly.ofCoeffs #[-root, 1]
+
+/-- `∏_{j=1}^{degree} (X − j)`, a Wilkinson-shaped polynomial with the distinct
+integer roots `1, …, degree`. Empty product `1` at `degree = 0`. -/
+def linProdPoly (degree : Nat) : ZPoly :=
+  (Array.range degree).foldl
+    (fun acc i => acc * linearFactor (Int.ofNat (i + 1)))
+    (1 : ZPoly)
+
+/-- The fixed Gaussian-dyadic centre `1/4 + (1/8)·i` used by the `taylor`
+benchmark: a nonzero dyadic point so the shift exercises every synthetic-
+division pass. -/
+def taylorCentre : GaussDyadic := (Dyadic.ofIntWithPrec 1 2, Dyadic.ofIntWithPrec 1 3)
+
+/-- A square of half-width `2^{−12}` centred on the integer root `1` of
+`linProdPoly`, used by the witness-check and Newton-step benchmarks. At this
+radius the isolation ratio to the nearest sibling root (distance `1`) is far
+inside the witness's firing threshold for every scheduled degree. -/
+def rootSquare : DyadicSquare := ⟨Dyadic.ofInt 1, 0, 12⟩
+
+/-! ### Result checksums (stable observables) -/
+
+/-- Stable observable for a dyadic number: its exact reduced rational. -/
+def dyadicChecksum (d : Dyadic) : UInt64 :=
+  let q := d.toRat
+  mixHash (hash q.num) (hash (q.den : Int))
+
+/-- Stable observable for a Gaussian dyadic. -/
+def gaussChecksum (z : GaussDyadic) : UInt64 :=
+  mixHash (dyadicChecksum z.1) (dyadicChecksum z.2)
+
+/-- Stable observable for an array of Gaussian dyadics (the `taylor` output). -/
+def gaussArrayChecksum (zs : Array GaussDyadic) : UInt64 :=
+  zs.foldl (fun acc z => mixHash acc (gaussChecksum z)) (hash zs.size)
+
+/-- Stable observable for a dyadic square. -/
+def squareChecksum (s : DyadicSquare) : UInt64 :=
+  mixHash (mixHash (dyadicChecksum s.re) (dyadicChecksum s.im)) (hash s.prec)
+
+/-- Stable observable for a certification result: its stored square plus the
+atom/cluster tag and root count. -/
+def certifiedChecksum {p : ZPoly} (c : Certified p) : UInt64 :=
+  let tag : Nat := match c with | .atom _ => 1 | .cluster cl => cl.k
+  mixHash (squareChecksum c.square) (hash tag)
+
+/-- Stable observable for an optional certification result. -/
+def optionCertifiedChecksum {p : ZPoly} : Option (Certified p) → UInt64
+  | none => 0
+  | some c => mixHash 1 (certifiedChecksum c)
+
+/-- Stable observable for an array of certification results. -/
+def certifiedArrayChecksum {p : ZPoly} (rs : Array (Certified p)) : UInt64 :=
+  rs.foldl (fun acc c => mixHash acc (certifiedChecksum c)) (hash rs.size)
+
+/-- Stable observable for an array of components (the `refine1` output). -/
+def componentsChecksum (cs : Array Component) : UInt64 :=
+  cs.foldl (fun acc c => mixHash acc (c.squares.foldl
+    (fun a s => mixHash a (squareChecksum s)) (hash c.candidateK))) (hash cs.size)
+
+/-! ### `Hashable` instances for benchmark input types
+
+`setup_benchmark` records a hash of the prepared input alongside each JSONL row.
+`ZPoly`, `DyadicSquare`, `Component`, and `DyadicRootIsolation` carry no derived
+`Hashable`, so the instances below route through the exact-rational observables
+above; product and option inputs then derive automatically. -/
+
+instance : Hashable ZPoly where hash p := hash p.toArray
+
+instance : Hashable DyadicSquare where hash := squareChecksum
+
+instance : Hashable Component where
+  hash c := c.squares.foldl (fun a s => mixHash a (squareChecksum s)) (hash c.candidateK)
+
+instance {p : ZPoly} : Hashable (DyadicRootIsolation p) where
+  hash iso := squareChecksum iso.square
+
+/-! ### Strategy-invariant projection for the `compare` group
+
+The three strategies isolate the same integer roots but store different squares
+(different precisions, sometimes off-by-one levels). The projection below is
+invariant across strategies on `linProdPoly`: it records the atom count and the
+multiset of atom centres rounded to the NEAREST INTEGER. The compare family's
+roots are integers and every strategy's certified centre lies within the
+stored square's radius of its root, far below `1/2`, so the rounding is
+robust to the strategies' differing squares and precisions (a finer grid
+would put bucket boundaries near non-integer centres and break invariance;
+this digest is only meaningful for integer-root families). The `compare`
+gate is exactly that agreement. -/
+
+/-- Round a dyadic to the nearest integer (`⌊x⌉`). -/
+def gridBucket (d : Dyadic) : Int := (d.toRat + (1 : Rat) / 2).floor
+
+/-- Lexicographic order on integer-grid buckets, for a deterministic multiset
+digest. -/
+def bucketLe (a b : Int × Int) : Bool :=
+  if a.1 = b.1 then a.2 ≤ b.2 else a.1 < b.1
+
+/-- Strategy-invariant digest of an isolation output: the atom count mixed with
+the sorted multiset of integer-grid centre buckets. -/
+def rootsDigest {p : ZPoly} (atoms : Array (DyadicRootIsolation p)) : UInt64 :=
+  let buckets := (atoms.map fun iso =>
+    (gridBucket iso.square.re, gridBucket iso.square.im)).qsort bucketLe
+  buckets.foldl (fun acc b => mixHash (mixHash acc (hash b.1)) (hash b.2))
+    (hash atoms.size)
+
+/-! ### Mid-refinement component fixture -/
+
+/-- A representative mid-refinement component of `seededPoly degree`: two
+`refine1` rounds down from `Component.cauchy`, keeping the first surviving
+component (a subdivided region localised near a root). Falls back to the Cauchy
+square when the degree is degenerate or every child was `T₀`-discarded. -/
+def midComponent (degree : Nat) : ZPoly × Component :=
+  let p := seededPoly degree
+  if h : 0 < p.degree?.getD 0 then
+    let start := Component.cauchy p h
+    let round1 := start.refine1 p
+    let round2 := round1.flatMap (·.refine1 p)
+    (p, (round2[0]?.orElse fun _ => round1[0]?).getD start)
+  else
+    (p, ⟨#[⟨0, 0, 0⟩], 0⟩)
+
+/-! ### Refined-atom fixture for `refineTo?` and `sameRoot` -/
+
+/-- A small fixed polynomial with distinct simple roots for the refined-atom
+fixtures: `(x−1)(x−2)(x+3)`. -/
+def refinePoly : ZPoly := DensePoly.ofCoeffs #[6, -7, 0, 1]
+
+/-- One atom of `refinePoly`, isolated to (at least) the separation depth. The
+`refineTo?` benchmark sharpens this atom; the `sameRoot` benchmark compares its
+refined form against itself. `none` never occurs for this squarefree fixture. -/
+def refineAtom? : Option (DyadicRootIsolation refinePoly) :=
+  if h : HasOnlySimpleRoots refinePoly then
+    match isolate refinePoly h 0 with
+    | some atoms => atoms[0]?
+    | none => none
+  else none
+
+/-- The refined-isolation form of `refineAtom?`, meeting the separation
+precision required by `RefinedIsolation`. -/
+def refinedAtom? : Option (RefinedIsolation refinePoly) :=
+  refineAtom?.bind DyadicRootIsolation.toRefined?
+
+/-! ### Benchmark targets -/
+
+/-- Benchmark target: exact Gaussian-dyadic Taylor shift at the fixed centre. -/
+def runTaylor (p : ZPoly) : UInt64 :=
+  gaussArrayChecksum (taylor p taylorCentre)
+
+/-- Benchmark target: Pellet atom witness (`k = 1`) on the root-centred square. -/
+def runWitnessCheck (p : ZPoly) : UInt64 :=
+  hash (witnessCheck p rootSquare 1)
+
+/-- Benchmark target: Newton-Kantorovich atom witness on the root-centred square. -/
+def runNkWitnessCheck (p : ZPoly) : UInt64 :=
+  hash (nkWitnessCheck p rootSquare)
+
+/-- Benchmark target: closed-form separation precision. -/
+def runMahlerPrec (p : ZPoly) : UInt64 :=
+  hash (mahlerPrec p)
+
+/-- Benchmark target: one speculative Newton step from the root-centred square. -/
+def runNewtonSquare (p : ZPoly) : UInt64 :=
+  squareChecksum (newtonSquare p rootSquare 1)
+
+/-- Benchmark target: one subdivision round on a mid-refinement component. -/
+def runRefine1 (pc : ZPoly × Component) : UInt64 :=
+  componentsChecksum (pc.2.refine1 pc.1)
+
+/-- Benchmark target: one certification attempt on a mid-refinement component. -/
+def runCertify (pc : ZPoly × Component) : UInt64 :=
+  optionCertifiedChecksum (Component.certify? pc.1 .nkThenPellet pc.2)
+
+/-- Benchmark target: `isolateAll?` at target precision `32`. -/
+def runIsolateAll (p : ZPoly) : UInt64 :=
+  if h : 0 < p.degree?.getD 0 then
+    match isolateAll? p 32 #[Component.cauchy p h] with
+    | some rs => certifiedArrayChecksum rs
+    | none => 0
+  else 0
+
+/-- Isolate `p` under `strategy` and digest the output with the
+strategy-invariant projection; `0` for non-squarefree or degenerate inputs. -/
+def isolateDigest (strategy : AtomStrategy) (p : ZPoly) : UInt64 :=
+  if h : HasOnlySimpleRoots p then
+    match isolate p h 0 strategy with
+    | some atoms => rootsDigest atoms
+    | none => 0
+  else 0
+
+/-- Benchmark target: `isolate` to the `separationDepth` floor (`atom_prec = 0`). -/
+def runIsolate (p : ZPoly) : UInt64 :=
+  isolateDigest .nkThenPellet p
+
+/-- Compare-group target: `isolate` under the Newton-Kantorovich-only strategy. -/
+def runIsolateNk (p : ZPoly) : UInt64 :=
+  isolateDigest .nk p
+
+/-- Compare-group target: `isolate` under the Pellet-only strategy. -/
+def runIsolatePellet (p : ZPoly) : UInt64 :=
+  isolateDigest .pellet p
+
+/-- Compare-group target: `isolate` under the default `nkThenPellet` strategy. -/
+def runIsolateNkThenPellet (p : ZPoly) : UInt64 :=
+  isolateDigest .nkThenPellet p
+
+/-- Benchmark target: sharpen a fixed `≈32`-precision atom to a parametric
+target precision. The prepared `σ` carries the fixed atom and the requested
+target so the atom construction stays out of the timed loop. -/
+def runRefineTo (input : Option (DyadicRootIsolation refinePoly) × Int) : UInt64 :=
+  match input.1 with
+  | some iso =>
+    match iso.refineTo? input.2 with
+    | some iso' => squareChecksum iso'.square
+    | none => 0
+  | none => 0
+
+/-- Per-parameter fixture for `runRefineTo`: the fixed refined atom paired with
+the target precision the parameter encodes. -/
+def prepRefineTo (target : Nat) : Option (DyadicRootIsolation refinePoly) × Int :=
+  (refineAtom?, (target : Int))
+
+/-! ### `taylor` / `mahlerPrec` : dense seeded family -/
+
+/-
+`taylor` produces `p(X + z) = Σ cₖ Xᵏ` by repeated synthetic division: the
+`k`-indexed outer pass runs an inner Horner sweep of length `n − 1 − k`, so the
+total is `Σ_k (n − 1 − k) = O(n²)` exact Gaussian-dyadic multiply/adds. Degree
+`n` is the benchmark parameter, so the op-count model is `n²`.
+-/
+setup_benchmark runTaylor n => n * n
+  with prep := seededPoly
+  where {
+    paramFloor := 16
+    paramCeiling := 256
+    paramSchedule := .custom #[16, 32, 64, 128, 256]
+    maxSecondsPerCall := 4.0
+    targetInnerNanos := 100000000
+    signalFloorMultiplier := 1.0
+  }
+
+/-
+`mahlerPrec` evaluates the closed-form Mahler/Landau separation bound: a fixed
+number of `ceilLog2` calls plus integer multiplies over the degree `n` and the
+coefficient-norm `log‖p‖∞`. The SPEC contract is `O(n · log‖p‖∞)`; the seeded
+family holds `‖p‖∞ ≤ 10` fixed, so the `log‖p‖∞` factor is a constant over this
+schedule and the op-count model reduces to linear in `n`.
+-/
+setup_benchmark runMahlerPrec n => n
+  with prep := seededPoly
+  where {
+    paramFloor := 16
+    paramCeiling := 256
+    paramSchedule := .custom #[16, 32, 64, 128, 256]
+    maxSecondsPerCall := 2.0
+    targetInnerNanos := 100000000
+    signalFloorMultiplier := 1.0
+  }
+
+/-! ### witness checks / Newton step : root-centred `linProdPoly` -/
+
+/-
+`witnessCheck` computes the exact Taylor coefficients at the square's centre
+(the `O(n²)` shift, which dominates) and then, for each of the three test
+radii, a single `O(n)` fold over the coefficients. The op-count model is `n²`.
+The square is centred on the integer root `1` of `linProdPoly`, so the witness
+actually fires at every scheduled degree.
+-/
+setup_benchmark runWitnessCheck n => n * n
+  with prep := linProdPoly
+  where {
+    paramFloor := 2
+    paramCeiling := 16
+    paramSchedule := .custom #[2, 4, 6, 8, 10, 12, 16]
+    maxSecondsPerCall := 4.0
+    targetInnerNanos := 100000000
+    signalFloorMultiplier := 1.0
+  }
+
+/-
+`nkWitnessCheck` has the same `O(n²)` Taylor-shift-dominated shape as
+`witnessCheck`, plus one `Dyadic.invAtPrec` reciprocal and a single `O(n)`
+radial-Lipschitz fold. Op-count model `n²`, root-centred on `linProdPoly`.
+-/
+setup_benchmark runNkWitnessCheck n => n * n
+  with prep := linProdPoly
+  where {
+    paramFloor := 2
+    paramCeiling := 16
+    paramSchedule := .custom #[2, 4, 6, 8, 10, 12, 16]
+    maxSecondsPerCall := 4.0
+    targetInnerNanos := 100000000
+    signalFloorMultiplier := 1.0
+  }
+
+/-
+`newtonSquare` computes the Taylor coefficients at the centre (the `O(n²)`
+shift), reads `c₀, c₁`, and does one `Dyadic.invAtPrec` reciprocal plus a
+constant amount of Gaussian-dyadic arithmetic. The Taylor shift dominates, so
+the op-count model is `n²`.
+-/
+setup_benchmark runNewtonSquare n => n * n
+  with prep := linProdPoly
+  where {
+    paramFloor := 2
+    paramCeiling := 16
+    paramSchedule := .custom #[2, 4, 6, 8, 10, 12, 16]
+    maxSecondsPerCall := 4.0
+    targetInnerNanos := 100000000
+    signalFloorMultiplier := 1.0
+  }
+
+/-! ### refinement primitives : mid-refinement component of the seeded family -/
+
+/-
+`refine1` subdivides each square of the component four ways and runs the `T₀`
+`rootFree` exclusion — one Taylor shift, `O(n²)` — on each child, then glues the
+survivors. For a component of a bounded number of squares this is a bounded
+number of `O(n²)` shifts, so the op-count model is `n²` in the polynomial
+degree `n`.
+-/
+setup_benchmark runRefine1 n => n * n
+  with prep := midComponent
+  where {
+    paramFloor := 4
+    paramCeiling := 12
+    paramSchedule := .custom #[4, 6, 8, 10, 12]
+    maxSecondsPerCall := 4.0
+    targetInnerNanos := 100000000
+    signalFloorMultiplier := 1.0
+  }
+
+/-
+`certify?` under the default `nkThenPellet` strategy first tries the
+Newton-Kantorovich witness on the doubled enclosing square: one
+`nkWitnessCheck` (`O(n²)`) and one speculative `newtonSquare` (`O(n²)`). On a
+mid-refinement component localised near a root this NK path fires, so the
+op-count model is `n²`. (The Pellet fallback, taken only when NK does not fire,
+loops over `k ≤ deg p` and is `O(n³)`; it is not the path this fixture
+measures.)
+-/
+setup_benchmark runCertify n => n * n
+  with prep := midComponent
+  where {
+    paramFloor := 4
+    paramCeiling := 12
+    paramSchedule := .custom #[4, 6, 8, 10, 12]
+    maxSecondsPerCall := 6.0
+    targetInnerNanos := 100000000
+    signalFloorMultiplier := 1.0
+  }
+
+/-! ### whole-polynomial drivers : dense seeded family -/
+
+/-
+`isolateAll?` refines the Cauchy component to disjoint certified atoms at target
+precision `32`. The SPEC heuristic is `O(n³ · B²)` bit operations for degree `n`
+with well-separated roots; the op-count model (dropping the working bit-length
+`B`) is `n³`: up to `O(n)` components, each driven through `O(n)` subdivision
+levels of `O(n²)`-per-witness work amortised by the speculative Newton jumps.
+The seeded family's distinct irrational roots force genuine subdivision, so the
+driver exercises the separation machinery rather than a rational-root
+short-circuit.
+-/
+setup_benchmark runIsolateAll n => n * n * n
+  with prep := seededPoly
+  where {
+    paramFloor := 4
+    paramCeiling := 20
+    paramSchedule := .custom #[4, 6, 8, 10, 12, 14, 16, 18, 20]
+    maxSecondsPerCall := 20.0
+    targetInnerNanos := 100000000
+    signalFloorMultiplier := 1.0
+  }
+
+/-
+`isolate` runs `isolateAll?` from the Cauchy component to
+`max atom_prec (separationDepth p)` and requires every result to be an atom.
+With `atom_prec = 0` the target is the `separationDepth` floor, which grows with
+the degree, so this is the deeper of the two whole-polynomial drivers. Same
+`O(n³)` op-count model as `isolateAll?`. The schedule caps lower (degree `16`)
+because the separation-depth target keeps one full-ladder pass practical there.
+-/
+setup_benchmark runIsolate n => n * n * n
+  with prep := seededPoly
+  where {
+    paramFloor := 4
+    paramCeiling := 16
+    paramSchedule := .custom #[4, 6, 8, 10, 12, 14, 16]
+    maxSecondsPerCall := 30.0
+    targetInnerNanos := 100000000
+    signalFloorMultiplier := 1.0
+  }
+
+/-
+`refineTo?` sharpens a fixed degree-3 atom from precision `≈32` to the parametric
+target `t`. Speculative Newton doubles the precision per accepted jump, so the
+final witness at precision `t` dominates: one `O(n²)`-op Taylor shift on
+`B ≈ t`-bit dyadics, whose schoolbook bit-cost is `O(t²)` at fixed degree. The
+parameter is the target precision, so the model is `t²`.
+-/
+setup_benchmark runRefineTo t => t * t
+  with prep := prepRefineTo
+  where {
+    paramFloor := 64
+    paramCeiling := 256
+    paramSchedule := .custom #[64, 96, 128, 192, 256]
+    maxSecondsPerCall := 4.0
+    targetInnerNanos := 100000000
+    signalFloorMultiplier := 1.0
+  }
+
+/-! ### `compare` group : dual-route atom-certificate experiment
+
+`runIsolateNk`, `runIsolatePellet`, and `runIsolateNkThenPellet` isolate the
+same `linProdPoly` inputs under the three `AtomStrategy` values and digest the
+output with the strategy-invariant `rootsDigest`. On this integer-root family
+all three agree, so `compare runIsolateNk runIsolatePellet runIsolateNkThenPellet`
+reports `allAgreed`; a divergence would be a cross-strategy conformance failure.
+The op-count model is `n³` (each is an `isolate` run), matching the drivers. -/
+
+-- Cost model: one `isolate` run over `linProdPoly n`; n subdivision/adoption
+-- rounds of O(n) witness checks at O(n) ops each (fixed-height family), so
+-- n^3 exact-dyadic operations; the NK-only strategy certifies each atom on its doubled square.
+setup_benchmark runIsolateNk n => n * n * n
+  with prep := linProdPoly
+  where {
+    paramFloor := 2
+    paramCeiling := 6
+    paramSchedule := .custom #[2, 3, 4, 5, 6]
+    maxSecondsPerCall := 8.0
+    targetInnerNanos := 100000000
+    signalFloorMultiplier := 1.0
+  }
+
+-- Cost model: one `isolate` run over `linProdPoly n`; n subdivision/adoption
+-- rounds of O(n) witness checks at O(n) ops each (fixed-height family), so
+-- n^3 exact-dyadic operations; the Pellet-only strategy runs the three-radius test per k candidate.
+setup_benchmark runIsolatePellet n => n * n * n
+  with prep := linProdPoly
+  where {
+    paramFloor := 2
+    paramCeiling := 6
+    paramSchedule := .custom #[2, 3, 4, 5, 6]
+    maxSecondsPerCall := 8.0
+    targetInnerNanos := 100000000
+    signalFloorMultiplier := 1.0
+  }
+
+-- Cost model: one `isolate` run over `linProdPoly n`; n subdivision/adoption
+-- rounds of O(n) witness checks at O(n) ops each (fixed-height family), so
+-- n^3 exact-dyadic operations; the default strategy tries NK first, Pellet as fallback.
+setup_benchmark runIsolateNkThenPellet n => n * n * n
+  with prep := linProdPoly
+  where {
+    paramFloor := 2
+    paramCeiling := 6
+    paramSchedule := .custom #[2, 3, 4, 5, 6]
+    maxSecondsPerCall := 8.0
+    targetInnerNanos := 100000000
+    signalFloorMultiplier := 1.0
+  }
+
+/-! ### `sameRoot` : fixed microsecond benchmark -/
+
+/-- The prebuilt refined-atom pair for the `sameRoot` benchmark, threaded through
+an `IO.Ref` so the single dyadic comparison is not constant-folded away. -/
+initialize sameRootRef :
+    IO.Ref (Option (RefinedIsolation refinePoly × RefinedIsolation refinePoly)) ←
+  IO.mkRef (refinedAtom?.map fun r => (r, r))
+
+/-
+`RefinedIsolation.sameRoot` is a single `DyadicSquare.discsMeet` comparison — a
+handful of exact-dyadic multiplies and one `≤` — so it is a microsecond-scale
+fixed benchmark rather than a parametric sweep. The atoms come from the `IO.Ref`
+above so the harness measures the comparison, not a folded constant.
+-/
+def runSameRoot : Unit → IO UInt64 := fun () => do
+  match ← sameRootRef.get with
+  | some (a, b) => return hash (RefinedIsolation.sameRoot a b)
+  | none => return 0
+
+setup_fixed_benchmark runSameRoot where {
+    repeats := 5
+    expectedHash := some 0xb
+  }
+
+end Hex.RootsBench
+
+def main (args : List String) : IO UInt32 :=
+  LeanBench.Cli.dispatch args
diff --git a/lakefile.lean b/lakefile.lean
index e5a38bf20..d97c5b736 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -235,6 +235,10 @@ lean_exe hexroots_emit_fixtures where
   srcDir := "conformance"
   root := `HexRoots.EmitFixtures
 
+lean_exe hexroots_bench where
+  srcDir := "bench"
+  root := `HexRoots.Bench
+
 lean_exe hexmatrix_bench where
   srcDir := "bench"
   root := `HexMatrix.Bench