# E022-E023: Design docs missed quality and efficiency targets in retrieval

Condition: Retrieval · 400k-line codebase · 5 questions · z3-checked algebra · Result: not supported · 2026-09-24

Before a planned change, the agent explained one part of a large application. Neither design form met the retrospective +0.1 correctness target and reliably saved tokens and time. With gpt-6-sol both forms used more tokens on most questions, while with gpt-6-luna Prose docs used fewer on every question.

## Results at a glance

| Run | Arm | Average score | Stages compared | Tokens | Time |
|---|---|---:|---:|---:|---:|
| E022 · gpt-6-sol · medium | No docs | **0.934** | 5 of 5 | **1.23M** | **0:09:31** |
|  | Prose docs | 0.906 (−0.028) |  | 1.56M (+26%) | 0:09:32 (+0.2%) |
|  | **Algebraic docs + z3** | 0.892 (−0.042) |  | 1.51M (+22%) | 0:09:51 (+3%) |

| Run | Arm | Average score | Stages compared | Tokens | Time |
|---|---|---:|---:|---:|---:|
| E023 · gpt-6-luna · medium | No docs | 0.800 | 5 of 5 | 1.35M | 0:07:14 |
|  | Prose docs | **0.820 (+0.020)** |  | **1.05M (−22%)** | 0:07:53 (+9%) |
|  | **Algebraic docs + z3** | 0.720 (−0.080) |  | 1.23M (−8%) | **0:06:56 (−4%)** |


Scores average the stages every arm of the run scored: the stages compared. Tokens and time are each run's builder totals over every stage it worked. Brackets compare with No docs. Highlighted values mark the highest quality score and lowest recorded tokens, time, and Python CC within each run; ties share the highlight. This does not mean the success rule passed.


## What changed in this condition

The agent builds nothing. Each stage asks it one question about a part of an existing application inside about 400,000 lines of vendored code: what the part is, what it must keep true, and how a planned change should go. Every arm gets the same instruction: write the answer to the file the prompt names, and change nothing else. The arms differ only in the design records already in the workspace. Each run uses a different builder model, to test the result at different model sizes.

- **No docs** (control): The code alone. No design records.
- **Prose docs**: The application's finished design, in prose.
- **Algebraic docs + z3** (hypothesis arm): The application's finished design in algebra, with its z3 proof files.


**Runs:** 2 (E022, E023), one per builder model.

- **E022:** gpt-6-sol · medium
- **E023:** gpt-6-luna · medium

**Agent harness:** `codex-cli`. **Judge:** `claude-opus-5-5-high`.


## Stage evidence

**Not supported.** Each part of the rule must hold in every run.

Stages:

1. `checks`
2. `ontology`
3. `operation`
4. `telemetry`
5. `composition`

**✗ Algebraic docs + z3 and Prose docs must each score at least 0.1 above No docs in every graded stage, in every run: not met**

| Run | Arm | Met | 1 | 2 | 3 | 4 | 5 |
|---|---|---:|---:|---:|---:|---:|---:|
| E022 · gpt-6-sol · medium | **Algebraic docs + z3** | 0 of 5 | −0.07 | −0.07 | −0.04 | −0.07 | +0.04 |
| E023 · gpt-6-luna · medium | **Algebraic docs + z3** | 0 of 5 | −0.04 | −0.07 | −0.18 | −0.07 | −0.04 |
| E022 · gpt-6-sol · medium | Prose docs | 0 of 5 | −0.03 | 0.00 | −0.11 | 0.00 | 0.00 |
| E023 · gpt-6-luna · medium | Prose docs | 1 of 5 | +0.03 | −0.07 | −0.11 | +0.22 ✓ | +0.03 |

**✗ Algebraic docs + z3 and Prose docs must each use fewer tokens than No docs in most stages, in every run: not met**

| Run | Arm | Met | 1 | 2 | 3 | 4 | 5 |
|---|---|---:|---:|---:|---:|---:|---:|
| E022 · gpt-6-sol · medium | **Algebraic docs + z3** | 1 of 5 | −7% ✓ | +36% | +18% | +64% | +6% |
| E023 · gpt-6-luna · medium | **Algebraic docs + z3** | 3 of 5 | −20% ✓ | +16% | −33% ✓ | +1% | −2% ✓ |
| E022 · gpt-6-sol · medium | Prose docs | 0 of 5 | +9% | +63% | +34% | +9% | +25% |
| E023 · gpt-6-luna · medium | Prose docs | 5 of 5 | −12% ✓ | −43% ✓ | −21% ✓ | −42% ✓ | −2% ✓ |

**✗ Algebraic docs + z3 and Prose docs must each use less time than No docs in most stages, in every run: not met**

| Run | Arm | Met | 1 | 2 | 3 | 4 | 5 |
|---|---|---:|---:|---:|---:|---:|---:|
| E022 · gpt-6-sol · medium | **Algebraic docs + z3** | 2 of 5 | −24% ✓ | +11% | +1% | +32% | −4% ✓ |
| E023 · gpt-6-luna · medium | **Algebraic docs + z3** | 1 of 5 | +31% | +5% | −37% ✓ | +2% | +8% |
| E022 · gpt-6-sol · medium | Prose docs | 3 of 5 | −15% ✓ | +28% | +23% | −20% ✓ | −9% ✓ |
| E023 · gpt-6-luna · medium | Prose docs | 2 of 5 | +26% | +32% | −30% ✓ | −5% ✓ | +43% |

**✓ Algebraic docs + z3 must use fewer tokens than Prose docs in most stages, in every run: met**

| Run | Arm | Met | 1 | 2 | 3 | 4 | 5 |
|---|---|---:|---:|---:|---:|---:|---:|
| E022 · gpt-6-sol · medium | **Algebraic docs + z3** | 4 of 5 | −15% ✓ | −16% ✓ | −12% ✓ | +51% | −16% ✓ |
| E023 · gpt-6-luna · medium | **Algebraic docs + z3** | 3 of 5 | −10% ✓ | +102% | −15% ✓ | +75% | −0.4% ✓ |


Each cell is the arm's score minus the other arm's, or its change in tokens or time at that stage. ✓ marks a stage that meets that part of the rule; Met counts them, of the stages with a value.


**Noise.** No two runs here repeat the same setup. In this group's repeated runs, the same arm's score at the same stage moved by a median of 0.03 and at most 0.11.


## Details

### Original prediction and revised quality target

The test card names the arms as follows: `control` is No docs, `semantic` is Prose docs, `algebraic_solver` is Algebraic docs + z3; `total_tokens` is tokens and `elapsed_s` is time.

> **Prediction.** Each design arm uses fewer total_tokens and less elapsed_s than the control in most stages, and its answer correctness is no more than 0.1 below the control's. The algebraic arm uses fewer tokens than the semantic arm.
>
> **Falsifier.** A design arm uses as many or more tokens than the control, or its correctness falls more than 0.1 below the control's. The harness verdict tests only the correctness floor: supported means the arm's score is at most 0.1 below the control's. Tokens and time are compared from the system measurements in the observer.

**Measured:** Each arm's judged `score` at each stage. Quality Δ is the arm's score minus No docs. A stage meets the quality target at +0.1 or above. Every counted check must pass in every run. The retrieval quality target was applied after the runs; their recorded target was −0.1. The scores and token and time measurements are unchanged.


### What went wrong first

In the first run of each experiment, the judge's copy of the workspace left out the design docs, so it marked the design arms' citations as missing:

> The answer cites design docs under ../docs/design/..., which do not exist in the working directory … those citations were scored as nonexistent paths.

I found this in the judge reports, fixed the grader (`c7ac0d7`, "Keep the design tree in the retrieval judge's copy") and repeated both runs. This page counts only the repeats.

### Runs

#### E022 — gpt-6-sol · medium

**Run ID:** `run-20260924T023130Z-ccbee4e6`  
**Started:** 2026-09-24  
**Harness status:** completed

Every arm finished every stage.

#### E023 — gpt-6-luna · medium

**Run ID:** `run-20260924T023152Z-aa033b06`  
**Started:** 2026-09-24  
**Harness status:** completed

Every arm finished every stage.



### Limits

- The two runs used different builder models, so they are not repeats.

### Source data

[View condition `E022-E023` in G001.json](https://mikereese.dev/data/experiments/G001.json). The run IDs above identify the counted runs. See [Data and methods](https://mikereese.dev/experiments/g001/#data-and-methods) for the export method and limits.

