diff --git a/progress/20260711T190000Z.md b/progress/20260711T190000Z.md new file mode 100644 index 000000000..146dc59a7 --- /dev/null +++ b/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.