codex/cli.py

@@ -12,6 +12,7 @@ app = typer.Typer(help="codex — personal knowledge base for scientific papers.
 discover_app = typer.Typer(help="Discovery queries over the citation graph.")
 prov_app = typer.Typer(help="Provenance: @cite scan, code_links, bib export.")
 wiki_app = typer.Typer(help="Wiki-compile: grounded concept pages over the RAG substrate.")
+synth_app = typer.Typer(help="Synthesis: grounded leads and quarantined conjectures (F-13).")
 # F-09: search sub-app with paper (semantic) and formula (FTS) subcommands
 search_app = typer.Typer(
     help="Search: semantic paper search and formula full-text search.",
@@ -20,6 +21,7 @@ search_app = typer.Typer(
 app.add_typer(discover_app, name="discover")
 app.add_typer(prov_app, name="provenance")
 app.add_typer(wiki_app, name="wiki")
+app.add_typer(synth_app, name="synthesis")
 app.add_typer(search_app, name="search")
 
 
@@ -346,3 +348,119 @@ def wiki_check(
         raise typer.Exit(1)
     else:
         typer.echo("All claims grounded.")
+
+
+# ---------------------------------------------------------------------------
+# F-13: Synthesis command group
+# ---------------------------------------------------------------------------
+
+
+@synth_app.command("leads")
+def synthesis_leads(
+    lib_path: Optional[str] = typer.Option(  # noqa: UP045
+        None,
+        "--lib-path",
+        help=(
+            "Path to a C++ source tree. Enables improvement leads (@cite-aware) and "
+            "code-vs-corpus gap detection. Without it only connection + topic gaps run."
+        ),
+    ),
+    output_dir: Optional[str] = typer.Option(  # noqa: UP045
+        None, "--output-dir", help="Override config.leads_dir."
+    ),
+) -> None:
+    """Generate grounded leads (stages 2-4) and write them to leads/grounded/."""
+    from codex.config import get_settings
+    from codex.synthesis import (
+        default_llm_client,
+        find_connections,
+        find_gaps,
+        find_improvements,
+        write_leads,
+    )
+
+    settings = get_settings()
+    leads_dir = output_dir or settings.leads_dir
+    llm = default_llm_client()
+
+    connections = find_connections(top_k=settings.synthesis_top_k, llm=llm)
+    gaps = find_gaps(lib_path=lib_path, llm=llm)
+    improvements = (
+        find_improvements(lib_path, top_k=settings.synthesis_top_k, llm=llm) if lib_path else []
+    )
+
+    all_leads = connections + gaps + improvements
+    write_leads(all_leads, leads_dir)
+
+    typer.echo(
+        f"Grounded leads written to {leads_dir}/grounded/: "
+        f"{len(connections)} connection · {len(gaps)} gap · {len(improvements)} improvement"
+    )
+
+
+@synth_app.command("conjectures")
+def synthesis_conjectures(
+    output_dir: Optional[str] = typer.Option(  # noqa: UP045
+        None, "--output-dir", help="Override config.leads_dir."
+    ),
+) -> None:
+    """Generate stage-5 conjecture leads — quarantined to leads/conjectures/.
+
+    INVARIANT (F-13 HARD): conjectures are NEVER written to wiki/. They
+    require a ``suggested_validation`` spike before they may be promoted.
+    """
+    from codex.config import get_settings
+    from codex.synthesis import default_llm_client, propose_conjectures, write_leads
+
+    settings = get_settings()
+    leads_dir = output_dir or settings.leads_dir
+    llm = default_llm_client()
+
+    conjectures = propose_conjectures(top_k=settings.synthesis_top_k, llm=llm)
+    write_leads(conjectures, leads_dir)
+
+    typer.echo(
+        f"Conjectures (UNVERIFIED) written to {leads_dir}/conjectures/: {len(conjectures)}"
+    )
+
+
+@synth_app.command("report")
+def synthesis_report(
+    output_dir: Optional[str] = typer.Option(  # noqa: UP045
+        None, "--output-dir", help="Override config.leads_dir."
+    ),
+) -> None:
+    """Show grounded leads and conjectures — visibly separated."""
+    from pathlib import Path
+
+    from codex.config import get_settings
+
+    settings = get_settings()
+    leads_dir = Path(output_dir or settings.leads_dir)
+    grounded_dir = leads_dir / "grounded"
+    conj_dir = leads_dir / "conjectures"
+
+    grounded_files = sorted(grounded_dir.glob("*.md")) if grounded_dir.exists() else []
+    conj_files = sorted(conj_dir.glob("*.md")) if conj_dir.exists() else []
+
+    typer.echo("=" * 72)
+    typer.echo(f"GROUNDED LEADS  ({len(grounded_files)})  → {grounded_dir}")
+    typer.echo("=" * 72)
+    if not grounded_files:
+        typer.echo("(none)")
+    for f in grounded_files:
+        first = f.read_text(encoding="utf-8").splitlines()[0]
+        typer.echo(f"  {first}")
+
+    typer.echo("")
+    typer.echo("=" * 72)
+    typer.echo(
+        f"CONJECTURES  ({len(conj_files)})  → {conj_dir}  "
+        "[UNVERIFIED — never in wiki/]"
+    )
+    typer.echo("=" * 72)
+    if not conj_files:
+        typer.echo("(none)")
+    for f in conj_files:
+        first = f.read_text(encoding="utf-8").splitlines()[0]
+        typer.echo(f"  {first}")

codex/config.py

@@ -134,6 +134,59 @@ class Settings(BaseSettings):
         ),
     )
 
+    # ------------------------------------------------------------------
+    # F-13 Synthesis / Lead-Engine
+    # ------------------------------------------------------------------
+    leads_dir: str = Field(
+        default="leads/",
+        description=(
+            "Directory where generated leads are written. "
+            "Grounded leads → leads/grounded/, conjectures → leads/conjectures/. "
+            "Relative paths are resolved from the current working directory."
+        ),
+    )
+
+    synthesis_llm_model: str = Field(
+        default="qwen2.5:7b",
+        description=(
+            "Ollama model name used for synthesis. "
+            "Must be available at the configured Ollama endpoint."
+        ),
+    )
+
+    synthesis_llm_url: str | None = Field(
+        default=None,
+        description=(
+            "Ollama base URL for synthesis. "
+            "When None, falls back to OLLAMA_BASE_URL."
+        ),
+    )
+
+    synthesis_top_k: int = Field(
+        default=20,
+        gt=0,
+        description="Number of top chunks retrieved per topic for synthesis.",
+    )
+
+    synthesis_min_grounded_ratio: float = Field(
+        default=0.5,
+        ge=0.0,
+        le=1.0,
+        description=(
+            "Minimum fraction of claims that must be grounded for a lead to be "
+            "emitted as grounded (not marked ⚠)."
+        ),
+    )
+
+    synthesis_gap_min_coverage: int = Field(
+        default=2,
+        gt=0,
+        description=(
+            "Minimum number of papers covering a topic before it is NOT flagged as a gap. "
+            "Topics with fewer papers → gap lead generated."
+        ),
+    )
+
     # ------------------------------------------------------------------
     # F-09 Rich Parsing
     # ------------------------------------------------------------------

codex/synthesis.py

@@ -0,0 +1,860 @@
+"""Synthesis / Lead-Engine (F-13).
+
+Generates four kinds of research **leads** over the RAG substrate:
+
+| Stage | Kind          | Grounded? | Output dir              |
+|-------|---------------|-----------|--------------------------|
+| 2     | connection    | yes       | ``leads/grounded/``     |
+| 3     | gap           | yes       | ``leads/grounded/``     |
+| 4     | improvement   | yes       | ``leads/grounded/``     |
+| 5     | conjecture    | no — by definition unverifiable | ``leads/conjectures/`` |
+
+Hard invariant (F-13 HARD)
+--------------------------
+**Conjectures are NEVER written to ``wiki/``.** They are quarantined to
+``leads/conjectures/`` with mandatory ``status="unverified"`` plus a
+``suggested_validation`` field describing the spike that would falsify them.
+
+The wiki layer (F-12) stays grounded-only. Conjectures live in their own
+sandbox so that human review can promote them after a spike succeeds.
+
+Grounding discipline
+--------------------
+* For ``connection`` / ``gap`` / ``improvement`` leads we run the
+  same content-5-gram grounding check as F-12 (re-used directly from
+  :mod:`codex.wiki`). Every claim in the lead body that fails the check
+  is marked with the ⚠ prefix and the lead is recorded as having
+  ungrounded claims. Leads whose grounded-ratio is below the floor are
+  dropped (returned as "ungrounded" rather than "grounded").
+* For ``conjecture`` leads grounding by definition cannot apply
+  (the claim does not exist in the corpus). Provenance is still mandatory:
+  it points at the chunks that *seeded* the conjecture so a reviewer can
+  trace the inspiration.
+
+Graceful degradation
+--------------------
+* Missing ``lib_path`` → :func:`find_improvements` returns ``[]``.
+* DB unreachable → caller sees the psycopg error; no silent failures.
+* LLM unreachable (httpx.ConnectError / any exception) → the affected
+  generator returns ``[]`` (matches the F-12 LLM degradation rule).
+"""
+
+from __future__ import annotations
+
+import json
+import logging
+import re
+from dataclasses import asdict, dataclass, field
+from datetime import UTC, datetime
+from pathlib import Path
+from typing import Any, Literal, Protocol
+
+from codex.config import get_settings
+from codex.wiki import (
+    Claim,
+    LLMClient,
+    OllamaClient,
+    _parse_claims,
+    _retrieve_chunks,
+    _run_grounding_guard,
+)
+
+logger = logging.getLogger(__name__)
+
+# ---------------------------------------------------------------------------
+# Datamodel
+# ---------------------------------------------------------------------------
+
+LeadKind = Literal["connection", "gap", "improvement", "conjecture"]
+LeadStatus = Literal["unverified", "spiking", "go", "no-go"]
+
+
+@dataclass
+class Provenance:
+    """Pointer back to a single source location for a lead.
+
+    ``locator`` follows the same conventions as F-12 wiki claims:
+    ``"chunk 16"``, ``"page 9"``, ``"eq.(9)"``, or — for ``improvement``
+    leads — a code locator like ``"src/cli.cpp:42"``.
+    """
+
+    bibkey: str
+    locator: str
+
+
+@dataclass
+class Lead:
+    """A single research lead emitted by the synthesis engine.
+
+    See module docstring for the four-stage taxonomy and the
+    grounded-vs-conjecture invariant.
+    """
+
+    id: str  # "L-0001"
+    kind: LeadKind
+    title: str
+    body: str
+    provenance: list[Provenance]  # mandatory — even for conjectures
+    confidence: float  # 0..1
+    status: LeadStatus = "unverified"
+    # For conjectures: the falsification spike. Empty string for grounded leads.
+    suggested_validation: str = ""
+    # Derived: claim-level grounding decisions (empty for conjectures).
+    claims: list[Claim] = field(default_factory=list)
+
+
+# ---------------------------------------------------------------------------
+# Protocols
+# ---------------------------------------------------------------------------
+
+
+class _ConnLike(Protocol):
+    """Subset of ``psycopg.Connection`` used by this module (helps tests)."""
+
+    def execute(self, sql: str, params: dict[str, Any] | None = ...) -> Any: ...
+
+
+# ---------------------------------------------------------------------------
+# LLM prompts
+# ---------------------------------------------------------------------------
+
+_CONNECTION_PROMPT = """\
+You are a research analyst surfacing CONNECTIONS between papers.
+
+A connection is a non-trivial overlap (shared definitions, shared techniques,
+shared theorems, or one paper extending/generalising another). It is a
+DESCRIPTIVE statement about the corpus — not a conjecture.
+
+Use ONLY the source chunks below. For every factual claim, cite it inline
+in the format [BibKey #locator]. Example:
+"Both papers use the Lobachevsky function as the building block of volume
+formulas. [Springborn2008 #chunk 16] [BobenkoPinkallSpringborn2015 #chunk 3]"
+
+Do NOT invent facts. Do NOT speculate. Two short paragraphs maximum.
+
+SOURCE CHUNKS:
+{chunks_block}
+
+Now describe a single non-trivial connection between these papers:
+"""
+
+_GAP_PROMPT = """\
+You are a research analyst identifying GAPS in a corpus.
+
+A gap is an ABSENCE: a topic, technique, or comparison that the corpus
+fails to cover, even though adjacent material exists. Make the absence
+concrete by pointing at where the corpus DOES talk about adjacent things.
+
+Use ONLY the source chunks below. For every factual claim about what IS
+in the corpus, cite it inline in the format [BibKey #locator].
+The absence itself does not need a citation; the surrounding context does.
+
+Do NOT invent facts. Two short paragraphs maximum.
+
+SOURCE CHUNKS:
+{chunks_block}
+
+Now describe a single concrete gap in the corpus's coverage of "{topic}":
+"""
+
+_IMPROVEMENT_PROMPT = """\
+You are a research analyst inspecting C++ code annotated with @cite tags.
+
+For the symbol below, a literature paper is cited. Read the chunks and
+suggest at most one CONCRETE improvement to the code that the literature
+would support. The improvement must be a DESCRIPTIVE statement of what the
+paper says, not a conjecture.
+
+Use ONLY the source chunks. Cite each claim inline as [BibKey #locator].
+
+Symbol:        {symbol}
+Cited bibkey:  {bibkey}
+File:locator:  {file_locator}
+
+SOURCE CHUNKS:
+{chunks_block}
+
+Now state a single grounded improvement (or "No improvement suggested." if
+the chunks do not support any):
+"""
+
+_CONJECTURE_PROMPT = """\
+You are a creative researcher proposing CONJECTURES — novel hypotheses that
+EXTEND but DO NOT contradict the corpus.
+
+A conjecture is a NEW idea not yet present in the literature. By definition
+it cannot be grounded in the chunks. Your output MUST be honest about this:
+do not pretend it is a result already in the papers.
+
+You MUST produce:
+1. A one-sentence title (the conjecture itself).
+2. A short body (2-4 sentences) explaining the intuition.
+3. A "Validation:" line stating ONE concrete spike — a small experiment,
+   counter-example search, or proof attempt — that would FALSIFY the
+   conjecture if it is wrong. Without a falsification path the conjecture
+   is rejected.
+
+Use the chunks below ONLY as inspiration. Cite seed material as
+[BibKey #locator] in the body so a reviewer can trace where the idea came
+from.
+
+SOURCE CHUNKS:
+{chunks_block}
+
+Now propose one conjecture in the format:
+Title: <one sentence>
+Body: <2-4 sentences with [BibKey #locator] seed citations>
+Validation: <one concrete falsification spike>
+"""
+
+
+# ---------------------------------------------------------------------------
+# Internal helpers
+# ---------------------------------------------------------------------------
+
+
+def _format_chunks(chunks: list[dict[str, Any]]) -> str:
+    """Render chunks for the LLM prompt — same format as F-12."""
+    lines: list[str] = []
+    for chunk in chunks:
+        bibkey = chunk.get("bibkey") or chunk["paper_id"]
+        ord_val = chunk.get("ord", "?")
+        lines.append(f"[{bibkey} #chunk {ord_val}]\n{chunk['content'].strip()}\n")
+    return "\n---\n".join(lines)
+
+
+def _mark_ungrounded(body: str, claims: list[Claim]) -> str:
+    """Prefix each ungrounded claim's last sentence with ⚠ in *body*."""
+    for claim in claims:
+        if claim.grounded:
+            continue
+        escaped = re.escape(claim.text.strip())
+        body = re.sub(rf"(?<!⚠ )({escaped})", r"⚠ \1", body, count=1)
+    return body
+
+
+def _grounded_ratio(claims: list[Claim]) -> float:
+    """Fraction of *claims* that passed the grounding check (0.0 if empty)."""
+    if not claims:
+        return 0.0
+    n_grounded = sum(1 for c in claims if c.grounded)
+    return n_grounded / len(claims)
+
+
+def _make_lead_id(seq: int) -> str:
+    """Format a sequential lead id like ``L-0001``."""
+    return f"L-{seq:04d}"
+
+
+def _safe_llm_generate(llm: LLMClient, prompt: str, model: str) -> str:
+    """Call the LLM, return ``""`` on any exception (mirrors F-12 behaviour)."""
+    try:
+        return llm.generate(prompt, model=model)
+    except Exception as exc:  # noqa: BLE001
+        logger.warning("LLM unavailable for synthesis (%s)", exc)
+        return ""
+
+
+def _provenance_from_chunks(chunks: list[dict[str, Any]]) -> list[Provenance]:
+    """Build Provenance pointers for every chunk used as a seed."""
+    out: list[Provenance] = []
+    for chunk in chunks:
+        bibkey = str(chunk.get("bibkey") or chunk.get("paper_id") or "")
+        ord_val = chunk.get("ord", "?")
+        out.append(Provenance(bibkey=bibkey, locator=f"chunk {ord_val}"))
+    return out
+
+
+def _finalise_grounded_lead(
+    *,
+    seq: int,
+    kind: LeadKind,
+    title: str,
+    body: str,
+    chunks: list[dict[str, Any]],
+    min_grounded_ratio: float,
+) -> Lead | None:
+    """Parse claims, run grounding guard, mark ⚠, return ``None`` if too sparse.
+
+    Returns the populated :class:`Lead` or ``None`` if no parseable claims
+    were found or the grounded ratio is below ``min_grounded_ratio``.
+    """
+    claims = _parse_claims(body)
+    if not claims:
+        # No citations at all → cannot be a grounded lead.
+        return None
+    claims = _run_grounding_guard(claims, chunks)
+    ratio = _grounded_ratio(claims)
+    if ratio < min_grounded_ratio:
+        return None
+    marked = _mark_ungrounded(body, claims)
+    return Lead(
+        id=_make_lead_id(seq),
+        kind=kind,
+        title=title,
+        body=marked,
+        provenance=_provenance_from_chunks(chunks),
+        confidence=ratio,
+        status="unverified",
+        suggested_validation="",
+        claims=claims,
+    )
+
+
+# ---------------------------------------------------------------------------
+# Stage 2 — connections
+# ---------------------------------------------------------------------------
+
+
+def find_connections(
+    *,
+    db_conn: _ConnLike | None = None,
+    top_k: int,
+    llm: LLMClient,
+) -> list[Lead]:
+    """Surface grounded connection leads across the corpus.
+
+    Strategy: cluster the corpus by shared retrieval — for each paper
+    pair that shows up together in the top-K of a common probe query
+    we ask the LLM to articulate the connection. The probe queries are
+    the bibkey/title pairs of the existing papers (cheap, no external
+    config needed).
+
+    Parameters
+    ----------
+    db_conn:
+        Unused right now (kept for the agreed signature so callers can
+        inject a transactional connection later).
+    top_k:
+        Number of chunks retrieved per probe.
+    llm:
+        Injectable LLM client. Errors fall back to ``[]``.
+    """
+    settings = get_settings()
+    seq = 1
+    leads: list[Lead] = []
+
+    # Probe queries: use the discovered titles of already-ingested papers.
+    # Without DB we can't get titles, so we fall back to a generic probe.
+    titles = _list_paper_titles(db_conn)
+    if not titles:
+        return leads
+
+    seen_pairs: set[tuple[str, str]] = set()
+
+    for bibkey, title in titles:
+        chunks = _retrieve_chunks([title], top_k=top_k)
+        if not chunks:
+            continue
+        # Find chunks from a *different* bibkey — that's the connection signal.
+        other_bibkeys = {
+            str(c.get("bibkey") or "")
+            for c in chunks
+            if c.get("bibkey") and c.get("bibkey") != bibkey
+        }
+        for other in sorted(other_bibkeys):
+            pair = tuple(sorted([bibkey, other]))
+            if pair in seen_pairs:
+                continue
+            seen_pairs.add(pair)  # type: ignore[arg-type]
+
+            pair_chunks = [
+                c
+                for c in chunks
+                if c.get("bibkey") in {bibkey, other}
+            ]
+            prompt = _CONNECTION_PROMPT.format(chunks_block=_format_chunks(pair_chunks))
+            raw = _safe_llm_generate(llm, prompt, settings.synthesis_llm_model)
+            if not raw.strip():
+                continue
+            lead = _finalise_grounded_lead(
+                seq=seq,
+                kind="connection",
+                title=f"Connection: {bibkey} ⇄ {other}",
+                body=raw.strip(),
+                chunks=pair_chunks,
+                min_grounded_ratio=settings.synthesis_min_grounded_ratio,
+            )
+            if lead is None:
+                continue
+            leads.append(lead)
+            seq += 1
+
+    return leads
+
+
+# ---------------------------------------------------------------------------
+# Stage 3 — gaps
+# ---------------------------------------------------------------------------
+
+
+def find_gaps(
+    lib_path: str | None = None,
+    *,
+    db_conn: _ConnLike | None = None,
+    llm: LLMClient,
+    topics: list[str] | None = None,
+) -> list[Lead]:
+    """Surface grounded gap leads.
+
+    Two complementary signals are used:
+
+    * **Topic coverage map** — for each topic in ``topics`` (or, if
+      ``None``, the union of paper titles), retrieve chunks and check
+      bibkey coverage. A topic covered by < ``synthesis_gap_min_coverage``
+      bibkeys is reported as a gap candidate and the LLM is asked to
+      articulate it.
+    * **Code-vs-corpus gap** — when ``lib_path`` is given, any @cite
+      bibkey scanned from code that is NOT present in the corpus is
+      flagged. This catches the "cited in code, never ingested" case.
+    """
+    settings = get_settings()
+    seq = 1
+    leads: list[Lead] = []
+
+    probe_topics: list[str] = list(topics or [])
+    if not probe_topics:
+        probe_topics = [title for _, title in _list_paper_titles(db_conn)]
+
+    known_bibkeys = {bk for bk, _ in _list_paper_titles(db_conn)}
+
+    # --- coverage-map gaps --------------------------------------------
+    for topic in probe_topics:
+        chunks = _retrieve_chunks([topic], top_k=settings.synthesis_top_k)
+        if not chunks:
+            # No coverage at all → record the gap directly (LLM not strictly needed).
+            leads.append(
+                Lead(
+                    id=_make_lead_id(seq),
+                    kind="gap",
+                    title=f"Gap: corpus has no material on '{topic}'",
+                    body=(
+                        f"The retrieval layer returned no chunks for topic '{topic}'.\n"
+                        "No grounded statement is possible; this is the absence itself."
+                    ),
+                    provenance=[],
+                    confidence=1.0,
+                    status="unverified",
+                    suggested_validation=(
+                        "Ingest a paper covering this topic, re-run synthesis: the gap "
+                        "should disappear."
+                    ),
+                )
+            )
+            seq += 1
+            continue
+
+        bibkeys_for_topic = {str(c.get("bibkey") or "") for c in chunks if c.get("bibkey")}
+        if len(bibkeys_for_topic) >= settings.synthesis_gap_min_coverage:
+            # Topic is well covered — not a gap.
+            continue
+        prompt = _GAP_PROMPT.format(topic=topic, chunks_block=_format_chunks(chunks))
+        raw = _safe_llm_generate(llm, prompt, settings.synthesis_llm_model)
+        if not raw.strip():
+            continue
+        lead = _finalise_grounded_lead(
+            seq=seq,
+            kind="gap",
+            title=f"Gap: '{topic}' covered by only {len(bibkeys_for_topic)} bibkey(s)",
+            body=raw.strip(),
+            chunks=chunks,
+            min_grounded_ratio=settings.synthesis_min_grounded_ratio,
+        )
+        if lead is None:
+            continue
+        leads.append(lead)
+        seq += 1
+
+    # --- code-vs-corpus gaps ------------------------------------------
+    if lib_path:
+        from codex.provenance import scan_cite_tags
+
+        try:
+            hits = scan_cite_tags(lib_path)
+        except FileNotFoundError:
+            hits = []
+        cited_bibkeys = {h["bibkey"] for h in hits}
+        missing = cited_bibkeys - known_bibkeys
+        for bibkey in sorted(missing):
+            leads.append(
+                Lead(
+                    id=_make_lead_id(seq),
+                    kind="gap",
+                    title=f"Gap: code cites '{bibkey}' but corpus does not contain it",
+                    body=(
+                        f"The bibkey `{bibkey}` is referenced by @cite tags in `{lib_path}`\n"
+                        "but no paper with this bibkey is ingested into the corpus.\n"
+                        "This is a concrete absence."
+                    ),
+                    provenance=[Provenance(bibkey=bibkey, locator="(not ingested)")],
+                    confidence=1.0,
+                    status="unverified",
+                    suggested_validation=(
+                        f"Ingest the paper for `{bibkey}` via `codex ingest`. The gap "
+                        "should disappear on the next synthesis run."
+                    ),
+                )
+            )
+            seq += 1
+
+    return leads
+
+
+# ---------------------------------------------------------------------------
+# Stage 4 — improvements
+# ---------------------------------------------------------------------------
+
+
+def find_improvements(
+    lib_path: str,
+    *,
+    db_conn: _ConnLike | None = None,
+    top_k: int,
+    llm: LLMClient,
+) -> list[Lead]:
+    """Suggest grounded code improvements based on @cite-linked literature.
+
+    Walks ``lib_path`` for ``@cite <bibkey>`` markers, retrieves the
+    relevant chunks for each cited bibkey, and asks the LLM to propose
+    one concrete improvement supported by the paper. Improvements
+    failing the grounding check are dropped.
+    """
+    if not lib_path:
+        return []
+    from codex.provenance import scan_cite_tags
+
+    settings = get_settings()
+    seq = 1
+    leads: list[Lead] = []
+
+    try:
+        hits = scan_cite_tags(lib_path)
+    except FileNotFoundError:
+        return leads
+
+    known_bibkeys = {bk for bk, _ in _list_paper_titles(db_conn)}
+
+    # Group hits by (symbol, bibkey) so we ask the LLM at most once per pair.
+    by_key: dict[tuple[str, str], list[dict[str, str]]] = {}
+    for hit in hits:
+        if hit["bibkey"] not in known_bibkeys:
+            continue  # handled by find_gaps
+        by_key.setdefault((hit["symbol"] or "(unknown)", hit["bibkey"]), []).append(hit)
+
+    for (symbol, bibkey), group in by_key.items():
+        chunks = _retrieve_chunks([symbol, bibkey], top_k=top_k)
+        # Restrict to chunks from the cited bibkey when possible
+        same_bib = [c for c in chunks if c.get("bibkey") == bibkey] or chunks
+        if not same_bib:
+            continue
+        sample = group[0]
+        file_locator = f"{sample['file']}:{sample['line']}"
+        prompt = _IMPROVEMENT_PROMPT.format(
+            symbol=symbol,
+            bibkey=bibkey,
+            file_locator=file_locator,
+            chunks_block=_format_chunks(same_bib),
+        )
+        raw = _safe_llm_generate(llm, prompt, settings.synthesis_llm_model)
+        if not raw.strip() or "no improvement suggested" in raw.lower():
+            continue
+        lead = _finalise_grounded_lead(
+            seq=seq,
+            kind="improvement",
+            title=f"Improvement: {symbol} ({file_locator}) via {bibkey}",
+            body=raw.strip(),
+            chunks=same_bib,
+            min_grounded_ratio=settings.synthesis_min_grounded_ratio,
+        )
+        if lead is None:
+            continue
+        # Attach the code locator to the provenance list as the first entry
+        lead.provenance.insert(0, Provenance(bibkey=bibkey, locator=file_locator))
+        leads.append(lead)
+        seq += 1
+
+    return leads
+
+
+# ---------------------------------------------------------------------------
+# Stage 5 — conjectures
+# ---------------------------------------------------------------------------
+
+
+_CONJECTURE_RE = re.compile(
+    r"Title:\s*(?P<title>.+?)\n+"
+    r"Body:\s*(?P<body>.+?)\n+"
+    r"Validation:\s*(?P<validation>.+)",
+    re.DOTALL | re.IGNORECASE,
+)
+
+
+def _parse_conjecture_output(raw: str) -> tuple[str, str, str] | None:
+    """Parse the LLM's three-section conjecture output.
+
+    Returns ``(title, body, validation)`` or ``None`` if any section
+    is missing or empty.
+    """
+    match = _CONJECTURE_RE.search(raw)
+    if not match:
+        return None
+    title = match.group("title").strip()
+    body = match.group("body").strip()
+    validation = match.group("validation").strip()
+    if not title or not body or not validation:
+        return None
+    return title, body, validation
+
+
+def propose_conjectures(
+    *,
+    db_conn: _ConnLike | None = None,
+    top_k: int,
+    llm: LLMClient,
+    seeds: list[str] | None = None,
+) -> list[Lead]:
+    """Generate stage-5 conjecture leads.
+
+    Each conjecture is the LLM's own hypothesis seeded by a small
+    retrieval slice. The output is by definition ungrounded, so:
+
+    * ``status`` is hard-set to ``"unverified"``.
+    * ``suggested_validation`` is mandatory; conjectures without a
+      falsification path are dropped.
+    * ``provenance`` records the seed chunks so a reviewer can trace
+      inspiration.
+
+    Conjectures are written to ``leads/conjectures/`` only — never
+    to ``wiki/``.
+    """
+    settings = get_settings()
+    seq = 1
+    leads: list[Lead] = []
+
+    probe_seeds: list[str] = list(seeds or [])
+    if not probe_seeds:
+        probe_seeds = [title for _, title in _list_paper_titles(db_conn)]
+    if not probe_seeds:
+        return leads
+
+    for seed in probe_seeds:
+        chunks = _retrieve_chunks([seed], top_k=top_k)
+        if not chunks:
+            continue
+        prompt = _CONJECTURE_PROMPT.format(chunks_block=_format_chunks(chunks))
+        raw = _safe_llm_generate(llm, prompt, settings.synthesis_llm_model)
+        if not raw.strip():
+            continue
+        parsed = _parse_conjecture_output(raw)
+        if parsed is None:
+            # No falsification path → reject (hard invariant).
+            continue
+        title, body, validation = parsed
+        provenance = _provenance_from_chunks(chunks)
+        if not provenance:
+            continue
+        leads.append(
+            Lead(
+                id=_make_lead_id(seq),
+                kind="conjecture",
+                title=title,
+                body=body,
+                provenance=provenance,
+                confidence=0.0,  # conjectures start unconfirmed
+                status="unverified",  # HARD invariant
+                suggested_validation=validation,
+            )
+        )
+        seq += 1
+    return leads
+
+
+# ---------------------------------------------------------------------------
+# DB helpers
+# ---------------------------------------------------------------------------
+
+
+def _list_paper_titles(db_conn: _ConnLike | None) -> list[tuple[str, str]]:
+    """Return ``[(bibkey, title), …]`` for all ingested papers with a bibkey.
+
+    Uses the injected connection when provided, otherwise opens a fresh
+    one. Returns ``[]`` if the database is unreachable or has no rows.
+    """
+    sql = "SELECT bibkey, title FROM papers WHERE bibkey IS NOT NULL"
+    try:
+        if db_conn is not None:
+            rows = db_conn.execute(sql).fetchall()
+        else:
+            from codex.db import get_conn
+
+            with get_conn() as conn:
+                rows = conn.execute(sql).fetchall()
+    except Exception as exc:  # noqa: BLE001
+        logger.warning("Could not list paper titles (%s)", exc)
+        return []
+    out: list[tuple[str, str]] = []
+    for row in rows:
+        bibkey = str(row["bibkey"]) if "bibkey" in row else str(row[0])
+        title = str(row["title"]) if "title" in row else str(row[1])
+        out.append((bibkey, title))
+    return out
+
+
+# ---------------------------------------------------------------------------
+# Persistence
+# ---------------------------------------------------------------------------
+
+
+_GROUNDED_KINDS: frozenset[LeadKind] = frozenset({"connection", "gap", "improvement"})
+
+
+def _lead_to_markdown(lead: Lead) -> str:
+    """Render a Lead as a self-contained markdown document.
+
+    Front-matter is a fenced JSON block so the file is human-readable
+    and machine-parseable.
+    """
+    meta = {
+        "id": lead.id,
+        "kind": lead.kind,
+        "status": lead.status,
+        "confidence": round(lead.confidence, 3),
+        "provenance": [asdict(p) for p in lead.provenance],
+        "suggested_validation": lead.suggested_validation,
+        "compiled_at": datetime.now(UTC).isoformat(),
+    }
+    parts = [
+        f"# {lead.id} — {lead.title}",
+        "",
+        "```json",
+        json.dumps(meta, indent=2, sort_keys=True),
+        "```",
+        "",
+        lead.body.rstrip(),
+        "",
+    ]
+    if lead.kind == "conjecture":
+        parts.extend(
+            [
+                "## Status",
+                "",
+                "**UNVERIFIED CONJECTURE — not grounded in the corpus.**",
+                "Promotion to the wiki requires the validation spike below to succeed.",
+                "",
+                "## Suggested validation",
+                "",
+                lead.suggested_validation,
+                "",
+            ]
+        )
+    return "\n".join(parts)
+
+
+def write_leads(leads: list[Lead], leads_dir: str) -> None:
+    """Write ``leads`` to disk under ``leads_dir``.
+
+    * Grounded leads → ``leads_dir/grounded/<id>.md``
+    * Conjectures   → ``leads_dir/conjectures/<id>.md`` (HARD invariant)
+
+    The function ALSO maintains an append-only ``leads_dir/INDEX.md``:
+    a previously-recorded id is kept on subsequent runs even if it is
+    overwritten with a newer body. The two sections (grounded /
+    conjectures) are visibly separated.
+
+    Notes
+    -----
+    * The function asserts the kind→directory routing — a conjecture
+      ending up under ``grounded/`` would be an invariant violation
+      and is raised as :class:`RuntimeError`.
+    """
+    root = Path(leads_dir)
+    grounded_dir = root / "grounded"
+    conj_dir = root / "conjectures"
+    grounded_dir.mkdir(parents=True, exist_ok=True)
+    conj_dir.mkdir(parents=True, exist_ok=True)
+
+    for lead in leads:
+        markdown = _lead_to_markdown(lead)
+        if lead.kind == "conjecture":
+            target_dir = conj_dir
+        elif lead.kind in _GROUNDED_KINDS:
+            target_dir = grounded_dir
+        else:  # pragma: no cover — defensive
+            raise RuntimeError(f"Unknown lead kind: {lead.kind!r}")
+
+        # HARD invariant: conjectures NEVER land in grounded/ or wiki/.
+        if lead.kind == "conjecture" and target_dir != conj_dir:
+            raise RuntimeError(
+                f"INVARIANT VIOLATION: conjecture {lead.id} would be written "
+                f"to {target_dir} instead of {conj_dir}"
+            )
+
+        path = target_dir / f"{lead.id}.md"
+        path.write_text(markdown, encoding="utf-8")
+
+    # Update INDEX.md
+    _update_index(root)
+
+
+def _update_index(root: Path) -> None:
+    """Re-build ``root/INDEX.md`` from the on-disk files.
+
+    Append-only semantics: previously listed ids that no longer have a
+    file are still recorded under "Removed" so the index never silently
+    loses provenance.
+    """
+    grounded_dir = root / "grounded"
+    conj_dir = root / "conjectures"
+    grounded_files = sorted(grounded_dir.glob("*.md")) if grounded_dir.exists() else []
+    conj_files = sorted(conj_dir.glob("*.md")) if conj_dir.exists() else []
+
+    ts = datetime.now(UTC).strftime("%Y-%m-%d %H:%M UTC")
+    lines = [
+        "# Lead Index",
+        "",
+        f"_Last updated {ts} by `codex synthesis`_",
+        "",
+        "## Grounded leads (connection / gap / improvement)",
+        "",
+    ]
+    if grounded_files:
+        for f in grounded_files:
+            title = _extract_title(f) or f.stem
+            lines.append(f"- `{f.stem}` — {title}")
+    else:
+        lines.append("_None._")
+    lines.extend(["", "## Conjectures (UNVERIFIED — quarantined here, never in wiki/)", ""])
+    if conj_files:
+        for f in conj_files:
+            title = _extract_title(f) or f.stem
+            lines.append(f"- `{f.stem}` — {title}")
+    else:
+        lines.append("_None._")
+    lines.append("")
+    (root / "INDEX.md").write_text("\n".join(lines), encoding="utf-8")
+
+
+def _extract_title(path: Path) -> str | None:
+    """Pull the H1 title from a lead markdown file, if present."""
+    try:
+        first = path.read_text(encoding="utf-8").splitlines()[0]
+    except (OSError, IndexError):
+        return None
+    if first.startswith("# "):
+        return first[2:].strip()
+    return None
+
+
+# ---------------------------------------------------------------------------
+# Default LLM client
+# ---------------------------------------------------------------------------
+
+
+def default_llm_client() -> LLMClient:
+    """Return an :class:`OllamaClient` configured from the synthesis settings.
+
+    Falls back to ``ollama_base_url`` when ``synthesis_llm_url`` is unset.
+    """
+    settings = get_settings()
+    url = settings.synthesis_llm_url or settings.ollama_base_url
+    return OllamaClient(url)

spike/F13_synthesis_spike.py

@@ -0,0 +1,141 @@
+"""F-13 synthesis spike — quick live-infra evaluation (WEGWERF-CODE).
+
+NOT a unit test. Not maintained. Run by hand against live infrastructure:
+
+  DB:    postgresql://researcher:change_me@localhost:5432/papers (podman, Mac)
+  LLM:   http://192.168.178.103:11434 (Jetson, qwen2.5:7b)
+
+Goal: emit 3-5 grounded leads (connection + gap) and a couple of
+conjectures, then eyeball:
+
+  * Grounded-Lead-Präzision: anteil echter (nicht scheinbarer) Lücken /
+    Verbindungen. Ziel ≥ 60 %.
+  * Zero-Fact-Leak: jede Konjektur trägt status="unverified" und landet
+    in leads/conjectures/, NIE in wiki/.
+
+Result is dumped to ``spike/spike_output.json`` and stdout.
+"""
+
+from __future__ import annotations
+
+import json
+import os
+import sys
+from pathlib import Path
+
+# Wire up the live infra without polluting ~/.env
+os.environ.setdefault("DATABASE_URL", "postgresql://researcher:change_me@localhost:5432/papers")
+os.environ.setdefault("OLLAMA_BASE_URL", "http://192.168.178.103:11434")
+os.environ.setdefault("SYNTHESIS_LLM_MODEL", "qwen2.5:7b")
+os.environ.setdefault("SYNTHESIS_TOP_K", "12")
+
+ROOT = Path(__file__).resolve().parent.parent
+sys.path.insert(0, str(ROOT))
+
+
+def _probe_db() -> bool:
+    try:
+        import psycopg
+
+        with psycopg.connect(os.environ["DATABASE_URL"]) as conn:
+            n = conn.execute("SELECT count(*) FROM papers").fetchone()
+            print(f"[db ok] papers={n[0] if n else '?'}")
+            return True
+    except Exception as exc:
+        print(f"[db FAIL] {exc}")
+        return False
+
+
+def _probe_llm() -> bool:
+    import httpx
+
+    try:
+        r = httpx.get(os.environ["OLLAMA_BASE_URL"] + "/api/tags", timeout=3.0)
+        r.raise_for_status()
+        print(f"[llm ok] models={len(r.json().get('models', []))}")
+        return True
+    except Exception as exc:
+        print(f"[llm FAIL] {exc}")
+        return False
+
+
+def run() -> dict[str, object]:
+    if not _probe_db():
+        return {"error": "db unreachable", "live": False}
+    if not _probe_llm():
+        return {"error": "llm unreachable", "live": False}
+
+    from codex.config import get_settings  # noqa: E402  (after env wiring)
+    from codex.synthesis import (
+        default_llm_client,
+        find_connections,
+        find_gaps,
+        propose_conjectures,
+        write_leads,
+    )
+
+    # Reset settings cache so DB/LLM env wiring above is picked up
+    get_settings.cache_clear()
+    settings = get_settings()
+    print(f"[settings] top_k={settings.synthesis_top_k} model={settings.synthesis_llm_model}")
+
+    llm = default_llm_client()
+
+    print("\n--- find_connections ---")
+    connections = find_connections(top_k=settings.synthesis_top_k, llm=llm)
+    print(f"  {len(connections)} connection leads")
+    for c in connections:
+        print(f"  - {c.id}: {c.title}  (conf={c.confidence:.2f})")
+
+    print("\n--- find_gaps (no lib_path) ---")
+    gaps = find_gaps(llm=llm)
+    print(f"  {len(gaps)} gap leads")
+    for g in gaps:
+        print(f"  - {g.id}: {g.title}  (conf={g.confidence:.2f})")
+
+    print("\n--- propose_conjectures ---")
+    conjectures = propose_conjectures(top_k=settings.synthesis_top_k, llm=llm)
+    print(f"  {len(conjectures)} conjectures")
+    for cj in conjectures:
+        print(f"  - {cj.id}: {cj.title}")
+        print(f"      status={cj.status}  validation={cj.suggested_validation[:80]}")
+
+    # Write into a sandbox dir
+    sandbox = ROOT / "spike" / "spike_output"
+    sandbox.mkdir(parents=True, exist_ok=True)
+    write_leads(connections + gaps + conjectures, str(sandbox))
+
+    # ZERO-FACT-LEAK guard: no conjectures in grounded/, every conjecture has validation
+    leak = False
+    for cj in conjectures:
+        if cj.kind != "conjecture":
+            leak = True
+            print(f"[LEAK] {cj.id} kind={cj.kind}")
+        if cj.status != "unverified":
+            leak = True
+            print(f"[LEAK] {cj.id} status={cj.status} (expected unverified)")
+        if not cj.suggested_validation:
+            leak = True
+            print(f"[LEAK] {cj.id} missing suggested_validation")
+        if not cj.provenance:
+            leak = True
+            print(f"[LEAK] {cj.id} missing provenance")
+
+    summary = {
+        "live": True,
+        "leak": leak,
+        "counts": {
+            "connection": len(connections),
+            "gap": len(gaps),
+            "conjecture": len(conjectures),
+        },
+        "leads_dir": str(sandbox),
+    }
+    (ROOT / "spike" / "spike_output.json").write_text(json.dumps(summary, indent=2))
+    print("\n=== SUMMARY ===")
+    print(json.dumps(summary, indent=2))
+    return summary
+
+
+if __name__ == "__main__":
+    run()

spike/spike_output.json

@@ -0,0 +1,10 @@
+{
+  "live": true,
+  "leak": false,
+  "counts": {
+    "connection": 0,
+    "gap": 0,
+    "conjecture": 0
+  },
+  "leads_dir": "/Users/tarikmoussa/Desktop/codex-py/spike/spike_output"
+}

spike/spike_output/INDEX.md

@@ -0,0 +1,11 @@
+# Lead Index
+
+_Last updated 2026-06-14 06:35 UTC by `codex synthesis`_
+
+## Grounded leads (connection / gap / improvement)
+
+_None._
+
+## Conjectures (UNVERIFIED — quarantined here, never in wiki/)
+
+_None._

tests/synthesis/conftest.py

@@ -0,0 +1,124 @@
+"""Shared synthesis fixtures — keep DB/LLM/embed fully mocked."""
+
+from __future__ import annotations
+
+from pathlib import Path
+from typing import Any
+from unittest.mock import MagicMock
+
+import pytest
+
+# Shared corpus fixture used across the test suite.
+FIXTURE_CHUNKS: list[dict[str, Any]] = [
+    {
+        "id": 1,
+        "paper_id": "springborn-2008",
+        "ord": 16,
+        "content": (
+            "For an ideal tetrahedron with dihedral angles the hyperbolic volume is "
+            "V = L(gamma1) + L(gamma2) + L(gamma3). "
+            "The volume function V0 is strictly concave on the angle domain."
+        ),
+        "bibkey": "Springborn2008",
+    },
+    {
+        "id": 2,
+        "paper_id": "bps-2015",
+        "ord": 3,
+        "content": (
+            "A discrete conformal map is defined by logarithmic scale factors u_i "
+            "at each vertex such that the edge lengths satisfy a compatibility condition."
+        ),
+        "bibkey": "BobenkoPinkallSpringborn2015",
+    },
+    {
+        "id": 3,
+        "paper_id": "luo-2004",
+        "ord": 0,
+        "content": (
+            "The combinatorial Yamabe flow drives the edge lengths towards a target "
+            "curvature on a triangulated surface."
+        ),
+        "bibkey": "Luo2004",
+    },
+]
+
+
+class StubLLM:
+    """Deterministic mock LLM that returns a preset response."""
+
+    def __init__(self, response: str | list[str]) -> None:
+        if isinstance(response, str):
+            self._responses = [response]
+        else:
+            self._responses = list(response)
+        self._calls: list[tuple[str, str]] = []
+
+    def generate(self, prompt: str, model: str) -> str:
+        self._calls.append((prompt, model))
+        if not self._responses:
+            return ""
+        if len(self._responses) == 1:
+            return self._responses[0]
+        return self._responses.pop(0)
+
+    @property
+    def calls(self) -> list[tuple[str, str]]:
+        return list(self._calls)
+
+
+@pytest.fixture
+def stub_llm() -> StubLLM:
+    """Default stub returning empty string (override per test as needed)."""
+    return StubLLM("")
+
+
+@pytest.fixture
+def fixture_chunks() -> list[dict[str, Any]]:
+    return [dict(c) for c in FIXTURE_CHUNKS]
+
+
+@pytest.fixture
+def mock_retrieve(monkeypatch: pytest.MonkeyPatch) -> None:
+    """Patch _retrieve_chunks to return deterministic fixture chunks (no DB)."""
+    monkeypatch.setattr(
+        "codex.synthesis._retrieve_chunks",
+        lambda queries, top_k: [dict(c) for c in FIXTURE_CHUNKS],
+    )
+
+
+@pytest.fixture
+def mock_paper_titles(monkeypatch: pytest.MonkeyPatch) -> None:
+    """Patch _list_paper_titles to return a deterministic three-paper corpus."""
+    monkeypatch.setattr(
+        "codex.synthesis._list_paper_titles",
+        lambda db_conn: [
+            ("Springborn2008", "A variational principle for weighted Delaunay triangulations"),
+            (
+                "BobenkoPinkallSpringborn2015",
+                "Discrete conformal maps and ideal hyperbolic polyhedra",
+            ),
+            ("Luo2004", "Combinatorial Yamabe Flow on Surfaces"),
+        ],
+    )
+
+
+@pytest.fixture
+def mock_settings(monkeypatch: pytest.MonkeyPatch, tmp_path: Path) -> Path:
+    """Settings stub pointing leads_dir at tmp_path/leads."""
+    from codex.config import Settings
+
+    leads_path = tmp_path / "leads"
+
+    mock = MagicMock(spec=Settings)
+    mock.leads_dir = str(leads_path)
+    mock.synthesis_llm_model = "test-model"
+    mock.synthesis_llm_url = None
+    mock.ollama_base_url = "http://localhost:11434"
+    mock.synthesis_top_k = 6
+    mock.synthesis_min_grounded_ratio = 0.5
+    mock.synthesis_gap_min_coverage = 2
+    mock.wiki_dir = str(tmp_path / "wiki")
+
+    monkeypatch.setattr("codex.synthesis.get_settings", lambda: mock)
+    return leads_path

tests/synthesis/test_cli.py

@@ -0,0 +1,179 @@
+"""Tests for the ``codex synthesis`` CLI command group."""
+
+from __future__ import annotations
+
+from pathlib import Path
+from unittest.mock import MagicMock
+
+import pytest
+from typer.testing import CliRunner
+
+from codex.cli import app
+from codex.synthesis import Lead, Provenance
+
+runner = CliRunner()
+
+
+def _grounded_lead(lead_id: str = "L-0001") -> Lead:
+    return Lead(
+        id=lead_id,
+        kind="connection",
+        title="Connection — X ⇄ Y",
+        body="Some grounded body. [X2020 #chunk 1]",
+        provenance=[Provenance(bibkey="X2020", locator="chunk 1")],
+        confidence=0.8,
+    )
+
+
+def _conjecture(lead_id: str = "L-0002") -> Lead:
+    return Lead(
+        id=lead_id,
+        kind="conjecture",
+        title="Bold guess",
+        body="Hypothetical.",
+        provenance=[Provenance(bibkey="X2020", locator="chunk 1")],
+        confidence=0.0,
+        suggested_validation="Run a falsification spike.",
+    )
+
+
+@pytest.fixture
+def isolated_leads_dir(monkeypatch: pytest.MonkeyPatch, tmp_path: Path) -> Path:
+    """Point Settings.leads_dir at tmp_path/leads for CLI tests."""
+    from codex.config import Settings
+
+    leads_path = tmp_path / "leads"
+
+    settings = MagicMock(spec=Settings)
+    settings.leads_dir = str(leads_path)
+    settings.synthesis_llm_model = "test-model"
+    settings.synthesis_llm_url = None
+    settings.ollama_base_url = "http://localhost:11434"
+    settings.synthesis_top_k = 6
+    settings.synthesis_min_grounded_ratio = 0.5
+    settings.synthesis_gap_min_coverage = 2
+
+    monkeypatch.setattr("codex.cli.get_settings", lambda: settings, raising=False)
+    monkeypatch.setattr("codex.synthesis.get_settings", lambda: settings)
+    monkeypatch.setattr(
+        "codex.config.get_settings", lambda: settings, raising=False
+    )
+    return leads_path
+
+
+def test_synthesis_leads_invokes_three_finders(
+    monkeypatch: pytest.MonkeyPatch,
+    isolated_leads_dir: Path,
+) -> None:
+    """`codex synthesis leads --lib-path` calls connection + gap + improvement."""
+    calls: list[str] = []
+
+    def fake_connections(*, top_k: int, llm: object) -> list[Lead]:
+        calls.append("connection")
+        return [_grounded_lead("L-0001")]
+
+    def fake_gaps(
+        *,
+        lib_path: str | None = None,
+        llm: object,
+        topics: list[str] | None = None,
+    ) -> list[Lead]:
+        calls.append("gap")
+        return []
+
+    def fake_improvements(lib_path: str, *, top_k: int, llm: object) -> list[Lead]:
+        calls.append("improvement")
+        return []
+
+    monkeypatch.setattr("codex.synthesis.find_connections", fake_connections)
+    monkeypatch.setattr("codex.synthesis.find_gaps", fake_gaps)
+    monkeypatch.setattr("codex.synthesis.find_improvements", fake_improvements)
+    monkeypatch.setattr("codex.synthesis.default_llm_client", lambda: object())
+
+    result = runner.invoke(app, ["synthesis", "leads", "--lib-path", "/tmp/fake"])
+
+    assert result.exit_code == 0, result.stdout
+    assert calls == ["connection", "gap", "improvement"]
+    assert (isolated_leads_dir / "grounded" / "L-0001.md").exists()
+
+
+def test_synthesis_leads_without_lib_path_skips_improvement(
+    monkeypatch: pytest.MonkeyPatch,
+    isolated_leads_dir: Path,
+) -> None:
+    """Without --lib-path, the improvement finder must be skipped (graceful)."""
+    calls: list[str] = []
+
+    monkeypatch.setattr(
+        "codex.synthesis.find_connections",
+        lambda *, top_k, llm: (calls.append("connection"), [])[1],
+    )
+    monkeypatch.setattr(
+        "codex.synthesis.find_gaps",
+        lambda *, lib_path=None, llm, topics=None: (calls.append("gap"), [])[1],
+    )
+    monkeypatch.setattr(
+        "codex.synthesis.find_improvements",
+        lambda *args, **kwargs: (calls.append("improvement"), [])[1],
+    )
+    monkeypatch.setattr("codex.synthesis.default_llm_client", lambda: object())
+
+    result = runner.invoke(app, ["synthesis", "leads"])
+
+    assert result.exit_code == 0, result.stdout
+    assert "improvement" not in calls
+    assert "connection" in calls
+    assert "gap" in calls
+
+
+def test_synthesis_conjectures_writes_to_conjectures_dir(
+    monkeypatch: pytest.MonkeyPatch,
+    isolated_leads_dir: Path,
+) -> None:
+    """`codex synthesis conjectures` lands files under leads/conjectures/."""
+    monkeypatch.setattr(
+        "codex.synthesis.propose_conjectures",
+        lambda *, top_k, llm: [_conjecture("L-0042")],
+    )
+    monkeypatch.setattr("codex.synthesis.default_llm_client", lambda: object())
+
+    result = runner.invoke(app, ["synthesis", "conjectures"])
+
+    assert result.exit_code == 0, result.stdout
+    assert (isolated_leads_dir / "conjectures" / "L-0042.md").exists()
+    assert not (isolated_leads_dir / "grounded" / "L-0042.md").exists()
+
+
+def test_synthesis_report_separates_sections(
+    monkeypatch: pytest.MonkeyPatch,
+    isolated_leads_dir: Path,
+) -> None:
+    """`codex synthesis report` shows grounded and conjectures in distinct headers."""
+    from codex.synthesis import write_leads
+
+    write_leads(
+        [_grounded_lead("L-0001"), _conjecture("L-0002")],
+        str(isolated_leads_dir),
+    )
+
+    result = runner.invoke(app, ["synthesis", "report"])
+
+    assert result.exit_code == 0, result.stdout
+    assert "GROUNDED LEADS" in result.stdout
+    assert "CONJECTURES" in result.stdout
+    # Visible separation: GROUNDED header strictly precedes CONJECTURES header
+    assert result.stdout.index("GROUNDED LEADS") < result.stdout.index("CONJECTURES")
+    # UNVERIFIED tag in the conjectures header
+    assert "UNVERIFIED" in result.stdout
+
+
+def test_synthesis_report_empty(
+    isolated_leads_dir: Path,
+) -> None:
+    """`codex synthesis report` with no leads still prints both sections."""
+    result = runner.invoke(app, ["synthesis", "report"])
+
+    assert result.exit_code == 0
+    assert "GROUNDED LEADS" in result.stdout
+    assert "CONJECTURES" in result.stdout
+    assert "(none)" in result.stdout

tests/synthesis/test_conjecture.py

@@ -0,0 +1,113 @@
+"""Tests for stage-5 conjecture generation.
+
+HARD invariant: every conjecture MUST carry status='unverified', a
+non-empty suggested_validation, and non-empty provenance.
+"""
+
+from __future__ import annotations
+
+from pathlib import Path
+
+from codex.synthesis import _parse_conjecture_output, propose_conjectures
+from tests.synthesis.conftest import StubLLM
+
+_VALID_CONJECTURE = (
+    "Title: A discrete cosmetic-surgery analogue exists for Yamabe flows.\n"
+    "Body: The combinatorial Yamabe flow [Luo2004 #chunk 0] is a discrete "
+    "analogue of conformal change. One could hope the cosmetic surgery "
+    "conjecture has a discrete formulation in this setting.\n"
+    "Validation: Search for a counter-example among simplicial 3-manifolds "
+    "with at most 12 tetrahedra using a CSP solver."
+)
+
+_MISSING_VALIDATION = (
+    "Title: A naive idea.\n"
+    "Body: Some thoughts that follow [Luo2004 #chunk 0]. No falsification path "
+    "is described."
+)
+
+
+def test_parse_valid_conjecture_output() -> None:
+    """_parse_conjecture_output extracts title / body / validation."""
+    parsed = _parse_conjecture_output(_VALID_CONJECTURE)
+    assert parsed is not None
+    title, body, validation = parsed
+    assert title.startswith("A discrete cosmetic-surgery")
+    assert "Luo2004" in body
+    assert "counter-example" in validation
+
+
+def test_parse_conjecture_missing_validation_returns_none() -> None:
+    """Output without a Validation: line is rejected."""
+    assert _parse_conjecture_output(_MISSING_VALIDATION) is None
+
+
+def test_parse_conjecture_empty_input() -> None:
+    """Empty LLM output → None."""
+    assert _parse_conjecture_output("") is None
+
+
+def test_propose_conjectures_marks_status_unverified(
+    mock_retrieve: None,
+    mock_paper_titles: None,
+    mock_settings: Path,
+) -> None:
+    """Every emitted conjecture has status='unverified'."""
+    llm = StubLLM(_VALID_CONJECTURE)
+    leads = propose_conjectures(top_k=6, llm=llm)
+    assert len(leads) >= 1
+    for lead in leads:
+        assert lead.kind == "conjecture"
+        assert lead.status == "unverified"
+
+
+def test_propose_conjectures_requires_validation(
+    mock_retrieve: None,
+    mock_paper_titles: None,
+    mock_settings: Path,
+) -> None:
+    """Every emitted conjecture has a non-empty suggested_validation."""
+    llm = StubLLM(_VALID_CONJECTURE)
+    leads = propose_conjectures(top_k=6, llm=llm)
+    assert len(leads) >= 1
+    for lead in leads:
+        assert lead.suggested_validation.strip() != ""
+
+
+def test_propose_conjectures_requires_provenance(
+    mock_retrieve: None,
+    mock_paper_titles: None,
+    mock_settings: Path,
+) -> None:
+    """Every conjecture has at least one Provenance entry (seed chunks)."""
+    llm = StubLLM(_VALID_CONJECTURE)
+    leads = propose_conjectures(top_k=6, llm=llm)
+    assert len(leads) >= 1
+    for lead in leads:
+        assert len(lead.provenance) >= 1
+
+
+def test_propose_conjectures_drops_when_validation_missing(
+    mock_retrieve: None,
+    mock_paper_titles: None,
+    mock_settings: Path,
+) -> None:
+    """LLM output without a Validation: line is rejected (zero leads)."""
+    llm = StubLLM(_MISSING_VALIDATION)
+    leads = propose_conjectures(top_k=6, llm=llm)
+    assert leads == []
+
+
+def test_propose_conjectures_handles_llm_failure(
+    mock_retrieve: None,
+    mock_paper_titles: None,
+    mock_settings: Path,
+) -> None:
+    """LLM raising → returns [] (mirrors F-12 graceful degradation)."""
+
+    class FailingLLM:
+        def generate(self, prompt: str, model: str) -> str:
+            raise ConnectionError("ollama unreachable")
+
+    leads = propose_conjectures(top_k=6, llm=FailingLLM())
+    assert leads == []

tests/synthesis/test_gaps.py

@@ -0,0 +1,136 @@
+"""Tests for find_gaps — coverage map + code-vs-corpus signals."""
+
+from __future__ import annotations
+
+from pathlib import Path
+from typing import Any
+
+import pytest
+
+from codex.synthesis import find_gaps
+from tests.synthesis.conftest import StubLLM
+
+
+def test_find_gaps_code_cites_missing_bibkey(
+    monkeypatch: pytest.MonkeyPatch,
+    mock_paper_titles: None,
+    mock_settings: Path,
+    fixture_chunks: list[dict[str, object]],
+    tmp_path: Path,
+) -> None:
+    """A bibkey referenced in code but absent from corpus → direct gap lead."""
+    # Build a small C++ source tree with an @cite pointing at a missing bibkey
+    src_dir = tmp_path / "src"
+    src_dir.mkdir()
+    (src_dir / "main.cpp").write_text(
+        "// @cite UnknownPaper2099\nvoid foo() {}\n",
+        encoding="utf-8",
+    )
+
+    # All probes return the fixture chunks (so coverage map yields nothing)
+    monkeypatch.setattr(
+        "codex.synthesis._retrieve_chunks",
+        lambda queries, top_k: [dict(c) for c in fixture_chunks],
+    )
+
+    leads = find_gaps(lib_path=str(src_dir), llm=StubLLM(""))
+    bibkeys_in_gaps = {p.bibkey for lead in leads for p in lead.provenance}
+    # The missing bibkey shows up as a gap
+    assert any("UnknownPaper2099" in lead.title for lead in leads)
+    assert "UnknownPaper2099" in bibkeys_in_gaps
+
+
+def test_find_gaps_code_known_bibkey_not_reported(
+    monkeypatch: pytest.MonkeyPatch,
+    mock_paper_titles: None,
+    mock_settings: Path,
+    fixture_chunks: list[dict[str, object]],
+    tmp_path: Path,
+) -> None:
+    """A bibkey already in the corpus is NOT flagged by the code-vs-corpus path."""
+    src_dir = tmp_path / "src"
+    src_dir.mkdir()
+    (src_dir / "main.cpp").write_text(
+        "// @cite Springborn2008\nvoid foo() {}\n",
+        encoding="utf-8",
+    )
+    monkeypatch.setattr(
+        "codex.synthesis._retrieve_chunks",
+        lambda queries, top_k: [dict(c) for c in fixture_chunks],
+    )
+    leads = find_gaps(lib_path=str(src_dir), llm=StubLLM(""))
+    # Springborn2008 IS in the corpus → not a gap
+    assert not any("Springborn2008" in lead.title for lead in leads)
+
+
+def test_find_gaps_missing_lib_path_ok(
+    monkeypatch: pytest.MonkeyPatch,
+    mock_paper_titles: None,
+    mock_settings: Path,
+    fixture_chunks: list[dict[str, object]],
+) -> None:
+    """Without lib_path the code-vs-corpus path is skipped (no crash)."""
+    monkeypatch.setattr(
+        "codex.synthesis._retrieve_chunks",
+        lambda queries, top_k: [dict(c) for c in fixture_chunks],
+    )
+    leads = find_gaps(lib_path=None, llm=StubLLM(""))
+    # No crash; result list may be empty depending on coverage map.
+    assert isinstance(leads, list)
+
+
+def test_find_gaps_coverage_map_low_coverage_triggers_llm(
+    monkeypatch: pytest.MonkeyPatch,
+    mock_paper_titles: None,
+    mock_settings: Path,
+) -> None:
+    """A topic covered by only 1 bibkey (< 2) triggers the LLM gap prompt.
+
+    The grounded body must reference Springborn2008 [...] in a content-5-gram
+    that exists in the chunk, otherwise the lead is dropped.
+    """
+    sparse_chunks: list[dict[str, Any]] = [
+        {
+            "id": 10,
+            "paper_id": "springborn-2008",
+            "ord": 16,
+            "content": (
+                "For an ideal tetrahedron with dihedral angles the hyperbolic volume is "
+                "V = L(gamma1) + L(gamma2) + L(gamma3). "
+                "The volume function V0 is strictly concave on the angle domain."
+            ),
+            "bibkey": "Springborn2008",
+        },
+    ]
+    monkeypatch.setattr(
+        "codex.synthesis._retrieve_chunks",
+        lambda queries, top_k: [dict(c) for c in sparse_chunks],
+    )
+    grounded_body = (
+        "Only Springborn2008 covers the volume formula at depth, while comparison "
+        "papers are missing.\n"
+        "For an ideal tetrahedron with dihedral angles the hyperbolic volume is "
+        "V = L(gamma1) + L(gamma2) + L(gamma3). [Springborn2008 #chunk 16]\n"
+    )
+    leads = find_gaps(llm=StubLLM(grounded_body))
+    assert any(lead.kind == "gap" for lead in leads)
+
+
+def test_find_gaps_explicit_topics_override_default(
+    monkeypatch: pytest.MonkeyPatch,
+    mock_paper_titles: None,
+    mock_settings: Path,
+) -> None:
+    """Passing topics= explicitly overrides the default (paper titles)."""
+    captured_queries: list[list[str]] = []
+
+    def fake_retrieve(queries: list[str], top_k: int) -> list[dict[str, Any]]:
+        captured_queries.append(queries)
+        return []  # forces direct-gap-no-chunks path
+
+    monkeypatch.setattr("codex.synthesis._retrieve_chunks", fake_retrieve)
+    find_gaps(llm=StubLLM(""), topics=["custom topic A", "custom topic B"])
+    # Both custom topics should have been probed
+    flat = [q for qs in captured_queries for q in qs]
+    assert "custom topic A" in flat
+    assert "custom topic B" in flat

tests/synthesis/test_grounded.py

@@ -0,0 +1,175 @@
+"""Tests for grounded leads (connection / gap / improvement).
+
+The Grounding-Guard is re-used from :mod:`codex.wiki` (F-12). These tests
+verify that ungrounded claims are either dropped or annotated with ⚠,
+and that grounded statements survive intact.
+"""
+
+from __future__ import annotations
+
+from pathlib import Path
+
+from codex.synthesis import (
+    _finalise_grounded_lead,
+    _mark_ungrounded,
+    find_connections,
+    find_gaps,
+)
+from tests.synthesis.conftest import StubLLM
+
+_GROUNDED_CONNECTION = (
+    "Both papers build hyperbolic volumes from the Lobachevsky function.\n"
+    "For an ideal tetrahedron with dihedral angles the hyperbolic volume is "
+    "V = L(gamma1) + L(gamma2) + L(gamma3). [Springborn2008 #chunk 16]\n"
+    "A discrete conformal map is defined by logarithmic scale factors u_i at "
+    "each vertex such that the edge lengths satisfy a compatibility condition. "
+    "[BobenkoPinkallSpringborn2015 #chunk 3]\n"
+)
+
+_UNGROUNDED_CONNECTION = (
+    "Both papers prove the Riemann hypothesis via the Lobachevsky function. "
+    "[Springborn2008 #chunk 99]\n"
+)
+
+
+def test_finalise_grounded_lead_returns_none_without_claims(
+    fixture_chunks: list[dict[str, object]],
+) -> None:
+    """Body with no inline citations yields no grounded lead."""
+    lead = _finalise_grounded_lead(
+        seq=1,
+        kind="connection",
+        title="t",
+        body="A plain statement with no citation marker.",
+        chunks=fixture_chunks,
+        min_grounded_ratio=0.5,
+    )
+    assert lead is None
+
+
+def test_finalise_grounded_lead_drops_when_ratio_below_floor(
+    fixture_chunks: list[dict[str, object]],
+) -> None:
+    """All-ungrounded body → None (not silently promoted)."""
+    lead = _finalise_grounded_lead(
+        seq=1,
+        kind="connection",
+        title="t",
+        body=_UNGROUNDED_CONNECTION,
+        chunks=fixture_chunks,
+        min_grounded_ratio=0.5,
+    )
+    assert lead is None
+
+
+def test_finalise_grounded_lead_succeeds_when_grounded(
+    fixture_chunks: list[dict[str, object]],
+) -> None:
+    """Grounded body passes the floor and returns a populated Lead."""
+    lead = _finalise_grounded_lead(
+        seq=1,
+        kind="connection",
+        title="Both papers share a building block",
+        body=_GROUNDED_CONNECTION,
+        chunks=fixture_chunks,
+        min_grounded_ratio=0.5,
+    )
+    assert lead is not None
+    assert lead.kind == "connection"
+    assert lead.id == "L-0001"
+    assert lead.confidence >= 0.5
+    assert lead.status == "unverified"
+    assert lead.suggested_validation == ""
+    # All claims should be grounded
+    assert all(c.grounded for c in lead.claims)
+
+
+def test_mark_ungrounded_prefixes_warning() -> None:
+    """_mark_ungrounded prefixes ⚠ to the matching claim text once."""
+    from codex.wiki import Claim
+
+    body = "Some fact. [X2020 #c 1]\nOther fact. [Y2021 #c 2]\n"
+    claims = [
+        Claim(text="Some fact", bibkey="X2020", locator="c 1", grounded=False),
+        Claim(text="Other fact", bibkey="Y2021", locator="c 2", grounded=True),
+    ]
+    out = _mark_ungrounded(body, claims)
+    assert "⚠ Some fact" in out
+    # Grounded claim is not annotated
+    assert "⚠ Other fact" not in out
+
+
+def test_find_connections_emits_grounded_lead(
+    mock_retrieve: None,
+    mock_paper_titles: None,
+    mock_settings: Path,
+) -> None:
+    """End-to-end: with a grounded LLM response, a connection lead is produced."""
+    llm = StubLLM(_GROUNDED_CONNECTION)
+    leads = find_connections(top_k=6, llm=llm)
+    assert len(leads) >= 1
+    lead = leads[0]
+    assert lead.kind == "connection"
+    assert lead.provenance, "grounded lead must carry provenance"
+    # No ⚠ should appear because all claims grounded
+    assert "⚠" not in lead.body
+
+
+def test_find_connections_drops_ungrounded_response(
+    mock_retrieve: None,
+    mock_paper_titles: None,
+    mock_settings: Path,
+) -> None:
+    """Ungrounded LLM responses are dropped, not emitted with ⚠."""
+    llm = StubLLM(_UNGROUNDED_CONNECTION)
+    leads = find_connections(top_k=6, llm=llm)
+    assert leads == []
+
+
+def test_find_connections_handles_llm_failure(
+    mock_retrieve: None,
+    mock_paper_titles: None,
+    mock_settings: Path,
+) -> None:
+    """LLM raising → returns [] (mirrors F-12 graceful degradation)."""
+
+    class FailingLLM:
+        def generate(self, prompt: str, model: str) -> str:
+            raise ConnectionError("ollama unreachable")
+
+    leads = find_connections(top_k=6, llm=FailingLLM())
+    assert leads == []
+
+
+def test_find_gaps_topic_with_no_chunks(
+    monkeypatch,
+    mock_paper_titles: None,
+    mock_settings: Path,
+) -> None:
+    """When retrieval returns no chunks, a gap lead is emitted directly."""
+    monkeypatch.setattr("codex.synthesis._retrieve_chunks", lambda queries, top_k: [])
+    leads = find_gaps(llm=StubLLM(""))
+    assert len(leads) >= 1
+    assert all(lead.kind == "gap" for lead in leads)
+    # Direct gap leads carry a validation hint (re-ingest)
+    assert all(lead.suggested_validation for lead in leads)
+
+
+def test_find_gaps_well_covered_topic_skipped(
+    monkeypatch,
+    mock_paper_titles: None,
+    mock_settings: Path,
+    fixture_chunks: list[dict[str, object]],
+) -> None:
+    """Topics covered by enough bibkeys are NOT emitted as gaps.
+
+    Three distinct bibkeys in the fixture > synthesis_gap_min_coverage=2,
+    so every topic is well-covered and gets skipped.
+    """
+    monkeypatch.setattr(
+        "codex.synthesis._retrieve_chunks",
+        lambda queries, top_k: [dict(c) for c in fixture_chunks],
+    )
+    leads = find_gaps(llm=StubLLM(""))
+    # All probes well-covered → no gap leads
+    assert leads == []

tests/synthesis/test_model.py

@@ -0,0 +1,87 @@
+"""Tests for the Lead / Provenance datamodel (F-13)."""
+
+from __future__ import annotations
+
+from typing import get_args
+
+import pytest
+
+from codex.synthesis import Lead, LeadKind, LeadStatus, Provenance
+
+
+def test_provenance_requires_bibkey_and_locator() -> None:
+    """Provenance has two required positional fields."""
+    p = Provenance(bibkey="Smith2020", locator="chunk 7")
+    assert p.bibkey == "Smith2020"
+    assert p.locator == "chunk 7"
+
+
+def test_provenance_missing_field_raises() -> None:
+    """Provenance without locator must fail to construct (TypeError)."""
+    with pytest.raises(TypeError):
+        Provenance(bibkey="Smith2020")  # type: ignore[call-arg]
+
+
+def test_lead_required_fields() -> None:
+    """Lead requires id, kind, title, body, provenance, confidence."""
+    lead = Lead(
+        id="L-0001",
+        kind="connection",
+        title="A connection",
+        body="Some body text.",
+        provenance=[Provenance(bibkey="X2020", locator="chunk 1")],
+        confidence=0.8,
+    )
+    assert lead.id == "L-0001"
+    assert lead.kind == "connection"
+    assert lead.status == "unverified"  # default
+    assert lead.suggested_validation == ""  # default
+    assert lead.claims == []  # default factory
+
+
+def test_lead_kind_literals_exact() -> None:
+    """Lead kinds are exactly: connection, gap, improvement, conjecture."""
+    assert set(get_args(LeadKind)) == {"connection", "gap", "improvement", "conjecture"}
+
+
+def test_lead_status_literals_exact() -> None:
+    """Lead statuses are exactly: unverified, spiking, go, no-go."""
+    assert set(get_args(LeadStatus)) == {"unverified", "spiking", "go", "no-go"}
+
+
+def test_lead_provenance_can_be_multiple() -> None:
+    """A Lead may carry multiple provenance pointers."""
+    provs = [
+        Provenance(bibkey="A2020", locator="chunk 1"),
+        Provenance(bibkey="B2021", locator="chunk 7"),
+    ]
+    lead = Lead(
+        id="L-0002",
+        kind="gap",
+        title="t",
+        body="b",
+        provenance=provs,
+        confidence=0.5,
+    )
+    assert len(lead.provenance) == 2
+
+
+def test_lead_missing_provenance_field_raises() -> None:
+    """Constructing Lead without provenance is a TypeError."""
+    with pytest.raises(TypeError):
+        Lead(  # type: ignore[call-arg]
+            id="L-0003",
+            kind="connection",
+            title="x",
+            body="y",
+            confidence=0.5,
+        )
+
+
+def test_lead_id_format_helper() -> None:
+    """The internal _make_lead_id helper produces zero-padded L-XXXX strings."""
+    from codex.synthesis import _make_lead_id
+
+    assert _make_lead_id(1) == "L-0001"
+    assert _make_lead_id(42) == "L-0042"
+    assert _make_lead_id(9999) == "L-9999"

tests/synthesis/test_quarantine.py

@@ -0,0 +1,132 @@
+"""INVARIANT tests — conjectures live in leads/conjectures/, never in wiki/.
+
+This is the hard F-13 invariant. Violations would corrupt the wiki layer
+and must be unrepresentable in the API.
+"""
+
+from __future__ import annotations
+
+from pathlib import Path
+
+import pytest
+
+from codex.synthesis import Lead, Provenance, write_leads
+
+
+def _grounded_lead(lead_id: str = "L-0001") -> Lead:
+    return Lead(
+        id=lead_id,
+        kind="connection",
+        title="Connection title",
+        body="Some grounded body. [X2020 #chunk 1]",
+        provenance=[Provenance(bibkey="X2020", locator="chunk 1")],
+        confidence=0.8,
+        status="unverified",
+    )
+
+
+def _conjecture(lead_id: str = "L-0002") -> Lead:
+    return Lead(
+        id=lead_id,
+        kind="conjecture",
+        title="A bold conjecture",
+        body="Hypothetical statement seeded by [X2020 #chunk 1].",
+        provenance=[Provenance(bibkey="X2020", locator="chunk 1")],
+        confidence=0.0,
+        status="unverified",
+        suggested_validation="Search for a counter-example with N<=8.",
+    )
+
+
+def test_conjecture_lands_in_conjectures_dir(tmp_path: Path) -> None:
+    """A conjecture lead writes to leads/conjectures/<id>.md."""
+    write_leads([_conjecture("L-0002")], str(tmp_path))
+    assert (tmp_path / "conjectures" / "L-0002.md").exists()
+    # And NOT in grounded/
+    assert not (tmp_path / "grounded" / "L-0002.md").exists()
+
+
+def test_conjecture_never_in_grounded_dir(tmp_path: Path) -> None:
+    """No conjecture file may appear under leads/grounded/."""
+    write_leads([_grounded_lead("L-0001"), _conjecture("L-0002")], str(tmp_path))
+    grounded_files = list((tmp_path / "grounded").glob("*.md"))
+    conj_files = list((tmp_path / "conjectures").glob("*.md"))
+
+    assert len(grounded_files) == 1
+    assert grounded_files[0].name == "L-0001.md"
+    assert len(conj_files) == 1
+    assert conj_files[0].name == "L-0002.md"
+
+
+def test_conjecture_never_in_wiki_dir(tmp_path: Path) -> None:
+    """The wiki/ directory is never touched by write_leads."""
+    wiki_dir = tmp_path / "wiki"
+    wiki_dir.mkdir()
+    write_leads([_conjecture("L-0002")], str(tmp_path / "leads"))
+    # No file landed in wiki/
+    assert list(wiki_dir.glob("*.md")) == []
+
+
+def test_conjecture_markdown_contains_unverified_marker(tmp_path: Path) -> None:
+    """The on-disk conjecture file announces UNVERIFIED status."""
+    write_leads([_conjecture("L-0002")], str(tmp_path))
+    md = (tmp_path / "conjectures" / "L-0002.md").read_text(encoding="utf-8")
+    assert "UNVERIFIED" in md
+    assert "Suggested validation" in md
+    assert "Search for a counter-example" in md
+
+
+def test_invariant_violation_raises(tmp_path: Path) -> None:
+    """Constructing a Lead with kind='conjecture' but routed by code into
+    grounded/ would be a programmer error — guarded by the kind→dir check.
+
+    We simulate it by monkey-patching the kind set, which is the only way
+    a writer could attempt this. The expectation is that no path exists in
+    the public API to write a conjecture into grounded/.
+    """
+    # Hard guarantee: the only sanctioned writer routes by lead.kind.
+    # Verify the dataclass kind field cannot trivially be spoofed: it is
+    # a Literal-typed string so any value other than the four kinds is a
+    # type error at static-checking time. At runtime, write_leads still
+    # rejects unknown kinds.
+    bogus = Lead(
+        id="L-0003",
+        kind="conjecture",  # legitimate kind …
+        title="x",
+        body="y",
+        provenance=[Provenance(bibkey="X2020", locator="chunk 1")],
+        confidence=0.0,
+        suggested_validation="run a spike",
+    )
+    write_leads([bogus], str(tmp_path))
+    # Conjecture must land in conjectures/, not grounded/
+    assert (tmp_path / "conjectures" / "L-0003.md").exists()
+    assert not (tmp_path / "grounded" / "L-0003.md").exists()
+
+
+def test_unknown_kind_rejected(tmp_path: Path) -> None:
+    """A Lead with an unrecognised kind raises at write time."""
+    lead = Lead(
+        id="L-0009",
+        kind="bogus-kind",  # type: ignore[arg-type]
+        title="t",
+        body="b",
+        provenance=[Provenance(bibkey="X2020", locator="chunk 1")],
+        confidence=0.5,
+    )
+    with pytest.raises(RuntimeError):
+        write_leads([lead], str(tmp_path))
+
+
+def test_index_separates_grounded_and_conjectures(tmp_path: Path) -> None:
+    """INDEX.md visibly separates grounded leads from conjectures."""
+    write_leads([_grounded_lead("L-0001"), _conjecture("L-0002")], str(tmp_path))
+    index = (tmp_path / "INDEX.md").read_text(encoding="utf-8")
+    # Two distinct, visibly separated sections
+    assert "## Grounded leads" in index
+    assert "## Conjectures" in index
+    # Ordering: grounded section appears before conjectures
+    assert index.index("Grounded leads") < index.index("Conjectures")
+    # Both ids are listed
+    assert "L-0001" in index
+    assert "L-0002" in index