# Roadmap

The prioritized work queue. When an item lands, delete it here; distilled
style rules go to `STYLE.md`, outward-facing summaries to `README.md`.
Problem selection follows Karp's 1972 paper and the Garey–Johnson appendix
(`materials/karp.txt`, `materials/garey-johnson.md`); bracketed codes below
are GJ appendix numbers. Last revised 2026-08-01.

Current state: thirty-eight problems and sixty reductions, every one
certified end to end. Every problem carries its representation pair
(one `Representation.lean` per domain, eight of them): each abstract problem provably
interreduces with its concrete encoding, so certified conclusions transfer to
the abstract problems by composition, across domains as well as within one.
The standing milestone is that the correctness catalog and the certified
catalog coincide; keep it. A new entry lands with its
certificate and its representation pair in the same batch — the pair is one
line per problem once the domain's encoding exists.

## How items are ordered

1. **Keep the certified subgraph equal to the whole graph.** The library's
   thesis is that certification is cheap enough to be universal; a growing
   gap between the correctness catalog and the certified catalog would
   refute it. New entries should land with their certificates, or acquire
   them before the next entry starts.
2. **Each new entry should stress something new** — a new instance shape, a
   new domain folder, a new combinator, a new proof pattern. A tenth
   graph-to-graph subset problem teaches nothing.
3. **Prefer unlockers.** Of Garey–Johnson's "six basic problems" (3SAT, 3DM,
   VERTEX COVER, PARTITION, HAMILTONIAN CIRCUIT, CLIQUE), all six are now
   present; HAMILTONIAN CIRCUIT, the last to land, unlocks an appendix
   section of descendants.
4. **Engine features on demand only.** A combinator or primitive lands with
   the first certificate that needs it, never speculatively — the same
   discipline that keeps the blanket theorem's induction tractable.

## P1 — the big constructions

1. **The packing–scheduling axis.** `Scheduling/` holds MULTIPROCESSOR
   SCHEDULING and SEQUENCING WITH RELEASE TIMES AND DEADLINES, the latter
   strongly hard from 3-PARTITION by composition — Garey–Johnson's [SS1]
   statement. One thing remains:
   - **Strong hardness for MULTIPROCESSOR SCHEDULING.** The 3-PARTITION → BIN
     PACKING certificate does not deliver it by composition: that certificate
     targets the *unary* bin-packing avatar, while BIN PACKING →
     MULTIPROCESSOR SCHEDULING is binary at both ends, so the composite proves
     ordinary hardness only. The gap is mechanical rather than mathematical — a
     `MultiprocessorUnaryTy` with its decoder and representation pair, and the
     same instance map at unary type, where the `bins = 0` branch test becomes
     `Code.isNil` on the bin numeral in place of `natEq … 0`.
2. **CUBIC restrictions** — VERTEX COVER (and INDEPENDENT SET) on *regular*
   degree-3 graphs, `= 3` rather than the `≤ 3` now in the catalog. A separate
   padding reduction with its own source: Garey–Johnson–Stockmeyer's Theorem
   2.6 delivers the bound, not the regularity (half its circuit vertices have
   degree two), while the book's GT1/GT20 comment asserts *cubic planar* from a
   citation cluster ([GJS 1976] + [GJ 1977a] + [Maier–Storer 1977]) that the
   primary construction does not support by itself. Land it when a descendant
   needs regularity, and settle the citation question then.
3. **0-1 INTEGER PROGRAMMING** [MP1] ← SAT (Karp's first reduction): forces
   the signed-number decision (a `Ty` extension vs. an inequality normal
   form avoiding negatives). Defer until a second client for signed weights
   appears.
4. **DIRECTED HAMILTONIAN CIRCUIT** [GT38] ← HAMILTONIAN CIRCUIT, by
   bidirection (`Digraph.ofSimpleGraph` again: directed Hamiltonian circuits
   of a bidirected graph are its undirected Hamiltonian cycles), which
   supersedes Karp's own VERTEX COVER → DIRECTED HC now that undirected HC is
   in the catalog. This is where the directed walk stack the feedback problems
   avoid becomes unavoidable: a Hamiltonicity predicate has to speak about
   walks, and mathlib's `Digraph/` has none. Scope that first — list-based
   closed walks, or an upstreamable `Digraph.Walk` — since the rest is small.
   DIRECTED HAMILTONIAN PATH then follows as HC → HP did.

## P2 — smaller entries

1. **EXACT COVER BY 3-SETS from MONOTONE ONE-IN-THREE 3SAT** — an all-positive
   exactly-one clause *is* a three-element set to be covered exactly once, so
   the reduction is a reading rather than a construction, and it gives X3C a
   second, literal-free route beside 3DM. Filed here when MONOTONE ONE-IN-THREE
   3SAT landed without it.
2. **SET SPLITTING restricted to 3-sets**, and BETWEENNESS re-sourced from it.
   Garey–Johnson derive [MS1] from [SP4], and the catalog cannot: Opatrný's
   clause gadget reads exactly three elements of a set, so it over-constrains a
   family of arbitrary-size sets, and BETWEENNESS reduces from NOT-ALL-EQUAL
   3SAT instead. The restriction would need its own hardness proof — the
   literal system of `SetSplitting/FromNae3Sat.lean` already produces 3-sets
   from a width-3 formula, so the entry is mostly a restatement — after which
   SET SPLITTING acquires the consumer it currently lacks.

## Engine and convenience features (each lands with its first client)

Gadget-style infrastructure, sequenced against the HC batch (last revised
2026-07-22, after the block-numbering layer landed in `Cert/Numbering.lean`
with all six annex numberings migrated onto it):

- **`idxOfBy` and `rangeOfLen`** — *exist; nothing to build*. The
  enum–filter–`listSum` idiom for "position of a label in a dedup'd list" is
  `slotOfCode` (`Logic/Sat/Encoding.lean`), and the enum-a-constructed-list
  idiom for index ranges is `Code.indices` (`Cert/Language.lean`); each
  carries its eval lemma, and the MAX 2SAT → SIMPLE MAX CUT annex used both
  unchanged. The standing rule they embody remains: deliberately **no**
  `range : nat → list nat` primitive, ever — a list of length `n` from a
  binary-encoded `n` is exponential in the bit-charged size model, and
  `Code.indices` off a list built to the right length is the honest
  workaround.
- **New aggregates**, per the standing admission rule (output size bounded
  by input bit content; own case of the blanket theorem). Known-eligible
  candidate: `listProd` (product's bit length ≤ total bit content), whose
  client would be SUBSET PRODUCT [SP14].
- **Macro frontend** (`for`/`when`/`emit` elaborating to point-free
  `Code`): the biggest ergonomics lever, deliberately deferred until the
  annex corpus is large enough to dictate the surface language. The
  MAX 2SAT → SIMPLE MAX CUT annex — the most demanding yet, with its
  environment-threaded clause pass and slot-table reads — is now the concrete
  reference for what that layer must express; revisit before the next large
  gadget certificate.

## Blocked / long-term

- **The machine-model bridge** — a single theorem by design, blocked on
  mathlib acquiring a formalization of polynomial-time computation.
- **Planar restrictions** (planar VC, planar 3-COLORABILITY) — blocked on
  planarity in mathlib; crossover gadgets are a major undertaking anyway.
- **FEEDBACK ARC SET on tournaments** — `Problem.restrict` with the tournament
  condition (exactly one arc per unordered pair, decidable, so weakening
  works). Hardness is not in Karp or Garey–Johnson: the literature route runs
  through Ailon–Charikar–Newman / Alon / Charbit–Thomassé–Yeo, whose
  constructions use randomization or blow-ups and need real scoping before
  formalization. The catalog-side anchor for weighted-tournament questions
  (Kemeny is weighted FAS on the majority tournament).
- **Prior-art mining** — the Isabelle poly-reductions repository has the
  largest comparable catalog; mine it for reduction inventory and for how
  they scale certification (pointers in the prototype notes).