---
name: elaboration
description: Write a high-signal mathematical synthesis from global memory and the fact graph for the Codex main agent's own strategy and worker dispatch.
---
# Elaboration
You are the **main agent**. At each strategic cycle, including the global review
on each roughly 30-minute heartbeat, you distill the project's current state into
one **elaboration** when the synthesis materially changes: a readable, deeply
analytical synthesis for your own reasoning and worker dispatch. The heartbeat
itself always requires a fresh global appraisal, but it need not create a
duplicate elaboration when nothing material changed. You may ask speculative
Codex subagents to explore individual gaps or undertake sustained technical
reasoning, but their reports remain unverified and must be labelled as
hypotheses. You author the next `master_guidance` yourself.
The elaboration is also what you draw on to keep the operator informed.
## Template invariants (validate every elaboration against these)
A well-formed elaboration satisfies all of the following — a worker or linter can
check them mechanically:
- **Five sections, in order, no dropped heading:** §0 Mathematical verdict · §1
Closed components and obsolete routes · §2 Interface contract table · §3
Dangerous heuristic lines and strategies not to pursue · §4 Missing bridge
lemmas. An empty section is written as its honest empty-state line, never
omitted.
- **The two fixed empty-state lines** (§1) are used verbatim when a subsection is
empty:
- `_(no signed-closed components yet)_`
- `_(no failed or obsolete routes recorded; absence here does not mean the strategy is unique)_`
- **Exactly seven status labels**, UPPERCASE, drawn only from: **CLOSED ·
SUBSTANTIAL · PARTIAL · DANGEROUS · FALSE AS STATED · OBSOLETE · UNKNOWN**.
- **§0 opens** with exactly one bolded verdict line and contains the status
dashboard table + the sub-task status summary table + the approach portfolio +
the Current best proof skeleton + the Central missing lemma.
- **Every `fact_id` cited exists** in the fact graph; no invented ids, no
paraphrase substituted for a verified statement.
- **Published** via `gm_add(kind="elaboration", …)` with `verifiable` left at its
default (`false`).
## Input Contract
Read **only the shared stores** — never a worker's private local memory (a layer
boundary, and the reason this is cleaner than a log-scraping summary agent). All
reads are project-scoped for the main agent (`project=`):
- **global memory** — findings, dead ends, recent `verification` traces, the
current `master_guidance`. Read via `gm_search`, or as a fallback by reading the
raw `runtime/projects/
/global_memory/.jsonl` files.
- **fact graph** — the verified facts, their statements, and the DAG. Read via
`fact_search`, or as a fallback by reading the raw
`runtime/projects//fact_graph/facts/*.md` files: what is established vs. still
open, and how facts compose.
- **the project's problem statement** — the fixed goal and, if present, its
enumerated sub-tasks / intended proof architecture.
## The fixed goal is sacred
Quote the goal and **do not change or weaken it** — do not redefine, simplify,
restrict to a special case, or substitute an easier proxy. If the evidence
suggests the goal may be false or unreachable by the current strategy, **say so
plainly while keeping the goal fixed.**
## Template — five sections
Produce one markdown document with these sections, in order. Omit a section's
body only by writing the honest empty-state line, never by dropping the heading.
### 0. Mathematical verdict
Open with **one** of these, in bold on its own line:
> **Not solved.** … | **Counterexample found.** … | **Verified complete proof.** … | **Solved.** …
Then:
- **Closed components** — what is signed-closed today (1–2 sentences; cite `fact_id`s).
- **Viable proof architecture** — one sentence naming the current best route.
- **Main blocker** — what concretely blocks right now (1–2 sentences; cite `fact_id`s).
- **Highest-priority unresolved bridge** — the most leveraged missing lemma / integration package.
- **Method failure vs. proposition failure** — state explicitly whether the evidence indicates a *method* has failed (the conjecture may still hold) or the *proposition itself* may be false. Use the phrase "method failure" or "proposition failure" verbatim.
- **Calibration caveat** — one line warning the reader against over-reading status labels (e.g. "Do not read SUBSTANTIAL/CONDITIONAL as 'almost solved' — every such row has an unmatched hypothesis on the actual model.").
Then a **status dashboard** (one table) with at least these rows: Fixed goal
(UNCHANGED, with goal text); Verified complete proof (YES/NO); Verified
counterexample (YES/NO); Signed-closed sub-tasks (count + names); Main blocker
(a specific lemma, not vague); Routes marked false/obsolete (YES/NO + which);
Highest-priority unresolved task (P0/P1/P2 with the exact mathematical task).
Then a **sub-task status summary** (one table: Sub-task | Status | Closed facts |
Conditional facts | Main missing interface), one row per sub-task the problem
enumerates. Use **only** these UPPERCASE labels:
- **CLOSED** — verified on the *actual* construction, no remaining
hypothesis-matching. A theorem import or conditional package being available is
**not** CLOSED — that is SUBSTANTIAL. CLOSED is rare; default away from it.
- **SUBSTANTIAL** — a conditional package exists, but ≥1 input/output hypothesis
is unmatched on the actual construction. The *default* for a sub-task with
load-bearing tools not yet applied to the actual model.
- **PARTIAL** — isolated ingredients only; no coherent conditional package yet.
- **DANGEROUS** — a plausible shortcut that is false / insufficient / hypothesis-sensitive.
- **FALSE AS STATED** — a once-plausible formulation now refuted; do not pursue as stated.
- **OBSOLETE** — superseded by a better route; do not pursue.
- **UNKNOWN** — insufficient verified information.
> **Strict CLOSED test.** For each sub-task you are tempted to mark CLOSED, ask:
> "Is there a verified fact that handles this on the *actual* construction, with
> zero remaining hypothesis to match?" If you cannot answer YES with a specific
> `fact_id` and zero remaining work, mark SUBSTANTIAL. Over-marking CLOSED is the
> single most damaging error here — it reads as "no further work needed."
Then an **approach portfolio** (one table: Approach | Mechanism | Mathematical
frontier | Decisive obstacle | Evidence for/against | Active/parked | Revisit
condition). Include every credible route still worth remembering, not only the
currently dominant route. Preserve parked routes and their return conditions so
that recent work cannot silently erase a serious alternative. If a major route
choice has changed, state the alternatives considered and the mathematical
reason for the change; this decision must also be preserved in the subsequent
`master_guidance`.
End §0 with **Current best proof skeleton** (6–12 short numbered lines: the
smallest structure that closes the goal *if* the central missing lemma were
known, with `fact_id`s where facts apply) and **Central missing lemma** (the
single most precise unresolved statement, at full precision — all quantifiers,
definitions inlined for self-containment, and one short "why this is non-trivial"
paragraph if warranted).
### 1. Closed components and obsolete routes
- **Signed-closed components** — a bullet list ("