# E020-E026: Seven declarative stages: quality margin unmet; tokens rose in three runs

Condition: Generation · fresh codebase · 7 declarative stages · z3-checked algebra · Result: not supported · 2026-09-24

The prompts here state what must be true, not how to build it. Across three repeat runs, the z3-checked algebra arm scored level with or below No docs and never reached the threshold. It used more tokens than No docs in every run.

## Results at a glance

| Run | Arm | Average score | Stages compared | Tokens | Time | Python CC |
|---|---|---:|---:|---:|---:|---:|
| E020 run 1 | No docs | **0.322** | 6 of 7 | **31.21M** | 1:39:38 | **5.63** |
|  | **Algebraic docs + z3** | 0.292 (−0.030) |  | 36.36M (+17%) | **1:38:00 (−2%)** | 7.64 |

| Run | Arm | Average score | Stages compared | Tokens | Time | Python CC |
|---|---|---:|---:|---:|---:|---:|
| E020 run 2 | No docs | **0.355** | 6 of 7 | **22.03M** | 1:23:43 | **5.71** |
|  | **Algebraic docs + z3** | 0.273 (−0.082) |  | 26.57M (+21%) | **1:21:00 (−3%)** | 6.48 |

| Run | Arm | Average score | Stages compared | Tokens | Time | Python CC |
|---|---|---:|---:|---:|---:|---:|
| E026 | No docs | 0.303 | 6 of 7 | **24.43M** | 1:37:05 | 6.61 |
|  | **Algebraic docs + z3** | **0.308 (+0.005)** |  | 28.14M (+15%) | **1:34:16 (−3%)** | **6.09** |


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. Python CC means the recorded mean cyclomatic complexity of the Python code's functions, classes, and methods at the stage immediately before Rust conversion.


## What changed in this condition

The agent grows the application from an empty repository over seven stages of declarative prompts: each states only what must be true when the stage ends. The last stage converts it to Rust. This condition has no Prose docs arm.

- **No docs** (control): No design method and no starting design. Before coding, it writes its own method, then its designs.
- **Algebraic docs + z3** (hypothesis arm): Algebraic docs, with each charter and proof also as a z3 file, and z3 installed. It must check its algebra with z3 before writing code, and every proof must pass when a stage ends.


**Runs:** 3 (E020 run 1, E020 run 2, E026), repeats of one setup.

**Builder model:** gpt-6-sol · 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. `initial-build`
2. `telemetry-add`
3. `parity-substrate`
4. `process-ontology`
5. `check-no-write`
6. `concurrent-submissions`
7. `rust-conversion`

**✗ Algebraic docs + z3 must 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 | 6 | 7 |
|---|---|---:|---:|---:|---:|---:|---:|---:|---:|
| E020 run 1 | **Algebraic docs + z3** | 0 of 6 | −0.04 | −0.06 | −0.02 | −0.04 | 0.00 | −0.02 | No docs failed |
| E020 run 2 | **Algebraic docs + z3** | 0 of 6 | −0.11 | −0.10 | −0.03 | −0.07 | −0.11 | −0.07 | both failed |
| E026 | **Algebraic docs + z3** | 0 of 6 | +0.09 | 0.00 | 0.00 | 0.00 | 0.00 | −0.06 | both failed |


Each cell is the arm's score minus the other arm's at that stage. ✓ marks a stage that meets that part of the rule; Met counts them, of the stages with a value. “failed” means that arm's grade failed at that stage, so the stage has no score.


**Noise.** Between runs that repeat the same setup, the same arm's score at the same stage moved by a median of 0.05 and at most 0.11, over 12 comparisons; 2 moved by 0.10 or more, the rule's threshold.


## Details

### The prediction, set before the runs

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

> **Prediction.** The algebraic arm's quality score exceeds the semantic arm's by at least 0.1.
>
> **Falsifier.** The algebraic arm's quality score is no higher than the semantic arm's. A positive difference below 0.1 is inconclusive.

**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. A planned comparison with Prose docs could not be measured because that arm did not run.


### z3

| Run | Arm | Last stage | Proof goals | Proved | Disproved | Undecided | Stages the agent ran z3 |
|---|---|---:|---:|---:|---:|---:|---:|
| E020 run 1 | **Algebraic docs + z3** | 7 | 139 | 139 | 0 | 0 | 5 of 7 |
| E020 run 2 | **Algebraic docs + z3** | 7 | 142 | 142 | 0 | 0 | 7 of 7 |
| E026 | **Algebraic docs + z3** | 7 | 159 | 155 | 4 | 0 | 5 of 7 |


After each stage, the system runs z3 on the proof goals in the design's z3 files and counts those it proves, disproves or leaves undecided. The counts are from the last stage that has them; — means none were recorded. The last column counts stages in which the agent itself ran z3. In E026, some goals were still disproved at the last stage.


### Runs

#### E020 run 1 — gpt-6-sol · medium

**Run ID:** `run-20260923T235842Z-4979eeee`  
**Started:** 2026-09-23  
**Harness status:** failed

The No docs arm's grade failed at stage 7 (`rust-conversion`): `cargo test` failed. Every earlier stage was graded.

#### E020 run 2 — gpt-6-sol · medium

**Run ID:** `run-20260924T031833Z-a6b163d1`  
**Started:** 2026-09-24  
**Harness status:** failed

The Algebraic docs + z3 arm's grade failed at stage 7 (`rust-conversion`): `cargo test` failed. The No docs arm's grade failed at stage 7 (`rust-conversion`): `cargo test` failed. Every earlier stage was graded.

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

**Run ID:** `run-20260924T033220Z-8386576e`  
**Started:** 2026-09-24  
**Harness status:** failed

The Algebraic docs + z3 arm's grade failed at stage 7 (`rust-conversion`): `cargo test` failed. The No docs arm's grade failed at stage 7 (`rust-conversion`): `cargo test` failed. Every earlier stage was graded.

The harness marks a run *failed* when any arm's grade fails. That stage has no score for that arm; the run's other stages still count.


### Source data

[View condition `E020-E026` 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.