# libraries.yml — per-library structure + state.
#
# Structural fields (deps, mathlib) change rarely, only when the library
# graph changes. State fields (done_through, status) change as libraries
# advance through phases or are activated/deactivated.
#
# Semantics:
# - done_through: K means phases 1..K are all complete for L (linear,
#   no skipping — enforced by the phase-dep table in PLAN/README.md).
# - done_through: 0 means no per-library phases are complete; L is
#   ready to start Phase 1 once Phase 0's global bootstrap is done.
# - done_through: 7 means L is fully done.
# - status: active | planned | draft (see PLAN/Conventions.md
#   §"Library status (active | planned | draft)" for the full
#   semantic contract).
#     - active: orchestrator dispatches Phase work.
#     - planned: SPEC ready, implementation deferred. Lake-alignment
#       and root-file checks waived. Listed in status report footer.
#       Required: done_through == 0.
#     - draft: SPEC incomplete. Same orchestration treatment as planned.
#       Required: done_through == 0.
#   Active libraries depend only on active libraries (load-time invariant).
# - Phase 0 (monorepo bootstrap) is global; its completion is observable
#   by the existence of lakefile.lean, scripts/check_dag.py, etc., not
#   by any field in this file.
# - phase4 (optional, for active libraries planning to reach
#   done_through ≥ 4): structured Phase-4 metadata that mechanical
#   checks read. SPEC text in SPEC/Libraries/<lib>.md carries the
#   narrative; this block carries the machine-readable form.
#     - phase4.comparators: list of named external comparators.
#       Each entry has:
#         tool: <string>          # human-readable tool identifier
#         class: gating | informational
#         goal: <string>          # required when class == gating;
#                                 # the performance goal the headline
#                                 # report measures against this
#                                 # comparator (e.g. "at least as
#                                 # fast as X on shared inputs").
#         rationale: <string>     # required when class == informational;
#                                 # why this comparator does not gate.
#       See SPEC/benchmarking.md §"Comparator classification" and
#       §"Comparator naming".
#     - phase4.input_families: list of named non-degenerate input
#       families the per-library SPEC requires Phase-4 benchmarking
#       to exercise. Each entry has:
#         name: <string>          # short identifier used in profile
#                                 # subsection headings
#         description: <string>   # one-line description matching the
#                                 # per-library SPEC's narrative
#       See SPEC/benchmarking.md §"Anti-patterns" entry on best-case
#       inputs and SPEC/profiling.md §"Coverage requirement".
#
# This file is the single source of truth for the library graph.
# lakefile.lean entries are cross-checked against active libraries.yml
# entries in CI via scripts/check_dag.py.

libraries:

  # ---------- Roots ----------
  HexBasic:
    deps: []
    mathlib: false
    done_through: 7
    status: active
  HexArith:
    deps: []
    mathlib: false
    done_through: 7
    status: active
    phase4:
      input_families:
        - name: modular-multiplication-chain
          description: Repeated Barrett and Montgomery UInt64 modular multiplication over the shared small odd modulus 65537.
        - name: word-powmod
          description: Public modular exponentiation over a fixed odd word-sized modulus with deterministic exponents varying by bit length.
        - name: bounded-word-extgcd
          description: Batched Nat, Int/GMP, and UInt64 extended-GCD calls on deterministic nonnegative bounded-word sample pairs.
  HexPoly:
    deps: []
    mathlib: false
    done_through: 7
    status: active
    phase4:
      comparators:
        - tool: "FLINT fmpz_poly via python-flint"
          class: informational
          rationale: "FLINT tunes Karatsuba/Toom-Cook/FFT crossovers in fmpz_poly_mul and uses non-recursive Newton-style algorithms for division and GCD; Hex's implementation is schoolbook with the Karatsuba crossover named in the algorithm table. The constant-factor gap is structural, not algorithmic — the ratio is recorded for orientation but is not a Phase-4 gate. Wired via a persistent-subprocess Python driver per SPEC/benchmarking.md §External comparators §Process call."
      input_families:
        - name: dense-int-arithmetic
          description: Deterministic dense integer polynomials for coefficientwise arithmetic, multiplication, derivative, and composition.
        - name: field-euclidean
          description: Fixed-size F7 dense polynomials for division, monic remainder, gcd, and extended gcd.
        - name: integer-content
          description: Dense integer polynomials with nontrivial coefficient content for content and primitive-part operations.
        - name: polynomial-crt
          description: Coprime monic rational-polynomial moduli and residues for CRT witness construction.
  HexMatrix:
    deps: [HexBasic]
    mathlib: false
    done_through: 7
    status: active
    phase4:
      input_families:
        - name: dense-square-multiplication
          description: Deterministic dense square integer matrices for textbook cubic matrix multiplication.
        - name: strassen-crossover-scaling
          description: Deterministic dense square integer matrices swept over dimension n and Strassen cutoff tau, for the naive-vs-mulStrassen log-log scaling figure and the measured crossover cutoff shipped as strassenDefault.cutoff.
  HexRowReduce:
    deps: [HexMatrix]
    mathlib: false
    done_through: 7
    status: active
  HexDeterminant:
    deps: [HexMatrix]
    mathlib: false
    done_through: 7
    status: active
    phase4:
      input_families:
        - name: leibniz-small-determinant
          description: Small structured integer matrices where the generic Leibniz determinant remains practical, cross-checked against the row-pivoted Bareiss determinant.
  HexBareiss:
    deps: [HexDeterminant, HexMatrix]
    mathlib: false
    done_through: 7
    status: active
    phase4:
      comparators:
        - tool: "FLINT fmpz_mat_det via python-flint"
          class: informational
          rationale: "FLINT's fmpz_mat_det uses multimodular reduction (determinant modulo many small primes, then CRT), which has a different asymptotic and constant-factor profile from the Hex row-pivoted Bareiss fraction-free elimination over Int. The ratio is recorded for orientation but is not a Phase-4 gate. Wired via a persistent-subprocess Python driver per SPEC/benchmarking.md §External comparators §Process call."
      input_families:
        - name: structured-bareiss-determinant
          description: Deterministic tridiagonal integer matrices for row-pivoted Bareiss determinant scaling without arbitrary coefficient blow-up.

  # ---------- Depth 1 ----------
  HexModArith:
    deps: [HexArith]
    mathlib: false
    done_through: 7
    status: active
    phase4:
      input_families:
        - name: word-residue-core
          description: Fixed-word prime-modulus residues for construction, casts, add/sub, extern multiplication, exponentiation, and inverse.
        - name: barrett-hot-loop
          description: Barrett-context multiplication chains over the UInt64 residue wrapper on the shared small odd prime modulus.
        - name: montgomery-hot-loop
          description: Montgomery conversion, Montgomery-form multiplication chains, and conversion back on the shared small odd prime modulus.
  HexGramSchmidt:
    deps: [HexRowReduce, HexDeterminant, HexBareiss]
    mathlib: false
    done_through: 7
    status: active
    phase4:
      input_families:
        - name: integer-gram-surface
          description: Deterministic n x (2n + 1) integer bases for Gram determinant vectors and scaled-coefficient surfaces.
        - name: row-update-helpers
          description: Deterministic small-entry update fixtures for size reduction and adjacent row swaps.
        - name: adjacent-swap-scalars
          description: Adjacent-swap denominator, pivot coefficient, Gram-determinant quotient, and scaled-coefficient numerator helper formulas.
  HexGF2:
    deps: [HexPoly, HexBasic]
    mathlib: false
    done_through: 7
    status: active
    phase4:
      comparators:
        - tool: "NTL GF2X via persistent C++ subprocess driver"
          class: informational
          rationale: "NTL ships hand-tuned word-level inner loops for GF(2)[x] (Karatsuba/FFT crossovers in mul, XOR-folding division, fast GCD); Hex's `GF2Poly` is the verified packed-word algorithmic surface. The constant-factor gap is structural rather than algorithmic — the ratios are recorded for orientation but are not a Phase-4 gate. Wired via a persistent-subprocess C++ driver (`scripts/oracle/gf2_ntl_bench_driver.cc`, built on-demand by `scripts/oracle/setup_gf2_ntl_driver.sh`) per SPEC/benchmarking.md §External comparators §Process call."
      input_families:
        - name: packed-word-clmul
          description: Deterministic UInt64 sample pairs for pure-Lean and extern carry-less word multiplication chains.
        - name: packed-bitwise-core
          description: Deterministic same-size packed GF2 polynomials for XOR addition and size-proportional left/right shifts.
        - name: packed-euclidean
          description: Deterministic same-size and division-shape packed GF2 polynomials for schoolbook multiplication, long division, remainder, gcd, and extended gcd.
        - name: gf2n-aes-field
          description: Deterministic AES-modulus single-word extension-field samples for addition, multiplication, inversion, division, and square-and-multiply powering.
        - name: gf2n-poly-quotient
          description: Deterministic degree-128 packed quotient-field samples for multiplication, inversion, division, and square-and-multiply powering.
        - name: packed-vs-generic-comparison
          description: Shared deterministic GF(2) coefficient fixtures for cross-library comparisons of packed `GF2Poly` versus generic `FpPoly 2` polynomial gcd and Berlekamp-style Frobenius-column construction.
  HexPolyZ:
    deps: [HexPoly, HexArith, HexBasic]
    mathlib: false
    done_through: 7
    status: active
    phase4:
      input_families:
        - name: congruence-witnesses
          description: Dense integer-polynomial finite-prefix congruence and constructed Bezout witness checks modulo a small prime.
        - name: content-normalization
          description: Dense integer polynomials with nontrivial coefficient content for content and primitive-part normalization.
        - name: mignotte-helpers
          description: Central binomial, square-root, coefficient-norm, and Mignotte coefficient-bound helper computations over deterministic integer-polynomial fixtures.

  # ---------- Depth 2 ----------
  HexLLL:
    deps: [HexGramSchmidt, HexMatrix, HexBasic]
    mathlib: false
    done_through: 7
    status: active
    phase4:
      comparators:
        - tool: "fpLLL via fplll-ffi"
          class: informational
          rationale: "fpLLL uses floating-point Gram-Schmidt (Nguyen-Stehle); this bypasses the integer-arithmetic operand-size drift the verified implementation pays, so the constant-factor gap is structural rather than algorithmic. The ratio is recorded for orientation but does not gate Phase 4. Measured through the fplll-ffi FFI shim (in-process C++ libfplll), the preferred comparator pattern and the same reducer the certified dispatch resolves at runtime, not a Python fpylll subprocess."
        - tool: "verified Isabelle LLL (AFP LLL_Basis_Reduction; Haskell extraction from Zenodo 2636367)"
          class: gating
          goal: "Lean LLL is at least as fast as the verified Isabelle LLL on shared canonical inputs at the bottom of each phase4.input_families parameter ladder."
        - tool: "verified Isabelle certified-LLL (JAR 2020 §7; svp_certified from the Zenodo 2636367 LLL_Basis_Reduction extraction, same archive as the native comparator)"
          class: gating
          goal: "The hex certified path (fpLLL + verified checker) is at least as fast as the Isabelle certified-LLL on shared canonical inputs at the largest eligible rung of each phase4.input_families ladder; the headline report records the ratio, the checker's cost share, and the candidate rejection rate."
      input_families:
        - name: bz-recombination
          description: "Berlekamp-Zassenhaus recombination basis at the documented (p, k, factors) configurations; the downstream hot path."
        - name: random-bounded
          description: "LCG-generated random integer bases, |entry| <= 30, n in {30, 60, 120, 240}; must include a committed seed where >= 1 Lovasz swap fires."
        - name: harsh-cubic
          description: "Entry bit-length ~ 3.3 * n at n in {15, 30, 45} (verified-Isabelle paper regime); exercises bigint operand-size drift."
        - name: ajtai
          description: "Ajtai-style worst-case lower-triangular bases (faithful port of fplll gen_trg / latticegen t, alpha 1.2); diagonal D_i in [2, 2^floor((2d-i)^1.2)], off-diagonals |.| < D_i/2. Drives the Theta(d^2 log B) swap count - the iteration-count scaling axis the near-orthogonal families leave unmeasured."
        - name: q-ary
          description: "q-ary LWE/SIS bases [[I,H],[0,qI]] (fplll gen_qary / latticegen q), H uniform mod q=2^(b-1)+rand; the step profile LLL smooths into the characteristic Z-shape."
        - name: ntru
          description: "NTRU-like bases [[I,Rot(h)],[0,qI]] on 2d x 2d (fplll gen_ntrulike / latticegen n), circulant h with h(1)=0 mod q; planted dense structure plus q-block."
        - name: knapsack
          description: "Rectangular d x (d+1) integer-relation bases (fplll gen_intrel / latticegen r), row i = [rand_b, e_{i+1}]; the only family with cols != rows, exercising the m>n ofBasis path. Also drives the success-vs-density recovery chart."
  HexPolyFp:
    deps: [HexPoly, HexModArith]
    mathlib: false
    done_through: 7
    status: active
    phase4:
      input_families:
        - name: quotient-powers
          description: Dense `F_65537` quotient-ring exponentiation and Frobenius power fixtures with modulus degree and exponent height scaled together.
        - name: modular-composition
          description: Same-size dense `F_65537` Horner modular composition modulo deterministic monic moduli.
        - name: product-squarefree
          description: Deterministic `F_5` products of linear factors covering weighted product reconstruction and Yun square-free decomposition summaries.

  # ---------- Finite-field quotient pipeline ----------
  HexGFqRing:
    deps: [HexPolyFp]
    mathlib: false
    done_through: 7
    status: active
    phase4:
      input_families:
        - name: dense-reduction
          description: Dense polynomial reduction and quotient construction modulo deterministic nonconstant dense moduli over F65537.
        - name: quotient-arithmetic
          description: Canonical quotient representatives for addition, multiplication, negation, subtraction, exponentiation, scalar multiplication, and natural casts.
  HexGFqField:
    deps: [HexGFqRing, HexBerlekamp]
    mathlib: false
    done_through: 7
    status: active
    phase4:
      comparators:
        - tool: FLINT fq_default via python-flint
          class: informational
          rationale: "FLINT's fq_default finite-field arithmetic is a tuned C implementation over irreducible polynomial quotient fields; HexGFqField is the verified field wrapper over HexGFqRing with certificate-checked irreducible moduli. The ratio is recorded for orientation but is not a Phase-4 gate. Wired via the shared persistent-subprocess python-flint driver (`scripts/oracle/flint_bench_driver.py`) per SPEC/benchmarking.md §External comparators §Process call."
      input_families:
        - name: dense-canonical-reduction
          description: Field construction from a dense polynomial through quotient-ring reduction modulo certificate-checked irreducible moduli over F7.
        - name: field-arithmetic
          description: Canonical field representatives over F7 quotients for addition, multiplication, negation, and subtraction.
        - name: field-exponentiation
          description: Square-and-multiply natural, signed, and Frobenius p-th powers on canonical field representatives over F7 quotients.
        - name: field-inversion-division
          description: Extended-gcd inversion and division on canonical field representatives over F7 quotients.

  # ---------- Factoring pipeline ----------
  HexBerlekamp:
    deps: [HexPolyFp, HexMatrix, HexRowReduce, HexGFqRing, HexBasic]
    mathlib: false
    done_through: 3
    status: active
    phase4:
      comparators:
        - tool: "FLINT nmod_poly.is_irreducible via python-flint"
          class: gating
          goal: "Lean runRabinTestChecksum is at least as fast as FLINT nmod_poly.is_irreducible on shared canonical inputs at the largest eligible rung."
        - tool: "FLINT nmod_poly.factor_distinct_deg via python-flint"
          class: gating
          goal: "Lean runDistinctDegreeChecksum is at least as fast as FLINT nmod_poly.factor_distinct_deg on shared canonical inputs at the largest eligible rung."
      input_families:
        - name: berlekamp-matrix
          description: Deterministic dense monic F_5 polynomials for Berlekamp Frobenius-matrix construction.
        - name: rabin-irreducibility
          description: Deterministic dense monic F_5 polynomials for Rabin irreducibility testing.
        - name: split-step-factorization
          description: Fibonacci-style F_5 polynomial pairs exercising quadratic Euclidean gcd work in Berlekamp split candidates.
        - name: distinct-degree-factorization
          description: Deterministic dense monic F_5 polynomials with mixed low-degree factor structure for distinct-degree factorization.
  HexHensel:
    deps: [HexPolyFp, HexPolyZ, HexBasic]
    mathlib: false
    done_through: 7
    status: active
    phase4:
      comparators:
        - tool: "FLINT nmod_poly_hensel_lift_* via python-flint"
          class: informational
          rationale: "FLINT exposes a family of tuned C Hensel-lift entry points (`nmod_poly_hensel_lift_once_preinv`, `nmod_poly_hensel_lift`, `nmod_poly_hensel_continue_lift`) that perform the same Newton-style quadratic lift Hex implements through its linear / quadratic / multifactor surfaces. The constant-factor gap reflects FLINT's word-level operand tuning and its `preinv` precomputation that Hex doesn't currently exploit. The comparator is wired as a persistent-subprocess call via the shared python-flint driver from HO-20 (`scripts/oracle/flint_bench_driver.py`); python-flint does not bind the `nmod_poly_hensel_lift_*` C entry points directly, so the driver emulates the Newton-style schema via `fmpz_poly` arithmetic, which is what the recorded informational ratios measure. A future gating upgrade requires a separate SPEC PR identifying a narrower comparable kernel (e.g. single-step lift with preinv on canonical inputs) per SPEC/Libraries/hex-hensel.md §External comparators."
      input_families:
        - name: bridge-operations
          description: Coefficient reduction from Z[x] to F_5[x], canonical lifting from F_5[x] to Z[x], and reduction modulo a fixed power of 5 over deterministic dense integer and F_5 polynomial fixtures.
        - name: linear-hensel
          description: Linear Hensel lifting on deterministic dense integer-polynomial fixtures, covering both a single correction step at fixed precision and the iterative wrapper over encoded (n, k) parameters including Mignotte-sized k.
        - name: quadratic-hensel
          description: Single quadratic Hensel correction step on deterministic dense integer-polynomial fixtures with full lifted Bezout updates.
        - name: multifactor-lifting
          description: Ordered multifactor product, linear ordered multifactor lifting, and the production quadratic ordered multifactor lifter on deterministic two-factor dense integer-polynomial fixtures over encoded (n, k) parameters.
  HexConway:
    deps: [HexBerlekamp]
    mathlib: false
    done_through: 7
    status: active
    phase4:
      input_families:
        - name: tier1-committed-table
          description: Imported Luebeck Conway-table entries for supported `(p, n)` pairs, covering finite table lookup, supported-entry recovery, and Tier-1 irreducibility verification.
  HexGFq:
    deps: [HexGFqField, HexConway, HexGF2]
    mathlib: false
    done_through: 7
    status: active
    phase4:
      input_families:
        - name: generic-constructor-projection
          description: Generic GFq constructor and representative projection on deterministic binary polynomial representatives over the committed Conway entry GFq 2 1.
        - name: packed-constructor-projection
          description: Packed GF2q constructor and representative projection on the committed single-word Conway entry GF2q 1.
        - name: packed-generic-shared-bridge
          description: Shared binary representative family exercising both packed GF2q and generic GFq constructor/projection paths on the common p = 2 API surface.
  HexBerlekampZassenhaus:
    deps: [HexBerlekamp, HexHensel, HexLLL]
    mathlib: false
    done_through: 0
    status: active
    phase4:
      comparators:
        - tool: "verified Isabelle BZ (AFP Berlekamp_Zassenhaus; Haskell extraction of factor_int_poly via Factorization_External_Interface)"
          class: gating
          goal: "Lean BZ is at least as fast as the verified Isabelle BZ on shared canonical inputs at the largest eligible scaling rung of every registered scientific bench target. Algorithm-class caveat per SPEC/Libraries/hex-berlekamp-zassenhaus.md §External comparators: the 1× gate presumes the comparator implements an algorithm of the same class or weaker than hex's; Isabelle's classical exhaustive recombination is weaker than hex's BHKS van Hoeij CLD."
      input_families:
        - name: public-factor-combinator
          description: Public `factor` combinator on deterministic split integer-polynomial smoke inputs, covering the fast-with-slow-fallback API surface.
        - name: cld-fast-path
          description: Proof-facing CLD `factorFast` path on deterministic split inputs, preserving `none` outcomes and the fast-path setup surfaces for smoke-intractable adversarial cases.
        - name: exhaustive-slow-backstop
          description: Unconditional `factorSlow` exhaustive recombination backstop on deterministic split inputs, including the bounded degree/height diagnostic subset.
        - name: degree-height-matrix
          description: Encoded degree/root-height split integer-polynomial matrix for public, fast-path, and slow-path BZ factorization registrations.
        - name: fallback-probe
          description: Explicit split-degree cascade-trigger inputs `(X-1)...(X-n)` for public BZ factorization, covering the prime-search fallback and BHKS recombination shape together.
        - name: ho2-adversarial-recombination
          description: HO-2 adversarial recombination shapes `X^4 + 1`, `(X^2 - 2)(X^2 - 3)`, Swinnerton-Dyer SD3, and `Phi_15`, including pinned modular split profiles.

  # ---------- Mathlib bridges ----------
  HexPolyMathlib:
    deps: [HexPoly]
    mathlib: true
    done_through: 7
    status: active
    phase4:
      input_families:
        - name: dense-mathlib-conversion
          description: Deterministic dense integer polynomials transported through `toPolynomial` and `ofPolynomial`, including the paired round-trip checksum.
        - name: euclidean-bridge-transport
          description: Polynomial Fibonacci quotient-chain fixtures over `Rat` carried through the executable `DensePoly.gcd`/`DensePoly.xgcd` plus the dense-to-Mathlib bridge.
  HexMatrixMathlib:
    deps: [HexMatrix]
    mathlib: true
    done_through: 6
    status: active
    phase4:
      input_families:
        - name: matrix-representation-conversion
          description: Deterministic dense integer matrices transported through `matrixEquiv`, `matrixEquiv.symm`, and paired round-trip checksums.
        - name: row-operation-bridge-checks
          description: Deterministic square integer matrices exercising executable row swap, scale, and add operations against the corresponding Mathlib-side row-operation constructions.
        - name: determinant-bridge-checks
          description: Small deterministic integer matrices exercising the Hex and Mathlib Leibniz determinant bridge paths on the shared fixture schedule.
  HexRowReduceMathlib:
    deps: [HexMatrixMathlib, HexRowReduce]
    mathlib: true
    done_through: 5
    status: active
  HexDeterminantMathlib:
    deps: [HexBareiss, HexDeterminant, HexMatrixMathlib]
    mathlib: true
    done_through: 5
    status: active
  HexBareissMathlib:
    deps: [HexDeterminantMathlib]
    mathlib: true
    done_through: 5
    status: active
  HexModArithMathlib:
    deps: [HexModArith]
    mathlib: true
    done_through: 7
    status: active
  HexGramSchmidtMathlib:
    deps: [HexGramSchmidt, HexBareissMathlib]
    mathlib: true
    done_through: 6
    status: active
  HexPolyZMathlib:
    deps: [HexPolyZ, HexHensel, HexPolyMathlib, HexModArithMathlib]
    mathlib: true
    done_through: 6
    status: active
  HexLLLMathlib:
    deps: [HexLLL, HexGramSchmidtMathlib, HexRowReduceMathlib]
    mathlib: true
    done_through: 4
    status: active
  HexBerlekampMathlib:
    deps: [HexBerlekamp, HexPolyMathlib, HexModArithMathlib]
    mathlib: true
    done_through: 3
    status: active
  HexHenselMathlib:
    deps: [HexHensel, HexPolyMathlib]
    mathlib: true
    done_through: 7
    status: active
  HexGF2Mathlib:
    deps: [HexGF2, HexPolyFp, HexGFqField]
    mathlib: true
    done_through: 4
    status: active
  HexGFqMathlib:
    deps: [HexGFq, HexGF2Mathlib]
    mathlib: true
    done_through: 7
    status: active
  HexBerlekampZassenhausMathlib:
    deps: [HexBerlekampZassenhaus, HexBerlekampMathlib, HexHenselMathlib, HexPolyZMathlib, HexMatrixMathlib, HexLLLMathlib]
    mathlib: true
    done_through: 2
    status: active

  # ---------- Planned (status: planned; SPEC ready, implementation deferred) ----------
  HexRoots:
    deps: [HexPolyZ]
    mathlib: false
    # done_through stays 3: the Phase-4 scientific run (commit b08a66cce522,
    # chungus2) returned inconclusive verdicts for 9 of 13 parametric
    # registrations and two SPEC time budgets fail, so Phase 4 is NOT claimed.
    # See reports/hexroots-performance.md §Concerns. The phase4 block below
    # records the comparators and input families the run used; it does not
    # assert completion.
    done_through: 3
    status: active
    phase4:
      comparators:
        - tool: "python-flint fmpz_poly.complex_roots"
          class: informational
          rationale: "The SPEC's ci-tier oracle (python-flint fmpz_poly.complex_roots, returning certified Arb balls with multiplicities) is a multiprecision ball-arithmetic engine, structurally different from this library's decidable exact-integer Pellet / Newton-Kantorovich certificates. Timed on the same seed-0xC0FFEE dense integer ladder the whole-polynomial drivers use (scripts/bench/hexroots_flint_compare.py); the ratio hex isolateAll?@32 / flint per degree is recorded in reports/hexroots-performance.md. Informational, not gating: the SPEC's time budgets — not a constant-factor 1x goal — are the yardstick for an integer-certified isolator against a float engine."
        - tool: "MPSolve"
          class: informational
          rationale: "MPSolve (Bini-Fiorentino, the SPEC's local-tier and Phase-4 external performance comparator) is a multiprecision-float C library computing approximate root inclusions, structurally different from this library's integer-certified Lean witnesses, so its ratio orients but does not gate. Scheduled-only: not wired in this PR. Required environment stated in bench/HexRoots/Bench.lean's module docstring (the mpsolve CLI built with GMP, driven on the seeded ladder via -au -Gi isolate mode)."
      input_families:
        - name: seeded-dense
          description: Seed-0xC0FFEE dense integer polynomials with coefficients in [-10, 10] (constant term first, leading forced nonzero), generically distinct irrational roots; drives taylor, mahlerPrec, refine1, certify, and the whole-polynomial isolateAll?/isolate drivers.
        - name: wilkinson-linprod
          description: Wilkinson-shaped products ∏(X−j), j=1..n, with distinct integer roots 1..n; Newton recentres exactly onto integer roots, exercised by the witness-check, Newton-step, and dual-route compare-group registrations.
        - name: refine-fixed
          description: The fixed degree-3 polynomial (x−1)(x−2)(x+3) whose isolated atom the refineTo? and sameRoot registrations sharpen to a parametric target precision.
  HexRootsMathlib:
    deps: [HexRoots, HexPolyZMathlib]
    mathlib: true
    done_through: 0
    status: planned
  HexResultant:
    deps: [HexPoly]
    mathlib: false
    done_through: 0
    status: planned
  HexResultantMathlib:
    deps: [HexResultant, HexPolyMathlib]
    mathlib: true
    done_through: 0
    status: planned
  HexNumberField:
    deps: [HexPolyZ, HexRoots, HexResultant, HexBerlekampZassenhaus, HexMatrix, HexRowReduce]
    mathlib: false
    done_through: 0
    status: planned
  HexNumberFieldMathlib:
    deps: [HexNumberField, HexResultantMathlib, HexBerlekampZassenhausMathlib, HexRootsMathlib, HexPolyZMathlib]
    mathlib: true
    done_through: 0
    status: planned
  HexRealRoots:
    deps: [HexPolyZ]
    mathlib: false
    done_through: 4
    status: active
    phase4:
      comparators:
        - tool: "SageMath real_roots / python-flint fmpz_poly real-root API"
          class: informational
          rationale: "The SPEC's oracle role list (SageMath real_roots, python-flint fmpz_poly, FLINT/Arb) targets floating-point / ball-arithmetic real-root isolation, structurally different from the certified exact-integer Sturm/Descartes engines this library implements: the comparator answers with approximate intervals refined to a requested precision, while Hex answers with a decidable Sturm-count certificate. The ratio is recorded for orientation but is not a Phase-4 gate, and is scheduled-only — the persistent-subprocess Python driver is not wired in this PR. The gating cross-implementation check is the internal Descartes-first vs certified-Sturm compare group (compare runIsolateDescartesFirst runIsolateSturm), which joins on isolation-endpoint hashes."
      input_families:
        - name: well-separated-products
          description: Products of unit-separated linear factors ∏(x−k), k=1..n, the Descartes engine's easy regime; resolves in O(n + log(bound/gap)) bisection levels.
        - name: chebyshev-clustered
          description: Integer Chebyshev polynomials T_n from the recurrence T_{k+1}=2x·T_k−T_{k-1}, with n real roots clustering near ±1 at gaps ~1/n².
        - name: mignotte-worst-case
          description: Mignotte polynomials xⁿ−(a·x−1)² at a=1000, the textbook Descartes worst case exercising the close real root pair.
        - name: dense-primitive
          description: Deterministic reliably-squarefree bounded-coefficient dense integer polynomials for the Sturm-chain, sign-variation, Möbius-transform, root-bound, separation-precision, and refinement primitives.
  HexRealRootsMathlib:
    deps: [HexRealRoots, HexPolyZMathlib]
    mathlib: true
    done_through: 3
    status: active
  HexRCF:
    deps: [HexRealRoots, HexRealRootsMathlib, HexPolyZ, HexPolyZMathlib]
    mathlib: true
    done_through: 0
    status: planned