# 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 ----------
  HexArith:
    deps: []
    mathlib: false
    done_through: 5
    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: 5
    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: []
    mathlib: false
    done_through: 5
    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. The other Phase-4 matrix surfaces (multiplication, row operations) declare absence with the structural-layer reason per SPEC/benchmarking.md §Comparator naming. Wired via a persistent-subprocess Python driver per SPEC/benchmarking.md §External comparators §Process call."
      input_families:
        - name: dense-square-multiplication
          description: Deterministic dense square integer matrices for textbook cubic matrix multiplication.
        - name: structured-bareiss-determinant
          description: Deterministic tridiagonal integer matrices for row-pivoted Bareiss determinant scaling without arbitrary coefficient blow-up.
        - name: leibniz-small-determinant
          description: Small structured integer matrices where the generic Leibniz determinant remains practical for Bareiss cross-checking.

  # ---------- Depth 1 ----------
  HexModArith:
    deps: [HexArith]
    mathlib: false
    done_through: 5
    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: [HexMatrix]
    mathlib: false
    done_through: 4
    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]
    mathlib: false
    done_through: 5
    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]
    mathlib: false
    done_through: 4
    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]
    mathlib: false
    done_through: 4
    status: active
    phase4:
      comparators:
        - tool: "fpLLL via fpylll"
          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."
        - 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."
      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."
  HexPolyFp:
    deps: [HexPoly, HexModArith]
    mathlib: false
    done_through: 5
    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: 5
    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, HexGFqRing]
    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]
    mathlib: false
    done_through: 5
    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: 5
    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: 5
    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: 5
    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: 4
    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.
  HexModArithMathlib:
    deps: [HexModArith]
    mathlib: true
    done_through: 4
    status: active
  HexGramSchmidtMathlib:
    deps: [HexGramSchmidt, HexMatrixMathlib]
    mathlib: true
    done_through: 3
    status: active
  HexPolyZMathlib:
    deps: [HexPolyZ, HexHensel, HexPolyMathlib, HexModArithMathlib]
    mathlib: true
    done_through: 3
    status: active
  HexLLLMathlib:
    deps: [HexLLL, HexMatrixMathlib, HexGramSchmidtMathlib]
    mathlib: true
    done_through: 3
    status: active
  HexBerlekampMathlib:
    deps: [HexBerlekamp, HexPolyMathlib, HexModArithMathlib]
    mathlib: true
    done_through: 3
    status: active
  HexHenselMathlib:
    deps: [HexHensel, HexPolyMathlib]
    mathlib: true
    done_through: 3
    status: active
  HexGF2Mathlib:
    deps: [HexGF2, HexPolyFp, HexGFqField]
    mathlib: true
    done_through: 3
    status: active
  HexGFqMathlib:
    deps: [HexGFq, HexGF2Mathlib]
    mathlib: true
    done_through: 3
    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: 0
    status: planned
  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]
    mathlib: false
    done_through: 0
    status: planned
  HexNumberFieldMathlib:
    deps: [HexNumberField, HexResultantMathlib, HexBerlekampZassenhausMathlib, HexRootsMathlib, HexPolyZMathlib]
    mathlib: true
    done_through: 0
    status: planned