# HardnessReductionsLean

A prototype Lean 4 / mathlib library of NP-hardness (Karp) reductions that
deliberately avoids Turing machines and any formalization of P/NP.

## Companion documents

- **`STYLE.md` — the style and proof-engineering guide.** Read the relevant
  section *before* writing: catalog entries and reduction statements, gadget
  construction, certificate annexes, the recurring tactic failure modes and
  their fixes, and the rules for admitting a `Code` primitive. It opens with a
  table saying which section applies to which job. Much of it is hard-won and
  non-obvious — the tactic section in particular will save hours.
- **`ROADMAP.md`** — the prioritized work queue.
- **`materials/`** (git-ignored) — design discussions, source material
  (Garey–Johnson, Karp), and research notes.

## Build

- `lake build` (lake is at `~/.elan/bin/lake`). Mathlib is required via
  `lakefile.toml` and its olean cache is already downloaded; a clean build of
  just this library takes a few minutes, incremental builds seconds.
- Lean toolchain: see `lean-toolchain`. Mathlib uses the new module system
  (`module` / `public import`); this library uses plain imports, which is fine.

## Architecture

Two layers, kept deliberately independent, plus a bridge:

1. **Mathematical layer**: `Problem α := α → Prop`, `Reduction P Q` = instance
   map + correctness iff (`P ⟶ᵣ Q` notation), both in `Core.lean`. No resource
   bounds anywhere. Instances are bundled structures with a `V : Type` field
   plus `Fintype`/`DecidableEq`/decidable relation instance fields (registered
   via `attribute [instance]`), so correctness proofs can use mathlib's
   `SimpleGraph` API directly.
2. **Certificate layer** (`Cert/` — generic engine only): a deep-embedded,
   point-free combinator language `Code σ τ` over a closed universe `Ty` of
   first-order types, with evaluator, bit-charged cost model, and a
   once-and-for-all theorem that all programs have polynomially bounded cost
   and output size (`Code.cost_size_le_polyBound`). The bridge from `Code` to
   any future machine-model formalization of FP is a single theorem, to be
   proven when mathlib gets one.
3. **Bridge** (`Cert/Bridge.lean`): `CertifiedReduction` = `Code` program +
   correctness on *concrete* instances; abstract problems pull back along total
   decode functions (`Problem.comap`). Decode totality convention for graphs:
   vertices are the *positions* of the explicit vertex list, edges are index
   pairs, junk ignored — so no well-formedness predicates are needed anywhere.

The standing milestone is that the correctness catalog and the *certified*
catalog coincide: every reduction should land with its certificate, or acquire
one before the next entry starts. The two are tracked as distinct objects in
`README.md`, and a gap between them is a bug in the queue, not a detail.

## File layout (Garey–Johnson-style catalog)

Files are organized as a catalog of hard problems, in domain folders mirroring
GJ's appendix sections (`Logic/`, `Graph/`, `Sets/`, `Numbers/`,
`Networks/`). The rule:
**a reduction is filed under its *target* problem** — it is a proof that the
target is hard.

- `<Domain>/<Problem>.lean` — the catalog entry: the problem definition, with a
  docstring pointing at its hardness proofs.
- `<Domain>/<Problem>/From<Source>.lean` — the reduction Source → Problem
  (correctness). One-line derived compositions get the same treatment (e.g.
  `Graph/VertexCover/FromSat.lean`).
- Certification artifacts are an annex of the reduction:
  `From<Source>/Code.lean` (the `Code` program) and `From<Source>/Adequacy.lean`
  (the `CertifiedReduction`), or a single `From<Source>/Certified.lean` when
  small.
- Shared per-domain material sits at domain level: instance types in
  `<Domain>/Defs.lean`, concrete `Ty` encodings + decoders + `Concrete.*`
  problems in `<Domain>/Encoding.lean` (or `<Domain>/<Problem>/Encoding.lean`
  where the instance type belongs to a single problem family, e.g.
  `Logic/Sat/Encoding.lean`). When several catalog entries ask *different
  questions of the same Garey–Johnson instance*, they share one instance type
  and one encoding, and each entry file holds only its question (precedent:
  `SetSystemInstance` — SET COVER, HITTING SET, SET PACKING).
- A gadget that two reductions read in different ways is not annex material: it
  gets a domain-level pair `<Domain>/<Gadget>.lean` (mathematical layer) and
  `<Domain>/<Gadget>/Code.lean` (program + decoding lemmas), and the annexes
  shrink to their correctness proofs (precedent: `Sets/StarSystem`, serving
  VERTEX COVER → SET COVER and INDEPENDENT SET → SET PACKING).
- Restrictions ("hard even if …", via `Problem.restrict`) nest under their
  problem: `<Domain>/<Problem>/<Restriction>.lean` + hardness in
  `<Problem>/<Restriction>/From<Source>.lean`. Famous restrictions with their
  own literature identity (3SAT, 3-COLORABILITY) are promoted to top-level
  entries (`Logic/Sat3.lean`, `Graph/Colorability3/`).
- Namespaces do NOT mirror paths: everything stays in `Hardness` /
  `Hardness.Cert` regardless of file location.

## Conventions

- Namespace everything under `Hardness`.
- Problems are SCREAMING_SNAKE (`CLIQUE`, `INDEPENDENT_SET`, `VERTEX_COVER`,
  `SAT`) — complexity-theory convention, a deliberate deviation from mathlib
  style.
- State the mathematical content of each reduction as a standalone lemma over
  unbundled data, then define the `Reduction` with a trivial glue proof. (Why,
  and what each target shape obliges you to prove: `STYLE.md`.)
- **Size-model discipline**, critical for the eventual honesty of the
  certificates: explicit vertex/element lists (isolated vertices are
  represented), numbers charged by bit length (`Nat.size`), no combinator may
  iterate a binary-encoded number of times.
- **Fresh names in gadget constructions are *tagged tuples of input objects***,
  realized as dependent pairs / sum types (e.g. `CNF.Occ φ` = clause index ×
  position), never generated counters.
- Reduction arrows are `→` in docstrings and README prose; ASCII `->` only in
  commit messages.
- When work lands: delete the item from `ROADMAP.md`, update `README.md`'s
  catalog and counts, and distill any new style lesson into `STYLE.md` — all in
  the same change. README entries and docstrings must be *timeless and evenly
  weighted* — no "the catalog's first X", no essay for the entry you just
  landed; see STYLE.md § Prose.
- Commit discipline for multi-front batches: engine extensions first, then one
  commit per certificate, then wiring (root imports + README + docs). A
  promotion into a shared file must move the definition and all its use-sites
  in the same commit, so every commit builds.

## Known deviations / lint

- `weak.linter.style.header = false` in `lakefile.toml`: no mathlib copyright
  headers here.
- Use `change` not `show` when the goal changes up to defeq (mathlib lint).