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.

5.5 Math-verify (WHOLE-PAPER) — re-verify the paper AS WRITTEN (HARD GATE)

Call the paper_verify_math tool. This is the gate that makes the paper — not just its facts — correct.

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

Why this stage exists. Each fact was verified individually before it was ever written. But the paper is a different artifact: the writer re-renders and re-stitches those facts for publication — concising, dropping "obvious" steps, adding "it suffices to…", "WLOG…", and inline reductions that were never themselves a fact. Those seams are exactly where a correct set of facts becomes an incorrect paper. A fact's earlier correct verdict does not transfer to its re-stitched paper rendering.

What the tool does. One fresh paper-math verifier codex (a dedicated role — separate from the fact-submission verifier and the reference verifier; a one-shot run, no resident service) reads the whole main.tex development in reading order plus the confirmed REFERENCE_LEDGER.md. It trusts the confirmed precise citations and scrutinizes the paper's own reasoning and self-containedness — no fact graph, no slicing. The verifier CLASSIFIES every finding it raises under one strict criterion: ignorable if a mathematics undergraduate could fill or follow the step unaided (a routine computation, a standard manipulation), must-fix for everything else (a missing definition, a load-bearing step with no derivation and no citation, an argument it cannot follow, a wrong deduction). The paper passes (correct) iff it has zero must-fix findings; any must-fix ⇒ wrong. The tool writes ONE whole-paper row to <paper>/VERIFY_LEDGER.md (only the tool writes verdict rows), carrying the must-fix findings in repair_hints and the ignorable ones in the row's ignorable field, and returns {status, verdict, repair_hints, must_fix, ignorable, ignorable_findings, body_chars, ledger_path, log_path, deliver_ok, blockers}.

Honesty: a failed verify RUN (codex error, unparseable verdict) is status="verify_error" — NOT a paper that passed; status="passed" requires an actual all-clear (no must-fix findings). Do not treat a verify_error as a clean paper.

The ignorable findings — record and surface, never chase. These are the steps the verifier judged an undergraduate could fill. They do not block deliver and they are not yours to fill on a whim: leave the text as written, keep the verifier's ignorable list verbatim in your deliver report, and — if any of them still feels worth expanding — hand THAT decision to the operator. Chasing ignorable findings to force a longer paper is exactly the transcription bloat the writing principles forbid. Your active work is the must-fix list only.

On must-fix (verdict wrong) — the verify → revise loop (you drive it, reading the ledger, not your memory). repair_hints carries the verifier's located must-fix findings (which theorem/paragraph, what is broken). The verifier has already done the ignorable-vs-real classification; you do not re-litigate it — you ACT on each must-fix. For each:

−1. A must-fix means there is a genuine gap to CLOSE — not a fact to drop in. Do not think of it as "find the backing fact and paste it." A must-fix is the paper itself being incomplete at that point: it may be one fact rendered unclearly, or a whole sub-development that was never written up, or a step that is actually wrong. Your job is to make the paper complete THERE — by writing the missing argument from verified facts (curate + render, §0–§2 below), or, when no fact establishes it, by sending it back to the swarm to be proved. You never author the mathematics yourself (the fact graph is the only source; see paper-never-author-math). What you never do is smooth a must-fix over with a summarizing phrase — that is precisely what the verifier rejected.

A must-fix that needs MANY facts — KEEP CURATING, KEEP WRITING. If filling a gap would take dozens or hundreds of facts, that is NOT a reason to stop or defer. It means the gap is itself a development that gets the SAME treatment as the paper: extract its support layer and keep writing — and recurse again if a sub-gap is deep in turn. The development's full-closure size is NOT the decision metric — measuring the transitive closure and giving up is the original overflow fallacy in new clothes. Concretely, recurse the curation principle onto the development itself: select ITS OWN support layer (the 10–20 facts that carry the argument — the base cases, the induction mechanism, the endpoint), and write it as a dedicated section at expert compression (the synthesis doctrine), triaging its sub-steps like any other content (standard-type sub-computations summarized, per the active criteria). THE TOOL FOR A DEEP GAP IS THE WRITER, NOT THE REVISER. The dedicated section is a NEW paper_write call (its own curated support layer and brief, stitched in per stage 2b — same seam rules), after which the reviser only wires the seams (\refs, setup pointers). paper_revise(add_facts=…) is reserved for LOCATED point repairs — re-rendering a mangled proof, adding the one missing step, a handful of facts (≤10) — never for a development: a fact pile fed to the reviser accretes a flat lemma blob and inflates the paper ~5–14K/round (measured), which is exactly the failure stage 2b exists to prevent. THE GAP-FILL BRIEF CONTROLS THE LENGTH — the writer has no idea of your budget. A writer call knows only what you hand it; its default register is "standalone paper" (title, intro, notation section), and nothing in its role prompt sees the host paper. So every gap-fill paper_write brief states: (a) REGISTER — "one SECTION of an existing paper, NOT a standalone paper: no title/abstract/intro/notation section; open inside the host's standing conventions" (attach the host's setup and the labels it may \ref); (b) INTERFACE — exactly the statement(s) it must deliver, what it may assume from earlier sections, and WHICH steps are the section's pivots (name them — those get derived; every unnamed step stays at mechanism+outcome); (c) a NUMERIC target from the expert-compression calibration (a deep-gap section: 2–3 pages / 6–10K — a 2–4K frame plus ~2–4K of derivation per novel pivot; see THE PIVOT IS NOT COMPRESSIBLE); (d) the proof-style spec, verbatim. Input curation is the other half of the lever: a ~10–20-fact support layer physically cannot balloon into 30 pages — hand it a closure instead and no brief will save you. Calibrate the cost at EXPERT COMPRESSION, not transcription: a human expert rendered a comparably deep flagged step in under 2K chars; a gap fill should typically land at 1–5K. If your estimate says +30K, you are estimating transcription — fix the instruction, not the budget. If the budget is genuinely tight, the cause is almost always UPSTREAM STRUCTURE, not the new content: earlier sections are wasting space (verbose renders, redundant setup/notation blocks, lemma sprawl, duplicated disclosures). Recover the space by LOCATED dedup edits you identify yourself (never a global compress order — the reviser cannot execute one; see the editorial bar), then write the gap. You do NOT defer a must-fix on your own authority: the companion-paper / conditional-statement / override forks exist, but they are decisions only the OPERATOR can initiate; your default is always: as long as a must-fix stands, you write. THE SPIN-OFF FORK — raise it, don't decide it. If the paper you have is otherwise a sound, well-structured ~30-page article, but your honest estimate says this ONE detail cannot be filled within a few pages even at expert compression, do not silently grind it in and do not silently drop it: REPORT the state and ASK the human whether the detail should become its own paper (the paper_id mechanism — a technical companion the main paper cites). Asking is not deferring: the decision stays with the human; you supply the honest estimate. THE PROOF-STYLE SPEC — what to write, and what NOT to write. The measured gap: an expert wrote a deep two-part lemma proof in ~1.6K chars; our renders of comparable content ran 10–15×. The difference is never the mathematics — it is CEREMONY. Put this spec verbatim into every rendering instruction you issue: - Write inside the paper's standing conventions. Never restate hypotheses or re-quantify objects the section's setup already fixes — one clause ("with notation as in Setup X") suffices. Fact-graph statements are fully self-quantified BY DESIGN; a rendered proof must NOT inherit that register. - Prose first. Manipulations flow inside sentences; display ONLY the one or two equations the reader must refer back to. A proof that is a chain of displayed equations is a computation log, not a proof. - One proof, no ceremony. Absorb sub-steps as sentences ("since … and …, it follows that …"). A new labeled lemma is justified ONLY when it is cited from ≥2 places or is genuinely independent — never one lemma per source fact. - Mechanism, pivot, close. Name what is computed, give the pivotal identity, conclude. Trust the competent reader for routine expansion — the verifier accepts mechanism+outcome for standard-type steps; what it rejects is a bare claim with NO mechanism. - Calibration: a deep lemma proof lands at 0.5–2K chars; if a single proof render exceeds ~4K, you ordered transcription — rewrite the instruction, not the budget. - THE PIVOT IS NOT COMPRESSIBLE. Mechanism+outcome is accepted for standard-TYPE steps ONLY. The argument's own NOVEL pivotal computation — the step that is this paper's contribution — must be DERIVED, not named (measured: two 2-page gap-fill sections were rejected at exactly their named-not-derived pivots, while every surrounding mechanism+outcome standard step was accepted). Budget a deep-gap SECTION at 2–3 pages / 6–10K: a 2–4K frame plus ~2–4K of actual derivation per pivot; a 1–2-page ask gets the frame right but forces the pivot into a bare name, which fails verification. Deriving a pivot does NOT suspend the style spec — the derivation is written like every other proof here: prose-first, one or two displays, standing conventions (the measured expert proof derived its pivot INSIDE 1.6K chars; deriving ≠ transcribing). If a derived pivot exceeds ~4K, the instruction ordered transcription — rewrite it. And YOU name the pivots in the brief — typically ONE step per section, the step that is that section's contribution; every step you did not name stays at mechanism+outcome. A writer left to guess which steps count will defensively derive everything — that is the transcription failure returning through the back door. - Named anti-patterns (put these in the instruction as prohibitions): requantification blocks; display-per-step; per-fact lemma-ization; "we now verify / recall that" scaffolding; restating definitions before use. THE ONE EXCEPTION — stop and ask the human. When you genuinely judge you cannot get it right; or two-to-three consecutive rounds on the SAME gap have produced no effective progress (verdict unchanged, findings not narrowing); or your edits are making the paper WORSE (regressions, new findings outpacing cleared ones, structure degrading) — STOP. Preserve the best state, and consult the operator with an honest account: what you tried, why it failed, and your best guesses. Grinding past that point burns budget and damages the paper; asking is the professional move, not a failure. Deliver honestly either way: report the verifier's verdict as it stands, with the verifier's ignorable list attached (which must-fix you filled, which ignorable findings remain) — never present a must-fix you smoothed over as "passed".

THE TERMINAL STATE — "passes modulo ignorable computations". On a paper written from verified facts, expect the FIRST verify to yield mostly ignorable findings plus AT MOST one or two must-fix structural gaps. Fill only the must-fix ones (each a small curated supplement — a support layer and a few K of expert-compressed writing), re-verify once, and you should reach zero must-fix with only an ignorable residual. Zero must-fix IS the successful end of the loop (the tool reports correct / deliver_ok): stop, report the verdict with the ignorable list, and hand the fill-or-not calls to the operator. Do NOT expand ignorable items to make the paper longer — the verifier already judged a competent reader fills them, and chasing them is how a paper bloats into a monograph. If you find yourself in a fourth-plus revise round still filling, STOP: you are over-filling ignorable content the verifier never asked you to write.

THE QUALITY BACKSTOP — fewer findings is not the goal; a better paper is. Keep the TOTAL number of writing rounds small (the healthy trajectory: one curated write + small located fixes + at most one real must-fix supplement). Across rounds, judge the PAPER, not just the findings count: if findings are going down but the paper is getting worse — narrative giving way to fact-stacking, structure fragmenting, length creeping — the loop is destroying value, and clearing more findings will not buy it back. STOP at once: preserve the best state, tell the human WHERE the writing difficulty is (which section, which kind of content, what you tried) and what guidance you need. And in ALL cases — success, stall, or stop — leave behind one final paper that is ELEGANT and carries an honest, located list of its remaining gaps, so a human knows exactly what is unproven and where. An elegant paper with known gaps is a deliverable; a gap-free fact-stack is not.

0. FIRST — fed ≠ rendered: read what ACTUALLY landed, not your memory of what you sent. Handing a fact to paper_revise(add_facts=…) does NOT mean its PROOF is in the paper. The reviser routinely renders the fact's statement as a lemma while its proof still asserts a step that the fact ITSELF delegates to a deeper fact ("by Fact X"). So before deciding what to send, do THREE reads: (a) the verifier's located finding — WHAT is flagged; (b) the reviser's actual rendered proof of that lemma in main.tex — what really landed; (c) the source fact's own proof in the fact graph. If that fact's proof discharges the flagged step by CITING a deeper fact, that deeper fact (and its sub-chain) is the true missing chokepoint — trace the by Fact … chain down to the fact whose proof actually contains the flagged computation, and feed that, bottom-up (a fact renders self-contained only once ITS predecessors are already rendered, so their \refs resolve instead of becoming stripped assertions). Counting a fact "done" because you sent it once under-counts the real depth — its delegated sub-proof can be dozens of facts — and misattributes a depth gap to "reviser fidelity." (Measured example: the MatTan ω(S) degree-formula fact delegated to a 121-fact induction that was never rendered; re-sending the top fact could never close it.) Only when the fact's own proof CONTAINS the flagged step in full, yet the paper still asserts it, is it a genuine fidelity problem → step 1a.
1. If it concerns the re-rendering of a verified fact (the writer compressed or mangled a proof that was already verified), re-render it — but instruct SYNTHESIS, never transcription: resolve the theorem's \label → source fact id via <paper>/.provenance.json, read that fact's proof (and, per step 0, the sub-facts it delegates to) from runtime/projects/<p>/fact_graph/facts/<id>.md, and — this is YOUR judgment step — name the argument's skeleton yourself (its 2–4 key steps) in the instruction you pass with the verified proof text to paper_revise(notes=…). Ask for ONE compact-but-complete proof at paper granularity, written as an expert author writes: every claim carried by an actual argument (never a bare "by the same argument" / "a similar computation"), short steps written in full, standard-type sub-computations stated with their precise mechanism and outcome; forbid one-lemma-per-fact transcription and helper-lemma sprawl. The support-layer BINDING RULE applies INSIDE proofs too: you curate what the proof presents, the renderer writes it. Per-round add_facts follows the BINDING-RULE spirit: a small bottom-up set (~10-15 facts at most); several small rounds beat one dump. 1a. If a compact synthesis is rejected, refine — do not jump to transcription. The verifier rejects bare assertions, not compactness (measured on the same deep step: a human-expert 1.6K compact rendering passed independent expert review, while a per-fact transcription of identical content ran 28K — 17× — with helper-lemma sprawl; forced-transcription orders were the bloat source, and are how a paper degenerates from an article into an unreadable monograph). So on a re-flag: read WHICH mechanism the verifier says is missing, and instruct adding exactly that step — still synthesized, still one proof. If two such refinements fail, suspect your fact selection first (step 0: fed ≠ rendered — the real chokepoint may be a deeper delegated fact), and only as a LAST resort order a fuller write-out of the one specific step (never the whole chain), accepting the local bloat knowingly.
2. If it is genuinely new paper math (glue, a reduction, a combined argument), pass the located finding itself to paper_revise(notes=…) for a real fix — or, if the paper is missing a prerequisite, re-select facts / re-run paper_write.
3. Recompile (Stage 3) → re-run paper_verify_math. Keep the loop bounded (~5 rounds); on overrun stop and escalate to the operator with the ledger as the honest record. (The verifier is an LLM and has run-to-run variance — a wrong that flips to correct with no edit is that variance; the loop absorbs it, so never hand-mark the ledger to defeat the gate.)

On too_large — YOU decompose; the tool never chunks. too_large means the assembled verifier input (role prompt + REFERENCE_LEDGER + the whole main.tex body) exceeds DANUS_PAPER_VERIFY_WHOLE_DOC_CAP (default ~700K chars ≈ 175K tokens): one codex call cannot hold the paper. The tool records the blocker honestly and does not split — decomposition is a judgment call, so it is yours:

1. First check whether the cap is just conservative: if the verifier model's context genuinely fits the prompt (body_chars in the envelope), raise DANUS_PAPER_VERIFY_WHOLE_DOC_CAP and re-run the tool. Done.
2. Otherwise decompose the paper by its results — never by position in the text. The verifier's contract is the constraint: it judges whether a document, read on its own, establishes its main result — so every part you send must BE such a document, culminating in a designated result. A sequential slice (consecutive pages or sections chosen for length) fails this: a middle slice culminates in nothing, and the verifier has no main result to judge. Instead, pick the paper's major results R1…Rn (the main theorem plus the big propositions it rests on) and build one part per result. Part k's input document is:
   • the paper's notation base: preamble macros + every Definition/Notation env;
   • the full statements only (no proofs) of the other designated results that part k's proofs rely on, presented as "established elsewhere in this paper (separately verified)";
   • the complete development of R_k as written (its supporting lemmas and R_k itself, statements + proofs), ending at R_k — the part's own main theorem. Each part must stand on its own given those established statements — that is what "self-contained" means here — and sit comfortably under the cap. The part for the paper's main theorem takes the other designated results as established and closes the argument.
3. Drive the verifier yourself, mirroring the tool: read agents/skills/write-paper/roles/PAPER_MATH_VERIFIER_PROMPT.md (and roles/AGENTS.md), append the confirmed REFERENCE_LEDGER.md and the part document, and run a fresh bin/codex exec --sandbox read-only per part; read the final findings JSON from its output. A part is clear iff it has zero must-fix findings (an ignorable-only residual still clears — record and surface it). A part carrying any must-fix → the revise loop above for those findings, then re-verify that part and every part that took its statement as established.
4. Clearing the gate: the ledger still holds the too_large row and only the tool writes verdicts — so surface the per-part record (each part's scope, verdict, log) to the operator, and only on their explicit confirmation set the whole-paper row's status to overridden with a note pointing at that record. That is the operator-override channel deliver_ok accepts (correct / trusted / overridden). Never do this silently.

Deliver is BLOCKED unless the whole-paper verification is correct or the operator explicitly overridden (the deliver_ok / blockers fields; paper_math_verify.deliver_ok reads the ledger deterministically). Override is an operator per-paper policy (default mandatory-verify): the operator may choose to ship despite a still-failing or too-large verification — but it is then visibly flagged in the paper (a \note / disclosure line), surfaced as a fork, never silent. Set the ledger status to overridden only on the operator's explicit call.

6. Deliver + (operator fork) push

Deliver the main.tex + main.pdf paths. First confirm the deliver gate: the whole-paper math verification (Stage 5.5) must show deliver_ok=True (the whole-paper verification correct, or an explicit operator overridden) — never deliver a paper whose math was not re-verified as written. Pushing to a LaTeX git repo (e.g. Overleaf) / posting to arXiv is outward — an operator fork (your standing red line: confirm anything that leaves the machine). driver/latex_git_push.sh handles the push; if it lacks the repo URL / token, ask the operator, store the non-secret config in your own notes and the token in the gitignored secrets file (see the script header), then confirm before pushing.

Default house style (configurable — lives in STYLE_GUIDE.md / PAPER_STRUCTURE.md)

The non-negotiable part is integrity, not typography: preserve the mathematics, cite honestly, never fabricate a reference, leak no pipeline metadata (the PRIME DIRECTIVE in roles/AGENTS.md). Everything else — document class (amsart by default), \epsilon, the manual surname-sorted \begin{thebibliography}{99}, manual Theorem~\ref{} cross-references, exact citation numbers, the filler bans, and the acknowledgement disclosure — is the default AMS-style house style. It lives in STYLE_GUIDE.md / PAPER_STRUCTURE.md, is embedded into the codex by the tool, and is the operator's to change (edit those files, or override per paper in PROJECT_BRIEF.md). You never apply it yourself — you do not write LaTeX.

Honesty (load-bearing)

State only what you verified. A paper is "produced" only after compile_verify.sh passed (PDF, zero errors, no undefined citations) and paper_verify_math shows deliver_ok=True (the paper re-verified correct as written, or an operator overridden) — "it should compile" / "the facts were already verified" is not confirmation (the paper re-stitches the facts, so it is re-verified as a distinct artifact). If the auditor could not verify a reference, say so; do not present an unverified bibliography as checked. Never claim a push succeeded unless you confirmed it landed.

Style maintenance (offline, operator-gated; the anchor preflight is stage 1a)

roles/STYLE_DISTILLER_PROMPT.md distills recurring rules from the operator's own papers under style/anchors/ into the unified style/STYLE_GUIDE.md, as proposals the operator accepts or rejects — it never auto-applies an edit, and it never touches any paper's main.tex. A bad distill would silently corrupt the guide that governs every future paper, so the accept gate is mandatory.

It is presence-triggered, once, operator-gated (stage 1a above): it runs in the preflight only when anchors/ is non-empty AND stale (newer than style/.distilled_at, or that marker is absent), so anchors an operator drops in are distilled rather than silently ignored — but it never runs when anchors/ is empty or unchanged, and it is not part of the per-paper hot path (the writer consumes the already-distilled guide). The operator may also run it by hand at any time.