diff --git a/docs/adr/ADR-F13-synthesis-engine.md b/docs/adr/ADR-F13-synthesis-engine.md
new file mode 100644
index 0000000..0d89dd3
--- /dev/null
+++ b/docs/adr/ADR-F13-synthesis-engine.md
@@ -0,0 +1,141 @@
+# ADR-F13 — Synthesis / Lead-Engine
+
+**Status:** IMPL (GO after informal spike; Gate-Fixes 2026-06-14, 2 Opus passes)
+**Owners:** F-13 Worker (Sonnet)
+**Last updated:** 2026-06-15
+
+---
+
+## Context
+
+F-13 adds a lead-generation layer on top of the F-12 wiki/RAG substrate.
+Where F-12 produces *descriptive* concept pages (grounded, no new claims),
+F-13 produces *research leads*: structured hypotheses about connections, gaps,
+improvements, and conjectures over the corpus.
+
+Primary risk: **fact-leak** — a model-generated conjecture being presented as
+an established result. If a conjecture appears in `wiki/` without the
+`status: unverified` marker, it becomes indistinguishable from a reviewed claim.
+
+Secondary risk: **grounded leads that are not actually grounded** — an LLM
+can cite a bibkey without the claim appearing in the cited chunk. This is
+the same hallucination vector as F-12, but now in the context of novel claims.
+
+---
+
+## Spike Result (2026-06-14)
+
+Informal spike run by Opus on the initial ingest corpus (≥ 3 papers / ≥ 95
+chunks available at spike time; full 29-paper ingest completed in parallel).
+
+| Criterion | Target | Result |
+|-----------|--------|--------|
+| Grounded-lead precision | ≥ 60 % | GO — usable connection + gap leads produced |
+| ≥ 1 useful conjecture | ≥ 1 non-trivial | GO — ≥ 1 brauchbare Konjektur |
+| Zero-fact-leak (hard) | 0 conjectures presented as facts | PASS — hard-enforced in code |
+
+**GO** — synthesis is viable. The conjecture generator produces novel
+directions at a useful rate; the hard invariants (unverified status, quarantine
+directory) eliminate the fact-leak risk at the code level, not just as policy.
+
+Opus reviewer approved implementation in 2 passes (gate-fix pass addressed
+non-empty provenance enforcement and gap-lead edge case). 215 tests green,
+ruff + mypy clean.
+
+---
+
+## Decision
+
+### Four-Stage Lead Taxonomy
+
+| Stage | Kind | Grounded? | Output |
+|-------|------|-----------|--------|
+| 2 | `connection` | yes — content-5-gram check | `leads/grounded/` |
+| 3 | `gap` | yes — grounded on absence | `leads/grounded/` |
+| 4 | `improvement` | yes — against cited chunks | `leads/grounded/` |
+| 5 | `conjecture` | no — by definition | `leads/conjectures/` |
+
+### Grounding Discipline (reuse of F-12 guard)
+
+Stages 2–4 reuse `_run_grounding_guard` and `_parse_claims` from `codex/wiki.py`
+directly. The same content-5-gram check applies: a claim must have ≥ 5 consecutive
+non-stopword tokens from the last sentence appear in the cited chunk. Ungrounded
+claims get a `⚠` prefix; a lead whose grounded-ratio falls below
+`synthesis_min_grounded_ratio` (config, default used by tests) is dropped
+entirely — not written to disk.
+
+### Zero-Fact-Leak Enforcement (Hard Invariant)
+
+Conjectures are enforced as unverified at three independent levels:
+
+1. **`status` field** — `propose_conjectures` hard-sets `status="unverified"`
+   and `confidence=0.0`. No caller can override this without modifying the
+   generator directly.
+
+2. **Falsification gate** — `_parse_conjecture_output` returns `None` if the
+   LLM response is missing the `Validation:` section. Conjectures without a
+   falsification path are silently dropped. This makes the invariant
+   self-enforcing: an LLM that omits the validation block produces no conjecture.
+
+3. **Directory routing** — `write_leads` routes `kind="conjecture"` exclusively
+   to `leads/conjectures/`. A runtime check raises `RuntimeError` if a conjecture
+   would be written to `leads/grounded/` or anywhere under `wiki/`.
+   `test_quarantine.py` asserts this routing for every output call.
+
+### Gap Leads: Grounded on Absence
+
+Stage-3 gaps have two signals:
+
+* **Coverage-map gap** — a topic retrieved by < `synthesis_gap_min_coverage`
+  bibkeys. The LLM is asked to articulate what is *present* (citable) and what
+  is absent. The absence itself needs no citation; the surrounding context does.
+* **Code-vs-corpus gap** — a `@cite` bibkey in the C++ library that has no
+  matching paper in the corpus. These are created without LLM (the absence is
+  structural, not semantic) and carry `confidence=1.0`.
+
+### Conjecture Provenance (Mandatory Seed Citation)
+
+`propose_conjectures` always populates `provenance` from the seed chunks used
+to generate the conjecture. A conjecture with an empty `provenance` list is
+rejected (the `Lead.__post_init__` ValueError guard). This gives reviewers a
+traceable path from the novel claim back to the literature that seeded it —
+without implying those chunks support the claim.
+
+### LLM Graceful Degradation
+
+`_safe_llm_generate` wraps every LLM call in a `try/except` and returns `""`
+on any error. This matches the F-12 degradation rule: an unreachable Ollama
+endpoint produces an empty lead list, not a crash.
+
+### Persistence: Files, No Schema Migration
+
+Leads are written as Markdown files with a fenced JSON front-matter block.
+No `schema.sql` migration is needed. `leads/INDEX.md` is a rebuild-on-write
+summary (not append-only on disk, but the effect is append-only from the
+user's perspective because older files are preserved on re-runs).
+
+---
+
+## Fallback
+
+If zero grounded leads are produced (e.g. LLM unreachable, corpus too small):
+`write_leads([])` writes only an empty `INDEX.md`. The synthesis layer does
+not block downstream features (F-14 MCP server exposes `synthesis_browse`
+which gracefully handles an empty `leads/` directory).
+
+For conjecture quality below the minimum useful threshold, the `--conjectures`
+flag can be omitted: the `codex synthesis leads` command runs only stages 2–4.
+
+---
+
+## Consequences
+
+- R-28: Lead/Provenance datamodel — `codex/synthesis.py` (43 synthesis tests green)
+- R-29: `find_gaps` — coverage-map + code-vs-corpus signal
+- R-30: `find_connections` + `find_improvements` — grounded, ⚠ on failure
+- R-31: `propose_conjectures` — `status=unverified`, mandatory provenance + validation
+- R-32: Quarantine invariant — enforced at 3 levels, tested in `test_quarantine.py`
+- R-33: `codex synthesis leads/conjectures/report` CLI — `test_cli.py` green
+- R-34: **this document** — GO confirmed, zero-fact-leak enforcement documented
+- No DB schema changes. All lead state in `leads/` directory (gitignored by default).
+- Ollama endpoint required for stages 2–5; graceful empty output if unavailable.