# Write Paper

> Turn a project's verified fact graph into a publishable LaTeX paper in a configurable house style — a standalone amsart .tex with a real bibliography, compiled to PDF. Use when a project's target theorem is established and the operator wants the paper, or asks to write/revise/audit references for the paper for a project. NOT human-summary (a reader-facing progress report with no bibliography); this is the publication artifact, with verified citations, headed for arXiv / a LaTeX git repo.

- Skill: `frenzymath/write-paper` (Agent Skill, multi-file: 8 files)
- Install (CLI): `npx skillmds@latest add frenzymath/write-paper`
- Raw SKILL.md: https://api.skillmd.com/api/skills/frenzymath/write-paper/raw
- Safety review: pending
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: Security
- Author: frenzymath (https://skillmd.com/u/frenzymath)
- Updated: 2026-09-17
- Page: https://skillmd.com/skills/frenzymath/write-paper

---


# write-paper — fact graph → publishable paper

You are the main agent. This skill turns a project's **verified fact graph** into
a **publishable** LaTeX paper in a configurable house style: a standalone
`\documentclass{amsart}` `.tex` with a real manual bibliography, compiled to a
clean PDF, ready for arXiv / an Overleaf (or other) LaTeX git repo. It is the
publication sibling of `human-summary` (a reader-facing progress report with no
bibliography).

The heavy LaTeX work is delegated to a **local codex at extra-high (`xhigh`)
reasoning** — the same codex machinery the workers and the verify service already
use. The writer,
auditor, verifier, and reviser roles are wrapped behind the `write-paper` MCP
service (tools `paper_write` / `reference_audit` / `reference_verify` / `paper_revise`):
you call them with structured args, the tool assembles each role's prompt
internally (so the style guide and fact-graph bytes never enter your context) and
drives the codex with each role isolated by construction. The reference chain is
`auditor (offline, flags) → verifier (online, checks) → reviser (edits)`. You
orchestrate the stages, call these tools, gate on compilation, and surface the one
or two real decisions to the operator.

## When to use

- A project's target theorem is established in the fact graph and the operator
  wants the paper.
- The operator asks to **write**, **revise**, **audit references for**, or
  **push** the paper for a project.

Do not use it for the progress report (`human-summary`) or the internal strategy
synthesis (`elaboration`).

## Source of content: the fact graph (never your memory)

Build the mathematics from the project's **verified facts**
(`<project>/fact_graph/facts/*.md`) and the verbatim goal in
`<project>/PROBLEM.md` — exactly as `human-summary` does, but for publication:

- Each fact's `## statement` is fully-quantified and self-contained → render into
  the paper's theorems/propositions (clean LaTeX, do not paraphrase loosely). Its
  `## proof` is the argument; `## intuition` feeds a proof sketch where useful.
- Load-bearing facts first: high dependency depth (headline results) and high
  in-degree (key lemmas). `predecessors` give you the internal `Theorem~\ref{}`
  cross-reference structure **with zero invention**.
- **Citations come structured, from the source.** Each fact's `external_refs`
  (key / authors / title / arxiv / year / cited_for) records the published
  results its proof cited. `driver/seed_ledger.py` aggregates them across the
  project into the starting `REFERENCE_LEDGER.md`. Do not re-mine citations from
  prose — that is the #1 failure mode (hallucinated references).
- **Preserve all mathematics. Invent nothing** — no assumptions, lemmas,
  citations, theorem labels, or definitions that are not in the fact graph. If a
  step is unclear, flag `[GAP: ...]`, do not smooth it over.

## Paper workspace: `<project>/paper/` (default) — and MULTIPLE papers per project

Per-project, alongside `fact_graph/` and `global_memory/`:

```
<project>/paper/                 # the DEFAULT paper (legacy paths — unchanged)
  PROJECT_BRIEF.md      # per-paper framing (interview the operator — see below)
  REFERENCE_LEDGER.md   # seeded from external_refs, verified by the auditor
  REVISION_LOG.md       # append-only round history
  main.tex / main.pdf   # the paper
<project>/TARGET.md              # the DEFAULT paper's finalized target (danus finalize)
```

Seed the workspace from `templates/` (copy `*.template` → the real names) if it
does not exist yet.

**One project can hold MULTIPLE papers** (e.g. a main theorem paper + a companion,
or several theorems each written up separately). Every `paper_*` tool and
`danus finalize` takes an optional **`paper_id`**:

- `paper_id` **omitted / `"main"`** → the **DEFAULT** paper on the **legacy** paths
  above (`<project>/paper/` + `<project>/TARGET.md`). Existing single-paper
  projects are byte-for-byte unchanged.
- any other `paper_id` (e.g. `thmB`) → an **isolated** workspace
  `<project>/papers/<paper_id>/` with its own `PROJECT_BRIEF.md` /
  `REFERENCE_LEDGER.md` / `REVISION_LOG.md` / `main.tex` / `TARGET.md`. So N papers
  never collide — each has its own files.

There is **one fact graph per project** (`<project>/fact_graph/`); papers never
fork or re-filter it. A paper's facts are simply the transitive-predecessor
**closure of its own headline set** — the SAME closure primitive the single-paper
pipeline already uses, merely rooted at that paper's recorded target. The three
shapes are one model — **a list of `{paper_id, headline_fact_ids}`**:

- **1 paper / 1 theorem** — the default: one entry, `paper_id="main"`.
- **N papers / 1 theorem each** — N entries, each a distinct `paper_id` and a
  single-fact headline; written in **separate workspaces** (no overwrite).
- **N papers / one multi-theorem paper** — an entry whose `headline_fact_ids` is a
  LIST of several targets; its fact set is the **union closure** of that list.

`paper_id` must be a single safe path segment (same validation as a project name);
it cannot escape the project dir.

## Style source

Two generic, self-contained layers under `style/`, neither naming an author or a
field:

- `style/STYLE_GUIDE.md` — the compact baseline house style (binding for *voice*:
  macros, theorem/proof shape, citations, cross-references, sentence-level rules).
- `style/PAPER_STRUCTURE.md` — the per-section content plan (binding for
  *structure*: what each part of the paper contains, by length tier — abstract,
  introduction, preliminaries, body, proofs, acknowledgements, bibliography).
  Field-neutral; uses placeholders, not any specific area's conventions.

Both are plain Markdown the operator may edit to encode their own preferences.

**Imitating your own past papers is strictly optional** — an add-on for authors
who already have published papers, not a dependency:

- `style/anchors/` — optional exemplar papers the operator drops in (one folder
  per paper, with its `.tex`) for the `STYLE_DISTILLER` to learn from (feeding the
  unified `STYLE_GUIDE.md`, which is the writer's single source of **voice**) and,
  optionally, for ONE of them — named deterministically by the brief's
  `structural_exemplar` field — to be imitated for **structure**. **Empty by
  default. The skill produces a complete, compilable paper from the two generic
  guides alone** — anchors only make the output sound more like the operator's own
  writing. The writer never "picks the closest" anchor: voice is the distilled
  guide (all anchors), structure is the single brief-named exemplar (or none).

The role prompts under `roles/` are generic and read directly; there is no
machine- or author-specific overlay.

## Per-call run logs (diagnostics)

Every `paper_*` tool returns a `log_path` and writes a full on-disk diagnostic
record there — the complete assembled prompt, codex's full stdout **and** full
stderr (not just the tail), the honest result, the tool's post-processing
decisions, and the returned envelope. On a non-`ok` or surprising result, **read
`log_path`** for the full assembled prompt + codex stdout/stderr + tool decisions
before retrying or reporting — it lets you localize the failure (prompt vs codex
vs tool logic) instead of retrying blind. The small envelope (status / returncode
/ `stderr_tail` / flags / paths) is unchanged; `log_path` is additive. Run logs
live under the paper's own `.runs/` (default `<project>/paper/.runs/`; a non-default
paper → `<project>/papers/<paper_id>/.runs/`), gitignored; set
`DANUS_WRITE_PAPER_RUN_LOG=0` to opt out (then `log_path` is `None`).

## Editorial quality bar — write WELL, not LONG (your judgment, applied at every stage)

You are the paper's editor. There is **no hard length cap** — some results genuinely
need many pages, and a fixed ceiling would only force you to mangle them. A good paper
is short because it is well-SHAPED, not because it was cut to a number. Shaping it is
YOUR job, and it starts before a single `paper_write` call:

- **A paper is not a stack of facts — and YOU are the one who prevents that.** The two
  controls that decide the paper's shape are both yours: which facts you SELECT (the
  support layer) and the editorial `instructions` you write for each `paper_write`. So
  first UNDERSTAND the proof strategy as a whole; then select the load-bearing results
  that carry the argument and, in your instructions, direct that the **support layer is
  developed in proper detail** while **every other fact contributes only the
  mathematical content the argument needs** — stated, not re-narrated as a full proof.
  A hundred-fact closure rendered flat, one lemma after another, is exactly the failure
  this prevents: the writer renders what you hand it and how you tell it to, so the
  shape is set by your selection and instructions. Calibrate "how much detail" by the
  bar the whole-paper verifier uses (§5.5): a step a mathematics undergraduate could
  fill unaided may be abbreviated; anything they could not must be developed or cited.
  The mechanics of selecting and instructing are the BINDING RULE at stage 2; the
  levers you apply are below.
- **Length is a SYMPTOM, never a target.** If a draft feels too long, the cause is
  almost always a violation of the shaping principle above — re-proving something
  citable, or re-narrating a routine computation — not "too many pages" as such. Fix
  the cause, not the page count. A genuinely deep result that is long AFTER honest
  citation and the right level of detail is SUPPOSED to be long; do not mangle it to
  hit a number.
  When one paper's worth of contribution truly spans a book, the human practice is a
  SERIES of papers (the `paper_id` split, lever #4) — an operator-initiated fork, not
  a cap you enforce on your own.
- **Density signals (health checks, not limits).** A strong paper usually carries
  ~10–30 labeled results, one theorem-sized idea per section, and lemmas that exist
  because the narrative needs them. Red flags that the shaping broke down:
  100+ labeled results; helper-lemma sprawl around a single proof; repeated
  setup/notation blocks; proofs that read as computation logs (transcription instead
  of exposition). These signal "go re-apply the shaping principle above", not "cut to N pages".
- **The levers, in order — all serve the shaping principle above, none a page count.** (1)
  cite, don't re-prove (standard machinery → precise citations); (2) render at the
  right granularity — full detail on the pivots, method+outcome on routine steps,
  never one-lemma-per-fact; (3) curate which results the paper PRESENTS (a paper is
  not every fact you proved; the support-layer BINDING RULE at stage 2); (4) **SPLIT
  into companion papers** when the contribution genuinely spans more than one paper
  (the `paper_id` mechanism — a deep development becomes its own "Part II" / technical
  companion the main paper cites).
- **The reviser cannot globally compress — so get the granularity right the first
  time.** Measured on a real paper: a dedicated compression-only round asked for −27K
  and delivered −0.5K; every "pay by compressing while adding" round under-paid while
  the paper inflated. A patch-style reviser executes located edits; it cannot execute
  global restructuring. So NEVER issue "compress the paper by N pages" — it silently
  under-delivers. What CAN work: YOU find specific mechanical redundancy yourself (a
  lemma proved twice, a definition declared twice, a duplicated setup block) and order
  its removal as POINT EDITS. The durable fix, though, is upstream: honest citation +
  right granularity when the section is first written.

## The pipeline (you drive these stages in order)

### 0. PROJECT_BRIEF — interview the operator (do not invent)

If `<project>/paper/PROJECT_BRIEF.md` is absent, **conduct a short interactive
interview** with the operator to fill it: title, audience/venue, human authors
(and affiliations), which facts are the headline results, per-paper style
overrides, deadline. Write their answers into the brief. Never fabricate these —
they are the operator's call. (If the operator wants to skip and accept defaults,
record that; the writer then emits author placeholders.)

**Pre-fill `headline_fact_ids` from the finalized target.** When you seed the
brief, if the paper's `TARGET.md` exists (the default paper's `<project>/TARGET.md`,
or `<project>/papers/<paper_id>/TARGET.md` for a non-default paper — written by
`danus finalize [--paper <paper_id>]` when the operator approved the result as the
answer), copy its fact id(s) into the brief's `headline_fact_ids` field so the
finalized target is already the paper's headline. If `TARGET.md` is absent, leave
the field blank and **ask the operator** — and know that `paper_write` will
**refuse with `status="needs_target"`** until either the field is set or the
operator runs `danus finalize <project> [--paper <paper_id>] <fact_id>`. The skill
never guesses the target from the graph shape.

Two **structured fields** the brief carries (machine-read; keep the `field: value`
shape on its own line):

- **`headline_fact_ids`** — the fact ids that ARE this paper's target results
  (the theorems it foregrounds). This is the backbone of the default: the writer
  is given the transitive-predecessor **closure** of these targets — NOT every
  proven fact — and the reference ledger is seeded from the **same** closure, so
  the writer's facts and the bibliography agree and the auditor never sees phantom
  rows for side lemmas the paper never cites. Pre-fill it from `<project>/TARGET.md`
  if present, else ask the operator explicitly. If it is left blank AND no
  `TARGET.md` is recorded, the target is **UNSET** and `paper_write` refuses
  (`needs_target`) rather than guessing — run `danus finalize <project> <fact_id>`
  to record the target first.
- **`structural_exemplar`** — optional: the name of ONE folder under
  `style/anchors/` whose STRUCTURE this paper should imitate. Voice always comes
  from the unified `STYLE_GUIDE.md`; this names only the single structural
  exemplar. Blank = none. If the operator already has anchors, ask which (if any)
  to imitate structurally. **If `style/anchors/` is empty, still offer once** —
  "you can drop a few of your own papers into `style/anchors/` now to match your
  writing voice; want to? (a complete paper is produced either way)" — so the
  capability isn't hidden behind an empty folder. If they add some, run Stage 1a
  to distil them before writing.

### 1. Seed the reference ledger

```bash
python3 .../write-paper/driver/seed_ledger.py <project_dir> --headline <headline_fact_ids> --out <project>/paper/REFERENCE_LEDGER.md
# multiple papers: add --paper <paper_id> to scope the closure to that paper's
# recorded target and (with no --out) write the ledger into its own workspace:
python3 .../write-paper/driver/seed_ledger.py <project_dir> --paper <paper_id>
```

This aggregates the `external_refs` of the **target-closure facts** into
`unverified` rows. Pass the **same** `headline_fact_ids` you recorded in the brief
(stage 0) as `--headline` so the ledger's closure equals the writer's closure
(one closure, shared): the ledger then lists only references the paper's facts
actually cite — no phantom rows for proven-but-unused side lemmas. Omit
`--headline` to let the script resolve it identically (brief field → else the
finalized `<project>/TARGET.md`). If no target is recorded at all, the seed
**refuses** (matching the writer). (Verification is stage 4; `--all-facts`
restores the legacy all-facts seeding if ever needed.)

### 1a. Style preflight — distil the anchors if they changed (presence-triggered, once, operator-gated)

Before the writer stage, check whether the operator's own papers under
`style/anchors/` need to be distilled into the unified `STYLE_GUIDE.md`. This is
the only automatic trigger for the `STYLE_DISTILLER` — without it, papers an
operator drops into `anchors/` are silently ignored.

Trigger rule (all offline; the distiller only PROPOSES, never auto-applies):

- If `style/anchors/` is **empty** → skip (the two generic guides produce a
  complete paper; nothing to distil).
- If `anchors/` is **non-empty** AND **stale** — its newest content is newer than
  the `style/.distilled_at` marker, or the marker is absent — then run the
  `STYLE_DISTILLER` (`roles/STYLE_DISTILLER_PROMPT.md`) to **propose**
  `STYLE_GUIDE.md` updates. Present the proposals to the operator; on **accept**,
  apply the accepted edits to `STYLE_GUIDE.md` and **touch** `style/.distilled_at`
  (record the distill time). On reject, still touch `.distilled_at` only if the
  operator says the current guide stands (so a rejected-but-reviewed anchor set is
  not re-proposed every run) — otherwise leave the marker so it re-triggers.
- If `anchors/` is **unchanged** since the last distill (nothing newer than
  `.distilled_at`) → skip.

A tiny helper compares mtimes so the check stays clean:

```bash
bash .../write-paper/driver/anchors_stale.sh <skill_dir>   # rc 0 = stale (distil), rc 1 = fresh/empty (skip)
```

**Why operator-gated, never auto-applied:** the distiller edits the guide that
governs *every* future paper; a bad distill would silently corrupt them all. The
distiller proposes; the operator accepts; only then does `STYLE_GUIDE.md` change.
This step is still optional in spirit — with no anchors it is a no-op — but when
anchors exist and changed, it runs so they are not ignored.

### 2. Write (PAPER_WRITER) — produce `main.tex`

**Call the `paper_write` tool** (the `write-paper` MCP service). You do **not**
build the prompt by hand and you do **not** read the style guide, the structure
plan, or the fact graph into your own context — the tool assembles all of that
internally and drives the codex, so the large bytes never enter your window.

**First, curate — MANDATORY, and it is YOUR job, at EVERY level. `paper_subgraph`.**

> **BINDING RULE — never hand a writer the whole closure.** Every single `paper_write`
> call must be given a hand-picked **support layer** via `fact_ids`: the few key
> load-bearing results that call should PRESENT. It is **forbidden to pass the full
> closure** (or to omit `fact_ids` so the tool embeds it) **unless the closure is
> single-digit** (< 10 facts). Dumping all facts on one writer call is the root cause
> of overflow, the chunked fallback, and flat/bloated output — do not do it. If you
> think "this piece is small enough to just send its facts," check the count first;
> if it is ≥ 10, curate.
>
> **This applies RECURSIVELY / fractally.** A hard sub-result written as its own
> lemma-chapter is STILL a `paper_write` call, so it ALSO gets a curated support layer
> — not that sub-result's whole closure. If that chapter's support layer leans on a
> deeper load-bearing result, that deeper result becomes its OWN curated `paper_write`
> call (its own chapter/sub-paper), which YOU then compose in (a written body slotted
> as a section — you do the stitching; see below). The paper is a TREE of curated
> single-pass writes you design and assemble, never one writer call swallowing a big
> fact set. "Pick the support layer" is the intelligence that stays with you at every
> node of that tree; the writer only renders what you hand it.

The target's full transitive closure can be hundreds of facts; embedding every
proof would overflow a single writer pass. So do what a human author does: read a
**compact skeleton** and SELECT the load-bearing subset to write up. Call

```
paper_subgraph(project=<project>, headline=[<target fact ids>|omit], paper_id=<paper_id|omit>)
```

It returns, deterministically (no codex, no writes), `{status, headline,
headline_source, count, facts}` where each `facts[i]` is `{id, statement (one-line),
predecessors, dependents (in-closure in-degree — higher = more load-bearing),
glossary_introduces}` in topological order. Read it, pick the results the paper
should PRESENT (the headline theorems + the lemmas their proofs actually turn on —
NOT every granular intermediate step; those get cited), and write short editorial
`instructions` (how to section, what to foreground — and encode the editorial shaping
principle: support layer in detail, everything else stated minimally; see the
editorial bar). An unset target → the same
`needs_target` refusal as `paper_write` (run `danus finalize` first).

**Then write** — pass your selection + direction to `paper_write`:

```
paper_write(project=<project>, headline=[<target fact ids>], paper_id=<paper_id|omit for default>,
            fact_ids=[<the load-bearing subset you selected>], instructions="<sectioning / emphasis>")
```

- `fact_ids` — the subset from `paper_subgraph` to PRESENT in full. The tool embeds
  only these (statement + proof) plus their **direct-predecessor statements** as
  `\ref`/`\cite` context (the granular lemmas are cited, not reproduced) — so a
  curated paper fits ONE pass. **Omit `fact_ids` ONLY when the closure is
  single-digit** (< 10 facts); on any larger closure omitting it (⇒ whole-closure
  embedding ⇒ chunked fallback ⇒ bloat) is the mistake the BINDING RULE above forbids.
  Unknown ids → `status="bad_fact_ids"` (no paper); ids outside the closure are kept
  with a `fact_id_warnings` note.
- `instructions` — your editorial direction, embedded verbatim as an authoritative
  `MAIN_AGENT_INSTRUCTIONS` block (wins over the writer's default structure, never
  over the PRIME DIRECTIVE / style voice / the mathematics).

- `project` — the project name (resolved under `DANUS_AGENTS_ROOT`).
- `paper_id` — WHICH paper in the project (multiple papers per project; one fact
  graph). Omit / `"main"` → the default paper on the legacy `<project>/paper/`
  paths; any other id → the isolated `<project>/papers/<paper_id>/` workspace. The
  brief / ledger / TARGET.md the tool reads are rooted at that paper's workspace.
- `headline` — the paper's **target** fact ids (the headline results). This is
  the DEFAULT scoping: the tool embeds only the target's transitive-predecessor
  **closure**, in topological order, with **zero invention** — NOT every proven
  fact. Omit `headline` to let the tool resolve it the same way the ledger did:
  the brief's `headline_fact_ids` field, else the finalized `<project>/TARGET.md`.
  The tool returns `headline` (the resolved target ids used) and `headline_source`
  (`arg` / `brief` / `target`). If the target is **UNSET** (no arg, no brief field,
  no `TARGET.md`) the tool returns `status="needs_target"` with a `candidates` list
  (the terminal facts) and writes **no** `main.tex` — **run `danus finalize
  <project> <fact_id>`** (or fill the brief) and call it again. It never guesses.
- The **structural exemplar** is read from the brief's `structural_exemplar`
  field (one anchor to imitate for STRUCTURE); there is no per-call anchor arg.
  Voice always comes from the unified `STYLE_GUIDE.md`.
- **`paper_write` does NOT stop the worker swarm by default** — entering
  write-paper does not always mean the whole problem is proven; a *partial* result
  can be written up while the swarm keeps exploring the rest. **If you already
  stopped the swarm because the whole problem is proved** (the completion rule in
  `AGENTS.md` / the main-agent contract), this fork is moot — the swarm is already
  down; just write the paper. **Otherwise (a partial result, exploration ongoing),
  you decide:** at the start of write-paper (Stage 0) surface the fork to the operator
  — *"Start the paper — stop the swarm's exploration, or keep it running? (A partial
  result can be written up while the swarm keeps proving the rest.)"* On **stop** →
  call `paper_write(stop_workers=True)` (or `danus stop <project>`); on **keep** →
  the default (no stop). When you do request a stop it is graceful (never drops an
  in-flight verified round), idempotent, and failure-isolated; the tool reports it
  in a `swarm_stop` field (`result` / `noop` / `error` / `skipped`).

Internally the tool embeds, in full: the role contract (`roles/AGENTS.md` — the
PRIME DIRECTIVE) and `roles/PAPER_WRITER_PROMPT.md`; the **unified**
`style/STYLE_GUIDE.md` (voice, distilled across all anchors) and
`style/PAPER_STRUCTURE.md`; `boilerplate/acknowledgement.md`; `PROJECT_BRIEF.md`
and the seeded `REFERENCE_LEDGER.md`; the fact-graph math of the **target
closure** (each fact's `## statement` / `## proof` / `## intuition` + the
predecessor DAG, verbatim); and, iff the brief's `structural_exemplar` names an
existing anchor, that ONE anchor as a structural exemplar. Those codex-facing
fixed files (`roles/`, `style/`, `boilerplate/`) live under
`agents/skills/write-paper/`, **not here** — the MCP reads and embeds them; you never do. It
writes codex's stdout to `<project>/paper/main.tex` (a full `\documentclass{amsart}`
… `\end{document}`, real `\ref`/`\cite`, manual `\begin{thebibliography}{99}`).

The tool returns a small dict — `{tex_path, status, returncode, headline,
headline_source, selected_facts, fact_id_warnings, gaps, stderr_tail, log_path}` (or
`{status:"needs_target", message, candidates, log_path}` when the target is unset,
or `{status:"bad_fact_ids", unknown_fact_ids}` when a selected id is not in the
graph). **Honesty:** it reports `status="ok"` only
on a zero exit with non-empty output; a nonzero codex exit, an empty artifact, or
a timeout is `status != "ok"` and **nothing is written** — do not treat a non-`ok`
result as a produced paper, and a `needs_target` result means you must record the
target first (`danus finalize`). `headline`/`headline_source` report which target
ids were used and where they came from. The `gaps` list is the `[GAP: ...]`
markers the writer left; act on them. The tool does **not** compile — the compile
gate is stage 3.

**Auto-chunking — the extreme fallback.** Curation (`fact_ids`) is the primary
answer to a large closure: a well-chosen subset writes in one pass. But if even the
prompt you assembled is still over budget (`DANUS_PAPER_WRITE_CHUNK_CHARS`, default
~800000 chars ≈ ~200K tokens) — a huge selection, or `fact_ids` omitted on a giant
closure — `paper_write` falls back automatically to **chunked** generation: a
**planning pass** (one codex call on the STATEMENTS ONLY of the set being written →
the fixed preamble + front matter + a section plan assigning every fact + the
bibliography), then **per-section fill** (one codex call per section, each given THIS
section's full proofs + the fixed preamble/labels + every other result's statement
for `\ref`), then a deterministic **stitch** into one `main.tex`. When you passed
`fact_ids`/`instructions`, the fallback chunks exactly that curated set and the
planner honors your instructions. Each call is still a NON-AGENTIC isolated codex
(empty cwd, everything embedded, no tool calls) — chunking is decided in Python and
sliced by section, not an agentic retrieval writer. The result carries `chunked:
true` and `sections: <n>`. Under budget → the single-pass path runs unchanged.
**Honesty is preserved:** if the planner or any section writer returns non-ok, or a
deterministic coverage check finds an assigned fact unassigned/duplicated,
generation fails honestly (`status="chunk_failed"`, `failed_phase`) and **no
`main.tex` is written** — a partial paper is never emitted. Cross-section coherence
(a `\ref` that does not resolve, a seam claim) is caught downstream by the compile
gate (stage 3) and `paper_verify_math`. If chunking keeps failing, prefer selecting
a smaller `fact_ids` subset, or split the work into multiple papers via `paper_id`.

**Manual fallback — you assemble and drive codex yourself (last resort).** If
`paper_write` returns `status="chunk_failed"` (or any non-`ok` you cannot resolve by
curating a smaller `fact_ids` subset or splitting into multiple papers), fall back to
the flexible manual path: **you** write the paper by driving codex directly. This is
the one place you assemble the codex prompt by hand — use your judgment (curate the
facts, restructure the sections, adjust emphasis) to get past whatever the
deterministic path choked on.

1. **Get the material.** Read the failed run's **`log_path`** — it holds the full
   assembled prompt (role contract + style guide + structure + brief + ledger + the
   fact bodies). Reuse it as-is, or re-assemble your own from the pieces you control:
   your curated `fact_ids` (each fact's `## statement`/`## proof` from
   `<project>/fact_graph/facts/*.md`, or via `paper_subgraph`), `style/STYLE_GUIDE.md`
   + `style/PAPER_STRUCTURE.md`, the brief, and the seeded `REFERENCE_LEDGER.md`.
2. **Drive codex yourself.** The prompt is large — write it to a temp file and put it
   on **stdin** (never argv), and run the repo's codex wrapper at `xhigh`, read-only
   (the same flags the tool uses — see `danus.authoring.driver`):
   ```bash
   bin/codex exec --model "$DANUS_MAIN_MODEL" --config model_reasoning_effort=xhigh \
     --sandbox read-only --skip-git-repo-check - < /tmp/writer_prompt.md \
     > <project>/paper/main.tex          # or <project>/papers/<paper_id>/main.tex
   ```
   In this fallback the bytes DO enter your context (you read/assemble the prompt) —
   that is the trade for flexibility, and it is acceptable because it is the rare last
   resort, not the hot path.
3. **Then re-enter the gates — verification is NOT bypassed.** Your hand-written
   `main.tex` goes through the SAME safety net as any tool-written one: the compile
   gate (stage 3), the reference audit/verify (stages 4/4.5), and **`paper_verify_math`**
   (stage 5.5). The manual fallback loosens only *how the paper is written*, never
   *how it is verified* — a hand-written paper with a broken proof is still caught and
   still blocks deliver.

**Honesty:** exactly as on the tool path, a paper is "produced" only after it
compiles AND passes `paper_verify_math`. Never present a hand-written `main.tex` as
done before the gates pass.

### 2b. DEEP theorems — the CHAPTER TREE (write chapters with the writer; never dump facts on the reviser)

When the target's load-bearing content is too deep for one curated single-pass write
(hundreds of novel facts — e.g. a paper whose verifier gaps keep exposing deeper
sub-lemmas), do NOT try to close it by feeding fact piles to `paper_revise` — an
accretion of 100+ reviser-inserted lemmas produces a flat, disorganized blob and
converges terribly (measured). And do NOT fall back to the auto-chunker to "handle"
it. Instead, YOU author the paper as a **tree of curated single-pass writes**:

1. **Design the tree** (you, from the `paper_subgraph` skeleton): a HOST frame +
   one chapter per deep development. The HOST's support layer is the main theorem,
   its direct combination inputs, and the chapter-level results — its instructions
   say: STATE each chapter-level result fully, with the one-sentence proof "The
   complete development is given in the dedicated technical section inserted
   below." (never a fabricated `\ref`), and prove ONLY the top-level assembly.
   Each CHAPTER is its own `paper_write` call with its own workspace
   (`paper_id=ch_*`), its own brief/ledger (`seed_ledger.py --paper`), and a
   **curated support layer (≤ ~10 facts — the BINDING RULE applies at every
   node)**; its instructions say: ONE short intro paragraph, a setup section, the
   lemmas in logical order, complete proofs; any prerequisite that is a result of
   the larger paper is declared explicitly in the setup ("we assume, established
   earlier in this paper: ...") — never re-proved, never hand-waved.
2. **Write the nodes** — independent `paper_write` calls (parallelize freely); a
   chapter that overflows the writer's single-response limit is a sign to SPLIT it
   into sub-chapters (deeper tree), not to chunk. Compile each node; run
   `paper_verify_math(paper_id=ch_*)` per chapter — its per-chapter verdict flags
   chapter-INTERNAL defects to fix now (a mangled induction, a dropped hypothesis)
   vs setup-imports (discharged at assembly, expected).
3. **Stitch (YOU are the editor — mechanical transforms only):** extract each
   chapter's body (drop title/abstract/acks/bib), demote sectioning one level,
   prefix every `\label`/`\ref` with `chX:`, wrap as
   `\section{<title>}\label{sec:tech-chX}`, insert the chapters **in topological
   order** before the host's assembly section, merge missing `\usepackage`s /
   `\newtheorem`s / macros / `\bibitem`s into the host (dedupe by name/key), and
   replace each host pointer-proof sentence with `Section~\ref{sec:tech-chX}`.
   Keep the stitch as a rerunnable script; **but every post-stitch edit lives on
   the merged file — re-stitching discards it**, so freeze the tree first, stitch
   once, then edit.

   **Stitch pitfalls (measured in a cold-start test — read before stitching):**
   - **Record a manifest at design time.** The pointer-proof sentences are
     byte-identical and carry no chapter hint; some chapters are pure support (no
     pointer at all). When you design the tree, record `{host theorem label →
     chapter paper_id}` and the intended insertion order in the tree-design file —
     don't force the assembler to re-derive it by reading statements.
   - **Ordering with delivered cycles.** Chapters written independently may have
     GENUINELY cyclic setup-imports (A assumes B's result, B assumes A's). No
     insertion order fixes that at stitch time — pick the order that points the
     most load-bearing arrows backward, and leave the residual forward edges to
     the seam-discharge stage (conditional restatement + later discharge).
   - **"Assembly section" means the main-theorem proof section.** If the host has
     OTHER full-proof sections that consume chapter results, they must ALSO end up
     AFTER the technical sections (relocate them), or the sequential verifier will
     reject the forward dependence.
   - **Macros: dedupe by name is unsafe on semantic conflicts.** Same-name macros
     with different bodies (e.g. `\join` as `\operatorname{join}` vs `\vee`)
     silently change a chapter's math if first-wins. Diff the bodies; on a
     semantic mismatch, rename in the chapter body. Preserve `\renewcommand` lines
     as-is (a chapter may legitimately renew a kernel command like `\H`); never
     downgrade them to `\newcommand`.
   - **Packages must merge BEFORE `hyperref`** (load-order trap); `\newtheorem`
     display-name variants for the same env — pick one.
   - **Bibliography:** import only `\bibitem`s whose keys are actually `\cite`d;
     first-wins on duplicate keys; DROP/replace keys the verified ledger marks
     rejected/unverified (a mechanical stitch happily keeps bad keys — check the
     ledger).
   - **The compile gate does NOT catch multiply-defined labels** — after
     namespacing, grep for duplicate `\label{...}` yourself.
   - **Chapter residue:** each chapter body still carries its own disclosure
     remark / `\note` annotations; the merged paper has N copies. Strip the
     duplicates at stitch time or queue them for the reviser — decide, don't
     ignore.
4. **Discharge the seams (reviser rounds on the merged paper, `notes=` trigger):**
   rewrite every chapter setup item "established earlier in the larger paper" to a
   precise `Theorem~\ref{...}` of THIS document; replace stale `[cite/blocker]`
   notes with precise `\cite` of ledger-verified keys; point the host assembly's
   invocations at the chapter theorems. **SEAM ACYCLICITY (load-bearing):** the
   whole-paper verifier reads SEQUENTIALLY — a proof may rely only on EARLIER
   results. Insert chapters in dependency order, and a setup item must point
   BACKWARD; if a chapter genuinely needs a LATER result, restate the affected
   theorem as explicitly conditional ("Assume (H). Then ...") and add, at the later
   point where (H) is proved, the one-sentence unconditional combination. Better:
   prevent it upstream — write chapter briefs so each chapter assumes only EARLIER
   chapters' outputs.
5. **Gates as usual on the merged paper:** compile + reference chain (reuse the
   project's VERIFIED ledger for the merged workspace) + `paper_verify_math` →
   iterate the discharge (and, for a genuinely missing development, grow the tree:
   one more small curated chapter, stitched in — never a fact pile to the reviser).

### 3. Compile-verify (hard gate)

```bash
bash .../write-paper/driver/compile_verify.sh <project>/paper/main.tex
```

Runs the LaTeX engine (default `pdflatex`; `xelatex`/`lualatex`/`tectonic` via
`TEX_ENGINE`); fails on any LaTeX error or any undefined citation/reference. With
no TeX Live installed, `TEX_ENGINE=tectonic` (after `bash scripts/install-tex.sh`)
is the zero-dependency engine.
**Do not proceed past a failed compile** — feed the offending log lines back to a
codex revise round (stage 5) and recompile. The compile is the **tool's /
orchestrator's** gate, never the reviser's own self-check (the reviser runs in an
empty cwd and cannot compile). **Authority boundary:** `paper_write` does NOT
compile — run this gate once on the writer's first `main.tex`. `paper_revise`
**retries the compile internally** (re-drives the reviser with the failing log
until the .tex compiles, or fails honestly), so a `paper_revise` returning
`compile="ok"` has ALREADY compiled — do **not** redundantly re-run this gate after
it; only run it after `paper_write` or a hand edit. A broken `.tex` must never be
delivered or pushed.

### 4. Reference audit (REFERENCE_AUDITOR) — FLAG, never fabricate

**Call the `reference_audit` tool.**

```
reference_audit(project=<project>, paper_id=<paper_id|omit for default>)
```

The tool assembles the auditor prompt (`roles/AGENTS.md` +
`roles/REFERENCE_AUDITOR_PROMPT.md` + `main.tex` + `REFERENCE_LEDGER.md` — and
**nothing else**: the auditor never sees the fact graph, the style guide, or the
structure plan) and drives a codex that has **no tools and no network**. The
auditor **only flags** entries it cannot vouch for; **verification is
`reference_verify`'s job** (Stage 4.5), not the auditor's. It returns
`{findings, ledger_path, status, returncode, log_path}`
and
writes **no** `main.tex`.

Take the auditor's `findings` and hand them straight to `reference_verify` (Stage
4.5) — that is where the flagged entries get checked online. As with
`paper_write`, a non-`ok` status means the audit run failed — do not treat empty
findings as a clean bibliography.

### 4.5 Reference verify (REFERENCE_VERIFIER) — online per-entry verification

**Call the `reference_verify` tool** with the auditor's findings.

```
reference_verify(project=<project>, findings=<the auditor's findings text>, paper_id=<paper_id|omit for default>)
```

This is the **online** half of the reference chain — `auditor (offline, flags) →
verifier (online, checks) → reviser (edits)`, symmetric to the proving chain
`worker → verifier → fact_graph`. The tool assembles the verifier prompt
(`roles/AGENTS.md` + `roles/REFERENCE_VERIFIER_PROMPT.md` + `main.tex` +
`REFERENCE_LEDGER.md` + the auditor's `findings` — and **no fact graph, style, or
structure**) and drives a codex over the **networked** path:
`--dangerously-bypass-approvals-and-sandbox` + the danus gateway at
`DANUS_ROLE=verifier` (exposing only `search_arxiv_theorems`, minimum privilege) +
codex's built-in `web_search`. The codex still runs in an empty cwd, so it cannot
touch the project tree; its only outward reach is the gateway's read-only tool +
web.

Per flagged entry it does: `search_arxiv_theorems(statement/title)` → best
`arxiv_id` → open `https://arxiv.org/abs/<id>` for the authoritative
authors/title/year + journal-ref, confirming it is the **same** paper (not merely
"a similar theorem exists"); non-arXiv references (textbooks / old journals) →
targeted web search at an authoritative source (publisher / DOI / zbMATH / DBLP).
It emits one verdict object per entry (`verified` / `corrected` / `rejected` /
`unverifiable` / `retarget-internal`) plus a one-line

…(truncated)