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

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 .../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):

   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 \usepackages / \newtheorems / macros / \bibitems 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 \bibitems whose keys are actually \cited; 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 .../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 replacement suggestion for the reviser, writes the confirmed metadata back into REFERENCE_LEDGER.md (each promoted row marked verified-by: verifier + source_url), and returns {verdicts, ledger_path, status, returncode, stderr_tail, log_path}. It never touches main.tex — applying the replacements is the reviser's job (Stage 5). unverifiable entries keep their [cite/blocker] flag.

Honesty: the ledger is updated ONLY on an honest ok run (zero exit, non-empty output). A nonzero exit / empty output / timeout → status != "ok" and the ledger is not touched — no false promotion. A degraded/offline run whose verdicts are all unverifiable promotes nothing.

Handoff to Stage 5. Collect each verdict's one-line replacement_suggestion and pass them to paper_revise as its citation_fixes argument — that is the verify→revise seam. The reviser applies those fixes against the \bibitem/ledger keys already present (never invents metadata); any [cite/...] still needing an external source and not covered by the fixes stays a [cite/blocker] marked \note{[deferred: to reference_verify]}. The three-stage chain is: auditor flags offline → verifier verifies online + writes the ledger → reviser applies the fixes into main.tex.

5. Revise (PAPER_REVISER) — on compile failures, verifier fixes, operator annotations, or a math wrong

Call the paper_revise tool when: a compile failed; the verifier returned citation fixes to apply; the operator added \edit{...} / \note{...} editorial annotations; or paper_verify_math returned wrong (pass its located findings — and, for any re-rendered fact, the fact's verified proof — via notes; Stage 5.5 says how).

paper_revise(project=<project>, compile_log=<failing pdflatex lines>, notes=<operator direction / math findings + verified proofs>, citation_fixes=<verifier replacement suggestions>, paper_id=<paper_id|omit for default>)

The tool assembles the reviser prompt (roles/AGENTS.md + roles/PAPER_REVISER_PROMPT.md + style/STYLE_GUIDE.md + main.tex + the REVISION_LOG.md tail + the trigger you passed as compile_log / citation_fixes / notes — and no fact graph), drives a codex, and — on a clean gate — overwrites <project>/paper/main.tex. Pass the offending log lines from a failed compile as compile_log, the verifier's per-entry replacement suggestions as citation_fixes (Stage 4.5's seam), and any operator editorial direction or math findings as notes.

• Change scope is governed by the trigger type. A compile_log → the reviser fixes only the compile errors; notes/citation_fixes → it acts only on those items; gap_fill (verifier feedback + facts to add) → it proves the supplied facts into the paper (the one trigger allowed to change formal content); no trigger → the global style-audit rewrite. (The tool prepends a MODE: line the reviser branches on.)
• The compile is the tool's gate now, not the reviser's self-check, and paper_revise retries it internally. After the leak gate the tool compiles the revised .tex outside the reviser; if it fails, it re-drives the reviser with the failing log (carrying the same notes/citation_fixes) up to DANUS_WRITE_PAPER_COMPILE_ATTEMPTS (default 3). On success it writes main.tex and returns compile="ok" + compile_attempts. If the LaTeX engine is missing it cannot gate what it cannot run: it writes once, returns compile="skipped: no engine", and you should run the standalone compile_verify.sh when a toolchain is available. If attempts are exhausted it does not overwrite main.tex, quarantines the last attempt to main.uncompiled.tex, and returns status="compile_failed" with a log tail.
• The revise output passes the same leak gate as paper_write. A fact_id / machinery token in the revised .tex → quarantined to main.leaky.tex, main.tex not overwritten, status="leak".
• REVISION_LOG.md now carries the reviser's real round summary (the %%%REVISION_SUMMARY%%% section of its output), not a boilerplate stub — the tool splits the output and writes the actual summary as the log entry body (or a [degraded: ...] note if the reviser emitted no summary section).

It returns {tex_path, status, returncode, revision_log_path, leak_findings, compile, compile_attempts, stderr_tail, log_path}; on a non-ok codex status nothing is overwritten. Recompiling standalone (stage 3) after a revise round is your independent confirmation, but the tool has already gated the compile internally.