codex-py/docs/adr/ADR-F13-synthesis-engine.md

# 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.