doc: progress note for the hex-roots implementation session

progress/20260711T190000Z.md

@@ -0,0 +1,52 @@
+**Accomplished**
+
+Took hex-roots from `status: planned` to Phase 3 complete plus full
+Phase-4 scaffolding and measurement, in 19 merged PRs (#8705, #8708,
+#8711, #8712, #8713, #8717, #8718, #8720, #8722, #8723, #8726, #8728,
+#8732, #8737, #8740, #8743, #8746, #8747, #8749), each implemented by
+an Opus subagent or directly, each Codex-reviewed before merge.
+Highlights beyond the Phase-1 note (20260711T135500Z):
+
+- Phase 2: three-reader skeptical review; fixes in #8732 (fuel-seed
+  bug, DFS relabel) plus the downstream API the review demanded:
+  `RefinedIsolation.refineTo?` with the root-identity proof via
+  `Quot.sound`, `toRefined?`, `certifyAtom?`, and the ball API
+  (`toBall`, `evalBall`, `excludesZero`, `meets`).
+- Phase 3: core conformance (#8737, twelve operations, bidirectional
+  cross-strategy matching) and the python-flint oracle (#8740,
+  14 fixtures, rigorous arb comparisons). The conformance work
+  exposed three real driver defects, fixed in #8743: worklist
+  re-entry lost roots lying in the certified disc but outside the
+  retained square (Mignotte's three large roots vanished); exact
+  Newton recentring compounded centre bit-length by ~2·deg per jump
+  (30k-digit centres by the fourth jump at degree 4, a 41-minute
+  Nat.pow panic); ready components kept doubling precision while
+  waiting for laggards. Post-fix: acceptance suite 2.2 s, degree-20
+  isolateAll? ~15 s (from hours).
+- Phase 4: bench module (#8747, 14 registrations incl. the
+  three-strategy compare group, which AGREES on the shared domain;
+  pellet/nk wall ratio 0.66→0.45 on integer-root families) and the
+  measurement PR (#8749): 4 consistent / 9 inconclusive verdicts,
+  2 of 3 SPEC time budgets fail (deg50@64 49.6× over; deg100@128
+  DNF), so `done_through` honestly stays 3 with Concerns populated.
+
+**Current frontier**
+
+hex-roots: `done_through: 3`, `scaffolding-reviewed` token committed,
+Phase-4 artefacts (bench, report, comparator data, phase4 metadata)
+on main, exit blocked by the two named findings.
+
+**Next step**
+
+Issues #8750 (bench re-scaffolding: smooth-difficulty driver family,
+wider compare schedule, integer Taylor centre, microsecond-band prep)
+and #8751 (deep-target performance: Graeffe iteration per the SPEC's
+deferred-optimisation note, or a time-budget re-appraisal). Also open:
+#8730 (taylor characterization lemma), #8731 (invFloor/invAtPrec
+bridge), #8744 (degree-20 fixture tier). Then hex-roots-mathlib,
+whose critical path the NK route reduces to Banach + Mahler.
+
+**Blockers**
+
+Phase-4 exit criteria (consistent verdicts, empty Concerns) are not
+met; tracked in #8750/#8751 rather than worked around.