docs: record authorized runner root filesystem expansion

Reviewed-on: #7

.gitea/workflows/env-probe.yml

@@ -29,3 +29,20 @@ jobs:
           (find / -maxdepth 4 \( -name 'lake-manifest.json' -o -name '.lake' \) -not -path '/proc/*' 2>/dev/null | head -20) || true
           (docker images 2>&1 | head -20) || true
           (docker ps -a 2>&1 | head -10) || true
+      - name: Read-only storage diagnosis
+        run: |
+          set -eu
+          hostname
+          lsblk -e 7 -o NAME,PATH,SIZE,FSTYPE,MOUNTPOINTS
+          findmnt -T /var/lib/docker
+          df -hT / /var/lib/docker
+          docker info --format 'storage={{.Driver}} root={{.DockerRootDir}}'
+          docker system df
+          docker builder du 2>/dev/null || true
+          for dir in /var/lib/docker /var/lib/containerd /opt/lean-cache /var/cache /tmp /var/log; do
+            if [ -d "$dir" ]; then du -xhd1 "$dir" 2>/dev/null || true; fi
+          done
+          for tool in sfdisk growpart resize2fs xfs_growfs; do command -v "$tool" || true; done
+          if [ "$(hostname)" = "iZ6we8b3jgd6nc2qehu06lZ" ] && command -v growpart >/dev/null; then
+            growpart -N /dev/nvme0n1 3 || true
+          fi

.gitea/workflows/runner-storage-maintenance.yml

@@ -0,0 +1,49 @@
+name: runner-storage-maintenance
+
+# Manual-only. Never runs on push or pull_request.
+on:
+  workflow_dispatch:
+    inputs:
+      confirm:
+        description: Enter EXPAND_RUNNER_ROOT after owner approval
+        required: true
+        type: string
+
+jobs:
+  expand-root:
+    if: ${{ github.event_name == 'workflow_dispatch' && inputs.confirm == 'EXPAND_RUNNER_ROOT' }}
+    runs-on: ubuntu24.04-x64-lean4.35
+    timeout-minutes: 20
+    steps:
+      - name: Back up partition table and expand the authorized ext4 root
+        run: |
+          # Owner-authorized manual-only root partition/filesystem expansion.
+          set -euo pipefail
+          exec 9>/var/lock/lean-bench-root-maintenance.lock
+          flock -n 9
+          [ "$(hostname)" = "iZ6we8b3jgd6nc2qehu06lZ" ]
+          [ "$(id -u)" = 0 ]
+          [ "$(blkid -s PARTUUID -o value /dev/nvme0n1p3 | tr A-Z a-z)" = 9b694bad-5bbb-4485-860f-e5544ae47410 ]
+          [ "$(findmnt -n -o SOURCE /)" = /dev/nvme0n1p3 ]
+          [ "$(findmnt -n -o FSTYPE /)" = ext4 ]
+          [ "$(lsblk -n -o START /dev/nvme0n1p3 | tr -d ' ')" = 413696 ]
+          [ "$(blockdev --getsize64 /dev/nvme0n1)" -ge 161061273600 ]
+          backup_dir="/root/lean-bench-maintenance/$(date -u +%Y%m%dT%H%M%SZ)"
+          install -d -m 700 "$backup_dir"
+          sfdisk --dump /dev/nvme0n1 > "$backup_dir/nvme0n1.sfdisk"
+          sync
+          printf 'Partition-table backup: %s\n' "$backup_dir/nvme0n1.sfdisk"
+          set +e
+          growpart -N /dev/nvme0n1 3 > "$backup_dir/growpart-dry-run.log" 2>&1
+          probe_status=$?
+          set -e
+          if [ "$probe_status" = 0 ]; then
+            growpart /dev/nvme0n1 3
+          elif ! grep -q '^NOCHANGE:' "$backup_dir/growpart-dry-run.log"; then
+            cat "$backup_dir/growpart-dry-run.log"
+            exit "$probe_status"
+          fi
+          resize2fs /dev/nvme0n1p3
+          [ "$(lsblk -n -o START /dev/nvme0n1p3 | tr -d ' ')" = 413696 ]
+          lsblk -e 7 -o NAME,PATH,SIZE,FSTYPE,MOUNTPOINTS
+          df -hT / /var/lib/docker

docs/experiments/P0-execution-2026-10-28.md

@@ -1,82 +0,0 @@
-# P0 execution report: 2026-10-28
-
-**Status: blocked by provider billing. No GO, PARTIAL or NO-GO decision.**
-The owner requested delivery of the fixes and this report now, with the remaining paid calls deferred.
-
-## What ran
-
-The owner explicitly authorized sending the 65 textbook passages and corresponding Lean code
-through the existing DashScope endpoint to `qwen-max`, at temperature 0 and a cumulative ceiling
-of 400 HTTP requests. The run issued **131 HTTP requests**. Provider responses accounted for
-**37,699 input tokens and 7,790 output tokens**, 45,489 total. These are recorded token counts,
-not an invoice or a monetary cost estimate. The client counted 89 received model responses;
-a received response is not necessarily a usable detector result.
-
-| Coverage | Count |
-|---|---:|
-| Original cohort | 65 |
-| Items with both detectors complete | 42 |
-| Items with one or both detectors missing | 23 |
-| Successful role-extraction/alignment components | 45 |
-| Successful judge components | 43 |
-| Missing role components | 20 |
-| Missing judge components | 22 |
-| Remaining request reservations | 269 |
-
-DashScope returned HTTP 400 with error code `Arrearage` and its overdue-payment reference.
-The first runner implementation recorded the failures and continued through the cohort, so
-65 saved rows did not mean 65 successful items. The scorer rejected these incomplete outputs.
-No partial-sample gate decision or performance comparison has been produced.
-
-## Inputs and labels
-
-The default `items.jsonl` export omitted `source_text`. All 65 original passages were recovered
-from the matching detection spans and checked byte-for-byte against the archived private
-`review.json`. Item IDs and Lean code were unchanged. The recovery tool also verifies every
-exported field against the archive, normalizing the archive's JSON-encoded imports field.
-Source-inclusive inputs and the regenerated labeling HTML remain in the ignored data directory.
-
-The owner replaced the planned Kimi/human labeling with Codex annotation. All 65 labels were
-frozen before the first detector request. They contain 30 faithful, 25 wrong, 7 minor drift and
-3 not-formalizable verdicts. This is one AI annotator, **not human gold**. The annotator saw the
-detector implementation and aggregate compilation counts, but not per-item compiler outcomes
-or detector outputs. Syntax/proof defects were ignored when the intended semantics were recoverable;
-no compiler or API-name audit was performed. Independent human auditing remains necessary before
-using these labels as evidence for paper-level claims.
-
-## Execution repairs
-
-- Empty passages and mismatched frozen inputs/labels are rejected before paid calls.
-- Each HTTP attempt reserves cumulative budget before sending, including transport and JSON retries.
-  Model, endpoint, temperature, input/label/prompt hashes and cumulative token usage are persisted.
-- Billing/authentication errors now stop immediately, preserving partial results.
-- Resume keeps every successful detector component and retries only missing components. Existing
-  rows are replaced atomically rather than duplicated. A budget stop also preserves completed work
-  within the current item. A lock prevents concurrent writers.
-- `--audit-only` reconciles saved metadata without API calls. It confirmed 42 complete items,
-  23 incomplete items, 42 missing components and 131 already-consumed request reservations.
-- Scoring requires complete results and unchanged frozen-label/result hashes. It restores the
-  preregistered complementary-signal PARTIAL rule and uses wrong versus faithful for primary metrics;
-  minor drift is included as positive only in the secondary comparison.
-- Detector prompts, matching thresholds, the concept table and frozen annotations were not tuned
-  against these outputs. Recovery changes concern transport, persistence and accounting only.
-
-The private first-attempt output and metadata were backed up before reconciliation. The results
-hash and the frozen-label hash did not change during the offline audit.
-
-## Validation and next action
-
-149 offline unit tests passed, including billing-stop and partial-resume regressions; repository-wide
-Ruff and diff checks passed. These checks did not compile Lean or build Docker locally.
-The initial PR revision passed Python tests and real Lean validation on
-`ubuntu24.04-x64-lean4.35`, runner 7, in [CI #427](https://gitea.entroia.com/Zayden-Jung/lean-bench/actions/runs/427).
-The image job was skipped by the PR workflow. The recovery revision's remote result is reported separately in the PR checks.
-
-After the owner confirms billing recovery, resume the existing run with the same inputs, frozen
-labels and cumulative budget. There are 42 missing components; retries may consume more requests.
-Do not change model or prompts to work around the provider block. Only after all 65 items have
-successful outputs should the scorer produce the registered decision and disagreement report.
-Phase 1 has not started.
-
-Tracked audit data: `experiments/P0-pilot/results/execution.json` (counts and hashes only).
-Private raw files: `experiments/P0-pilot/data/` (gitignored).

docs/experiments/P0-gpt-diagnostic.md

@@ -0,0 +1,127 @@
+# P0: full-cohort GPT-assisted diagnostic (2026-10-28)
+
+**All 65 items have a fresh source-role description, a fresh semantic judgment and a
+completed deterministic alignment. This is a same-assistant diagnostic, not an independent
+benchmark or a completion of the preregistered Qwen gate. No gate decision is issued.**
+
+## Scope and provenance
+
+The owner requested that the current GPT assistant reassess the entire cohort after the
+Qwen run was interrupted by provider billing failures. Every item was reviewed again;
+no Qwen detector output was reused, and the incomplete Qwen run was not patched with GPT
+outputs. The earlier labels and Qwen files remain unchanged in the original worktree.
+This branch starts at main `5d531c9` and does not depend on the separate billing-recovery PR.
+
+The source-role structures and four-way judgments were authored directly by the assistant
+in this chat, frozen before computing the new alignment statistics, and replayed by an
+offline script. They were not responses obtained through a GPT API endpoint. The exact
+deployed model identifier, temperature and chat token usage are unavailable; they are not
+invented. There were **zero new external model API calls** for this diagnostic, and no
+DashScope credential was loaded.
+
+The assistant had already seen the earlier labels, Lean code, detector implementation and
+aggregate compilation statistics. It also viewed passages and Lean together during this
+review. Thus the source descriptions are **not a blinded source-only extraction** and the
+new judgments are **not independent of the reference labels**. Reading only a passage when
+writing a role does not remove prior context exposure. Syntax and proof defects are
+separated from recoverable semantic meaning; no new Lean compilation or library API audit
+was performed. An independent human review remains necessary for research claims.
+
+## Results for all 65 items
+
+| Fresh semantic judgment | Items |
+|---|---:|
+| Faithful | 25 |
+| Minor drift | 13 |
+| Wrong | 24 |
+| Not formalizable from the extracted specification | 3 |
+| Total | 65 |
+
+The strict binary assistant judge flags every verdict except faithful. The full four-way
+judgment, error categories and an individual explanation are retained for every item.
+Explanations and role descriptions are private because they paraphrase the source passages.
+
+The unchanged deterministic role matcher flagged **55/65** items. It flagged all **24**
+items newly judged wrong, but also **16/25** newly judged faithful. These are comparisons
+between dependent components of the same diagnostic, not an independently measured recall
+or false-positive rate. They identify an over-sensitive diagnostic behavior worth auditing.
+
+Common conflict categories across all items include missing objects (41 items), degenerate
+projections (15), goal mismatch (15), missing hypotheses (14), extra hypotheses (13),
+quantifier conflicts (7) and type conflicts (5). Categories overlap. In particular, a named
+source quantity can be computed inline in Lean, a product representation can replace an
+abstract isomorphic group, and a bundled type can encode conditions without separate
+binders. The current lexical matcher does not establish equivalence of those representations.
+These are hypotheses for a later matcher audit, not measured causal explanations for every flag.
+No matching threshold, concept table or authored assessment was changed after the scores
+were inspected.
+
+## Relation to the frozen earlier AI labels
+
+The fresh four-way judgments agree with **59/65** earlier labels. Six changed:
+
+| Blind ID | Earlier AI label | Fresh judgment |
+|---|---|---|
+| P02 | Faithful | Minor drift |
+| P18 | Faithful | Minor drift |
+| P23 | Faithful | Minor drift |
+| P34 | Faithful | Minor drift |
+| P51 | Faithful | Minor drift |
+| P57 | Wrong | Minor drift |
+
+The six changes concern representation, type/scope and coverage judgments. They demonstrate
+annotation instability and should be independently adjudicated, not silently overwritten.
+The 59/65 agreement is **not an accuracy estimate**.
+
+For debugging continuity, the summary contains confusion counts and Wilson intervals against
+the frozen earlier AI labels. The primary comparison excludes earlier minor-drift and
+not-formalizable labels (55 items); the secondary comparison includes minor drift as positive
+(62 items). These tables are explicitly named `reference_agreement`. They cannot establish
+that GPT or role alignment outperforms Qwen. The Qwen coverage is incomplete and this pass
+has different provenance and no independent ground truth. `decision` is null; no GO,
+PARTIAL or NO-GO is computed.
+
+## Artifacts and replay
+
+Tracked, text-free artifacts:
+
+- `experiments/P0-pilot/results/gpt-diagnostic-summary.json`: provenance, input/assessment/code
+  hashes, distributions, fixed matching thresholds and non-independent agreement statistics.
+- `experiments/P0-pilot/results/gpt-diagnostic-items.json`: all 65 blind IDs, verdicts, error
+  categories, compile flags, role scores and conflict categories; no passages or explanations.
+- `experiments/P0-pilot/assistant_diagnostic.py`: validates authored inputs and replays the
+  existing projection, lint, alignment and statistics code offline.
+- `tests/test_assistant_diagnostic.py`: completeness, identity, schema, offline replay and
+  public-output privacy regressions using synthetic text.
+
+Private artifacts under the gitignored `experiments/P0-pilot/data/gpt-diagnostic/`:
+
+- `items.jsonl`: source-inclusive copy of the unchanged cohort.
+- `assistant-assessments.json`: all newly authored source structures and judgments, frozen
+  before alignment statistics were inspected.
+- `results.jsonl`: complete replay outputs for the 65 items.
+- `review.html`: local, self-contained per-item source/Lean/reason/role/alignment review.
+- `original-hashes.json`: snapshot of the earlier Qwen files and reference labels for
+  verifying that this work did not change them.
+
+Run from the repository root with the private files present:
+
+```sh
+PYTHONPATH=. python3 experiments/P0-pilot/assistant_diagnostic.py \
+  --items experiments/P0-pilot/data/gpt-diagnostic/items.jsonl \
+  --key experiments/P0-pilot/labels/key.json \
+  --assessments experiments/P0-pilot/data/gpt-diagnostic/assistant-assessments.json \
+  --labels experiments/P0-pilot/labels/labels.json \
+  --private-out experiments/P0-pilot/data/gpt-diagnostic \
+  --summary experiments/P0-pilot/results/gpt-diagnostic-summary.json \
+  --public-items experiments/P0-pilot/results/gpt-diagnostic-items.json
+```
+
+The replay is deterministic; it does not regenerate GPT judgments, call a model, or compile
+Lean. Without the private assessment file, public readers can inspect the categorical
+results but cannot reconstruct the authored descriptions and explanations from hashes.
+
+152 offline unit tests, repository-wide Ruff and diff checks passed locally without a Lean
+or Docker build. Remote Python and real Lean verification use the owner-confirmed
+`ubuntu24.04-x64-lean4.35` tag; the delivered PR records their current status. The existing
+PR workflow skips the Docker image job. No Phase 1 work has started.

docs/experiments/P0-pilot.md

@@ -2,11 +2,7 @@
 
 Experiment ID **P0**, Phase 0. Registry and conventions: [README.md](README.md).
 
-Status: **approved 2026-10-22; 65 AI labels frozen 2026-10-28; detector run blocked by DashScope Arrearage after 131 requests. 42 items are complete, 23 need missing detector components. No gate decision has been issued.**
+Status: **approved 2026-10-22; 65 AI labels frozen 2026-10-28; detector execution pending explicit data-transfer approval. No pilot API request has been sent.**
-
-The owner explicitly authorized sending the 65 passages and Lean code to DashScope/qwen-max,
-then requested fixes and an execution report now, with paid recovery calls deferred.
-Execution report: [P0 execution, 2026-10-28](P0-execution-2026-10-28.md).
 
 Owner amendment (2026-10-28, in the execution chat): Codex now handles preparation,
 annotation, detector execution and reporting; Kimi's participation is no longer required.

docs/infrastructure/runner-lean435.md

@@ -3,7 +3,7 @@
 Gitea runner `iZ6we8b3jgd6nc2qehu06lZ` (act_runner v5.2.0, runner id 7), label `ubuntu24.04-x64-lean4.35`. Both `lean-bench` and `lean-agent` CI run here; the old `gitea-cicd-server-for-CODEX` label is no longer used.
 
 ## The host
-- Jobs run **on the host, not in a container**, as root. Ubuntu 24.04.5, kernel 6.8, 4 CPU, 15 GiB RAM, no swap, 99 GB disk (88 GB free at setup).
+- Jobs run **on the host, not in a container**, as root. Ubuntu 24.04.5, kernel 6.8, 4 CPU, 15 GiB RAM, no swap, 150 GiB system disk (expanded from 100 GiB on 2026-10-28); the ext4 root filesystem reports about 148 GiB, with 75 GiB available immediately after expansion.
 - Lean 4.35.0 via elan 4.2.4 in `/root/.elan`. Python 3.12.3, git 2.43, gcc 13.3, curl, jq.
 - **No Node**, so `actions/checkout` and other JavaScript actions cannot run. Workflows clone with `git fetch --depth 1 origin $SHA` using `${{ github.token }}`.
 - Docker was not installed; the lean-bench `image` job installs `docker.io` + `docker-buildx` (Docker 29.1.3) if missing.
@@ -20,3 +20,30 @@ Gitea runner `iZ6we8b3jgd6nc2qehu06lZ` (act_runner v5.2.0, runner id 7), label `
 - Mathlib's post-update hook runs the cache fetch **inside `lake update`**, so retries placed after it never run. Set `MATHLIB_NO_CACHE_ON_UPDATE=1` for `lake update` and fetch in a retry loop. In the image the archives live in a BuildKit cache mount (`/root/.cache/mathlib`), so a retried build resumes.
 - Cold image build about 19 min; with layers cached about 2 min.
 - Gitea 1.26.1 has no cancel-run API; a person cancels in the web UI, then the API can `DELETE` the finished run. The Actions logs endpoint needs a token; the runs/jobs status endpoints work anonymously on this public repo.
+
+## Root capacity expansion (2026-10-28)
+
+The owner expanded the cloud disk to 150 GiB, but root partition `/dev/nvme0n1p3`
+and its ext4 filesystem still occupied about 100 GiB. CI run number 43 (API run ID 438)
+therefore continued to report 28 GiB available and failed its unchanged 30 GiB preflight.
+Rerunning a failed job retains the same UI run number; its job attempt number increments.
+
+Read-only probe run number 45 (API run ID 442) confirmed the raw-disk/partition mismatch.
+Its `growpart -N` output showed that partition 3 could extend from 209301471 to
+314159071 sectors while keeping start sector 413696 and its partition UUID unchanged.
+Temporary files and logs were small; Docker/containerd storage and Mathlib were the main
+consumers. No tagged image, build cache or Mathlib cache was deleted for this repair.
+
+The owner explicitly authorized partition and filesystem expansion in the execution chat.
+Manual maintenance run number 46 (API run ID 443) then backed up the partition table to
+`/root/lean-bench-maintenance/20261028T121919Z/nvme0n1.sfdisk`, expanded partition 3,
+and grew the mounted ext4 filesystem online. The resulting partition is 149.8 GiB;
+`df` reported a 148 GiB filesystem with 75 GiB available. No reboot was required.
+
+`.gitea/workflows/env-probe.yml` now includes read-only storage and cache diagnostics.
+`.gitea/workflows/runner-storage-maintenance.yml` is manual-only and requires the literal
+confirmation `EXPAND_RUNNER_ROOT`. It validates hostname, root device, ext4 type, partition
+UUID, start sector and disk size, takes a lock, and backs up the partition table before any
+change. Future execution still requires explicit owner authorization for that maintenance.
+It never formats a device or prunes images. The failed image job was retried after expansion;
+its actual build, smoke-test and image-retention outcome is recorded in CI run number 43.

experiments/P0-pilot/README.md

@@ -44,9 +44,6 @@ Labeling must be finished before anyone opens `results.jsonl`.
 - Metadata is stored beside the output as `results.meta.json`. Model, endpoint, temperature,
   input hash, frozen-label hash and prompt hashes must match on resume. Usage is cumulative.
   A file lock prevents concurrent writers. A budget stop returns exit status 2.
-- Billing/authentication failures stop immediately. Resume retries only missing detector components,
-  keeping both complete items and the successful side of partial items. Rows are replaced atomically.
-  `--audit-only` reconciles saved completion counts and status without any API request.
 - The nominal successful path uses 130 calls (one source extraction and one judge per item);
   malformed replies and network retries may increase the actual count.
 - Scoring requires complete labels and results and no unresolved detector errors. The primary
@@ -56,10 +53,15 @@ Labeling must be finished before anyone opens `results.jsonl`.
 - Raw passages, labeling HTML and model responses remain in the ignored `data/` directory.
   Only verdicts, abstract annotation notes, hashes and text-free summaries belong in Git.
 
-## Current execution
+## Separate GPT-assisted diagnostic
 
-The 2026-10-28 run was blocked by DashScope `Arrearage`: 42 items are complete, 23 need
+The owner requested a complete 65-item reassessment by the current GPT assistant on
-42 detector components, and 131 of the 400 request reservations have been consumed.
+2026-10-28. This is separate from the incomplete Qwen run: no outputs are mixed and
-The owner requested fixes and a report now, with paid resumption deferred.
+neither the earlier labels nor Qwen files are overwritten. The assistant had prior
-See `docs/experiments/P0-execution-2026-10-28.md` and `results/execution.json`.
+exposure to the reference labels and Lean; this is not blind or independent validation.
-No gate decision has been issued. Restore provider billing before resuming the same run.
+No GO/PARTIAL/NO-GO decision is issued.
+
+See `docs/experiments/P0-gpt-diagnostic.md` for all counts, limitations, artifact locations
+and the offline replay command. The tracked `results/gpt-diagnostic-*.json` files contain
+only categorical/numeric outputs and audit metadata. The authored source structures,
+reasons and full review page stay in the ignored `data/gpt-diagnostic/` directory.

experiments/P0-pilot/assistant_diagnostic.py

@@ -0,0 +1,200 @@
+"""Validate and replay a current-chat assistant review without calling any model.
+
+Private source schemas and reasons stay in data/. Public summaries contain only
+categories, counts, numeric scores, hashes and an explicit non-independent provenance.
+"""
+from __future__ import annotations
+
+import argparse
+import hashlib
+import html
+import json
+import math
+from collections import Counter
+from pathlib import Path
+
+from leanbench.align import DEFAULT_THRESHOLD, GOAL_THRESHOLD, align
+from leanbench.evalstats import auc, confusion, wilson
+from leanbench.lint import lint
+from leanbench.project import project
+from leanbench.srcsimplex import parse_source_simplex
+
+VERDICTS = {"faithful", "minor_drift", "wrong", "not_formalizable"}
+ERRORS = {"missing_hypothesis", "extra_hypothesis", "wrong_type", "quantifier",
+          "wrong_conclusion", "degenerate", "hallucinated_api", "other"}
+
+
+def digest(path: Path) -> str:
+    return hashlib.sha256(path.read_bytes()).hexdigest()
+
+
+def finite(value):
+    if isinstance(value, dict):
+        return {k: finite(v) for k, v in value.items()}
+    if isinstance(value, (list, tuple)):
+        return [finite(v) for v in value]
+    if isinstance(value, float) and not math.isfinite(value):
+        return None
+    return value
+
+
+def unique(rows, field):
+    indexed = {row[field]: row for row in rows}
+    if len(indexed) != len(rows):
+        raise ValueError(f"Duplicate {field}")
+    return indexed
+
+
+def evaluate(items, key, assessment):
+    """Keep model-authored assessments separate from deterministic detector outputs."""
+    by_id = unique(items, "id")
+    records = unique(assessment["records"], "blind_id")
+    if (not key or len(set(key.values())) != len(key) or set(records) != set(key)
+            or set(by_id) != set(key.values())):
+        raise ValueError("Items, key and assessments must cover the same cohort exactly once")
+    output = []
+    for blind, item_id in key.items():
+        item, record = by_id[item_id], records[blind]
+        if record["id"] != item_id or not item.get("source_text", "").strip():
+            raise ValueError(f"Missing source text or mismatched item for {blind}")
+        judge = record["judge"]
+        if (judge.get("verdict") not in VERDICTS or type(judge.get("faithful")) is not bool
+                or judge["faithful"] != (judge["verdict"] == "faithful")
+                or not isinstance(judge.get("reason"), str) or not judge["reason"].strip()
+                or not isinstance(judge.get("errors"), list)
+                or not set(judge["errors"]) <= ERRORS):
+            raise ValueError(f"Invalid authored judgment for {blind}")
+        source = parse_source_simplex(record["source"])
+        projection = project(item["lean_code"])
+        alignment = align(source, projection)
+        output.append({"id": item_id, "blind_id": blind,
+                       "source": source.as_dict(), "judge": judge,
+                       "projection": projection.as_dict(), "role": alignment.as_dict(),
+                       "lint": lint(projection), "compiled": bool(item.get("verified")),
+                       "errors": {}})
+    return output
+
+
+def public_items(rows, labels):
+    if set(labels) != {row["blind_id"] for row in rows}:
+        raise ValueError("Reference labels must cover the entire cohort")
+    out = []
+    for row in rows:
+        reference = labels[row["blind_id"]]["verdict"]
+        if reference not in VERDICTS:
+            raise ValueError("Invalid reference verdict")
+        out.append({"blind_id": row["blind_id"], "reference_verdict": reference,
+                    "assistant_verdict": row["judge"]["verdict"],
+                    "assistant_error_types": row["judge"]["errors"],
+                    "verdict_agrees": reference == row["judge"]["verdict"],
+                    "compiled": row["compiled"], "lint_flagged": bool(row["lint"]),
+                    "role_flagged": row["role"]["flagged"],
+                    "role_score": row["role"]["score"],
+                    "role_conflict_types": row["role"]["errors"],
+                    "source_role_count": len(row["source"]["roles"]),
+                    "lean_role_count": len(row["projection"]["roles"]),
+                    "degenerate_projection": row["projection"]["degenerate"]})
+    return out
+
+
+def agreement(rows, labels, secondary=False):
+    cohort = [r for r in rows if labels[r["blind_id"]]["verdict"] != "not_formalizable"
+              and (secondary or labels[r["blind_id"]]["verdict"] != "minor_drift")]
+    positives = {"wrong", "minor_drift"} if secondary else {"wrong"}
+    target = [labels[r["blind_id"]]["verdict"] in positives for r in cohort]
+    out = {}
+    for name, flags in {
+        "role": [r["role"]["flagged"] for r in cohort],
+        "assistant_judge": [not r["judge"]["faithful"] for r in cohort],
+        "lint": [bool(r["lint"]) for r in cohort],
+        "compile_only": [not r["compiled"] for r in cohort],
+    }.items():
+        counts = confusion(flags, target)
+        out[name] = {**counts.as_dict(), "precision_ci": wilson(counts.tp, counts.tp + counts.fp)}
+    out["role"]["auc"] = auc([-r["role"]["score"] for r in cohort], target)
+    return {"n": len(cohort), "metrics_are_non_independent_reference_agreement": True,
+            "detectors": out}
+
+
+def write_review(path, rows, items):
+    by_id = {r["id"]: r for r in items}
+    sections = []
+    for row in rows:
+        item = by_id[row["id"]]
+        sections.append(
+            f'<section id="{html.escape(row["blind_id"])}"><h2>{row["blind_id"]}</h2>'
+            f'<h3>Passage</h3><pre>{html.escape(item["source_text"])}</pre>'
+            f'<h3>Lean</h3><pre>{html.escape(item["lean_code"])}</pre>'
+            f'<h3>Fresh assistant judgment: {row["judge"]["verdict"]}</h3>'
+            f'<p>{html.escape(row["judge"]["reason"])}</p>'
+            f'<h3>Source roles</h3><pre>{html.escape(json.dumps(row["source"], indent=2, ensure_ascii=False))}</pre>'
+            f'<h3>Deterministic alignment</h3><pre>{html.escape(json.dumps(row["role"], indent=2, ensure_ascii=False))}</pre></section>'
+        )
+    path.write_text('<!doctype html><html lang="en"><meta charset="utf-8">'
+                    '<title>P0 GPT-assisted diagnostic</title><style>'
+                    'body{font:16px/1.6 system-ui;max-width:1050px;margin:32px auto;padding:0 20px}'
+                    'pre{white-space:pre-wrap;overflow-wrap:anywhere;background:#f4f5f6;padding:16px}'
+                    'section{border-top:1px solid #ccc;margin:40px 0}</style>'
+                    '<h1>P0: 65-item GPT-assisted diagnostic</h1>'
+                    '<p>Private review. Same-assistant, non-blind diagnosis; no independent accuracy or gate decision. '
+                    'Passages and model-derived descriptions must remain outside Git.</p>'
+                    + ''.join(sections) + '</html>', encoding="utf-8")
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("--items", type=Path, required=True)
+    parser.add_argument("--key", type=Path, required=True)
+    parser.add_argument("--assessments", type=Path, required=True)
+    parser.add_argument("--labels", type=Path, required=True)
+    parser.add_argument("--private-out", type=Path, required=True)
+    parser.add_argument("--summary", type=Path, required=True)
+    parser.add_argument("--public-items", type=Path, required=True)
+    args = parser.parse_args()
+    if "data" not in args.private_out.parts:
+        parser.error("Private output must be under the gitignored data/ directory")
+    items = [json.loads(x) for x in args.items.read_text().splitlines() if x.strip()]
+    key = json.loads(args.key.read_text())["key"]
+    assessment = json.loads(args.assessments.read_text())
+    provenance = assessment["provenance"]
+    if (provenance["items_sha256"] != digest(args.items)
+            or provenance["key_sha256"] != digest(args.key)):
+        parser.error("Authored review is bound to different inputs or blind key")
+    rows = evaluate(items, key, assessment)
+    labels = json.loads(args.labels.read_text())["labels"]
+    public = public_items(rows, labels)
+    summary = {
+        "experiment": "P0-GPT-diagnostic", "status": "complete", "n": len(rows),
+        "provenance": provenance, "decision": None,
+        "decision_withheld_reason": "Same-assistant, non-blind diagnostic; not the preregistered Qwen pilot or independent ground-truth validation.",
+        "hashes": {"items": digest(args.items), "key": digest(args.key),
+                   "assessments": digest(args.assessments), "reference_labels": digest(args.labels),
+                   "replay_script": digest(Path(__file__)),
+                   **{f"leanbench/{name}.py": digest(Path(__file__).resolve().parents[2] / "leanbench" / f"{name}.py")
+                      for name in ("align", "project", "srcsimplex", "lint")}},
+        "fixed_thresholds": {"matching": DEFAULT_THRESHOLD, "goal": GOAL_THRESHOLD},
+        "verdict_counts": dict(Counter(r["judge"]["verdict"] for r in rows)),
+        "role_flagged": sum(r["role"]["flagged"] for r in rows),
+        "lint_flagged": sum(bool(r["lint"]) for r in rows),
+        "compiled": sum(r["compiled"] for r in rows),
+        "degenerate_projection": sum(r["projection"]["degenerate"] for r in rows),
+        "exact_verdict_agreement": sum(r["verdict_agrees"] for r in public),
+        "changed_verdicts": [r["blind_id"] for r in public if not r["verdict_agrees"]],
+        "primary_reference_agreement": agreement(rows, labels),
+        "secondary_reference_agreement": agreement(rows, labels, secondary=True),
+        "role_flagged_by_new_verdict": {v: {"n": sum(r["judge"]["verdict"] == v for r in rows),
+             "flagged": sum(r["judge"]["verdict"] == v and r["role"]["flagged"] for r in rows)}
+             for v in sorted(VERDICTS)},
+    }
+    args.private_out.mkdir(parents=True, exist_ok=True)
+    (args.private_out / "results.jsonl").write_text(''.join(json.dumps(r, ensure_ascii=False) + '\n' for r in rows))
+    write_review(args.private_out / "review.html", rows, items)
+    args.summary.parent.mkdir(parents=True, exist_ok=True)
+    args.public_items.parent.mkdir(parents=True, exist_ok=True)
+    args.summary.write_text(json.dumps(finite(summary), indent=2, allow_nan=False) + '\n')
+    args.public_items.write_text(json.dumps(public, indent=2, allow_nan=False) + '\n')
+    print(json.dumps({k: summary[k] for k in ("n", "status", "verdict_counts", "role_flagged", "exact_verdict_agreement", "decision")}))
+
+
+if __name__ == "__main__":
+    main()

experiments/P0-pilot/results/execution.json

@@ -1,71 +0,0 @@
-{
-  "experiment": "P0",
-  "status": "provider_blocked",
-  "decision": null,
-  "decision_withheld_reason": "Incomplete detector outputs after DashScope Arrearage; no GO/PARTIAL/NO-GO is valid.",
-  "cohort_size": 65,
-  "completed_items": 42,
-  "items_with_failures": 23,
-  "missing_components": {
-    "judge": 22,
-    "role": 20
-  },
-  "request_attempts": 131,
-  "max_calls": 400,
-  "remaining_request_budget": 269,
-  "usage": {
-    "calls": 89,
-    "prompt_tokens": 37699,
-    "completion_tokens": 7790
-  },
-  "model": "qwen-max",
-  "temperature": 0.0,
-  "items_sha256": "487ecd22919a5e3b0174a2846ab8fe7c0daf4d3feccccf8ea6571aec04c41bed",
-  "labels_sha256": "1552dba85e75426799151384e7e28c9a0b1072ed4c862df0876df89920d2a638",
-  "results_sha256": "fce402e6eab460a48bb9a8e94140bb23f305843ab46d227bbffa5100d7de69e5",
-  "prompt_hashes": {
-    "source": "382f9a7b5a0cfb2d50d525f884dc806f45adaa59bcc45e388920c4759db1546f",
-    "judge": "7ab92682bd71d78a212471289f0f01db39d6b68f49d44df65d7b1c9e34ebb5e2"
-  },
-  "labels": {
-    "type": "single AI annotator; not human gold",
-    "frozen": true,
-    "count": 65
-  },
-  "affected_blind_ids": [
-    "P02",
-    "P04",
-    "P09",
-    "P18",
-    "P19",
-    "P20",
-    "P21",
-    "P22",
-    "P24",
-    "P27",
-    "P29",
-    "P30",
-    "P33",
-    "P36",
-    "P37",
-    "P38",
-    "P42",
-    "P43",
-    "P45",
-    "P47",
-    "P54",
-    "P59",
-    "P62"
-  ],
-  "successful_components_preserved": 88,
-  "resume_policy": "After owner confirms billing recovery, retry missing components only using the same run files, frozen labels, model, prompts and cumulative 400-request ceiling.",
-  "owner_instruction": "2026-10-28: complete fixes and the execution report now; resume paid calls later.",
-  "validation": {
-    "offline_unit_tests": 149,
-    "ruff": "passed",
-    "remote_runner_tag": "ubuntu24.04-x64-lean4.35",
-    "initial_remote_ci": "https://gitea.entroia.com/Zayden-Jung/lean-bench/actions/runs/427",
-    "initial_remote_ci_status": "success; image job skipped for PR",
-    "recovery_remote_ci": "See follow-up PR #6 checks for the delivered head revision"
-  }
-}

experiments/P0-pilot/results/gpt-diagnostic-summary.json

@@ -0,0 +1,275 @@
+{
+  "experiment": "P0-GPT-diagnostic",
+  "status": "complete",
+  "n": 65,
+  "provenance": {
+    "run_kind": "current-chat assistant-authored diagnostic; not an API benchmark",
+    "evaluator": "Codex GPT assistant; exact deployed model identifier unavailable",
+    "authored_at": "2026-10-28T11:23:06.275167+00:00",
+    "items_sha256": "487ecd22919a5e3b0174a2846ab8fe7c0daf4d3feccccf8ea6571aec04c41bed",
+    "key_sha256": "f827cac92ee4e907554fadcc7c0e006ef2b829350f74e7f8b54ca11945e62836",
+    "reference_labels_seen_in_prior_chat": true,
+    "lean_seen_while_authoring_source_roles": true,
+    "new_external_api_calls": 0,
+    "assistant_token_usage": null,
+    "limitations": [
+      "Same assistant previously authored the reference labels; agreement is not independent accuracy.",
+      "Prior context contains the earlier review and detector code. This is not a blinded source-only extraction or a fresh-model replicate.",
+      "All judgments are manually authored in this chat, not responses from a GPT API endpoint.",
+      "Semantics are assessed conditionally on recoverable notation. No new Lean compilation or library API audit is performed.",
+      "The strict Boolean judge flags all verdicts except faithful, including not_formalizable; four-way verdicts are also retained."
+    ]
+  },
+  "decision": null,
+  "decision_withheld_reason": "Same-assistant, non-blind diagnostic; not the preregistered Qwen pilot or independent ground-truth validation.",
+  "hashes": {
+    "items": "487ecd22919a5e3b0174a2846ab8fe7c0daf4d3feccccf8ea6571aec04c41bed",
+    "key": "f827cac92ee4e907554fadcc7c0e006ef2b829350f74e7f8b54ca11945e62836",
+    "assessments": "f12735802ba0d4d94b776a91581a13a508eab0ce90ba8973a6c9c4e4d1390272",
+    "reference_labels": "1552dba85e75426799151384e7e28c9a0b1072ed4c862df0876df89920d2a638",
+    "replay_script": "5c02e3d26761ce0b4e38d4be9e65b95bfd8db048c9c7c73edaac17e654e10c0f",
+    "leanbench/align.py": "730e44f1158e6e441e4745dff7324e565b89b6e5148017c3fd93f4c69c22c9ce",
+    "leanbench/project.py": "8ed76924b463ba418ceb732d0fcb6c572a548d94fe7f23759c67746da24d9430",
+    "leanbench/srcsimplex.py": "d10b785299ceb17cadc4e97737eef74183ed390d04b4571a702cd4fd42b069d0",
+    "leanbench/lint.py": "4396e879312f370cd70beeffcbd7ffeab8a41ee1704cc1f235dbbcd6e843fd68"
+  },
+  "fixed_thresholds": {
+    "matching": 0.3,
+    "goal": 0.2
+  },
+  "verdict_counts": {
+    "faithful": 25,
+    "minor_drift": 13,
+    "wrong": 24,
+    "not_formalizable": 3
+  },
+  "role_flagged": 55,
+  "lint_flagged": 21,
+  "compiled": 10,
+  "degenerate_projection": 15,
+  "exact_verdict_agreement": 59,
+  "changed_verdicts": [
+    "P02",
+    "P18",
+    "P23",
+    "P34",
+    "P51",
+    "P57"
+  ],
+  "primary_reference_agreement": {
+    "n": 55,
+    "metrics_are_non_independent_reference_agreement": true,
+    "detectors": {
+      "role": {
+        "tp": 25,
+        "fp": 21,
+        "fn": 0,
+        "tn": 9,
+        "n": 55,
+        "recall": 1.0,
+        "precision": 0.5434782608695652,
+        "false_flag_rate": 0.7,
+        "f1": 0.704225352112676,
+        "recall_ci": [
+          0.8668035060468213,
+          1.0
+        ],
+        "false_flag_ci": [
+          0.5212387898833981,
+          0.8333543735604105
+        ],
+        "precision_ci": [
+          0.4017993496608042,
+          0.67845489578878
+        ],
+        "auc": 0.61
+      },
+      "assistant_judge": {
+        "tp": 25,
+        "fp": 5,
+        "fn": 0,
+        "tn": 25,
+        "n": 55,
+        "recall": 1.0,
+        "precision": 0.8333333333333334,
+        "false_flag_rate": 0.16666666666666666,
+        "f1": 0.9090909090909091,
+        "recall_ci": [
+          0.8668035060468213,
+          1.0
+        ],
+        "false_flag_ci": [
+          0.07336434240351683,
+          0.33564705185680177
+        ],
+        "precision_ci": [
+          0.6643529481431982,
+          0.9266356575964831
+        ]
+      },
+      "lint": {
+        "tp": 12,
+        "fp": 5,
+        "fn": 13,
+        "tn": 25,
+        "n": 55,
+        "recall": 0.48,
+        "precision": 0.7058823529411765,
+        "false_flag_rate": 0.16666666666666666,
+        "f1": 0.5714285714285713,
+        "recall_ci": [
+          0.30031003928960015,
+          0.6650178204685269
+        ],
+        "false_flag_ci": [
+          0.07336434240351683,
+          0.33564705185680177
+        ],
+        "precision_ci": [
+          0.468664666737861,
+          0.8672020613444361
+        ]
+      },
+      "compile_only": {
+        "tp": 24,
+        "fp": 24,
+        "fn": 1,
+        "tn": 6,
+        "n": 55,
+        "recall": 0.96,
+        "precision": 0.5,
+        "false_flag_rate": 0.8,
+        "f1": 0.6575342465753424,
+        "recall_ci": [
+          0.8045552759497747,
+          0.9929039496133008
+        ],
+        "false_flag_ci": [
+          0.6269395261897256,
+          0.9049502189759876
+        ],
+        "precision_ci": [
+          0.36389098932037767,
+          0.6361090106796223
+        ]
+      }
+    }
+  },
+  "secondary_reference_agreement": {
+    "n": 62,
+    "metrics_are_non_independent_reference_agreement": true,
+    "detectors": {
+      "role": {
+        "tp": 32,
+        "fp": 21,
+        "fn": 0,
+        "tn": 9,
+        "n": 62,
+        "recall": 1.0,
+        "precision": 0.6037735849056604,
+        "false_flag_rate": 0.7,
+        "f1": 0.7529411764705882,
+        "recall_ci": [
+          0.8928172849426366,
+          1.0
+        ],
+        "false_flag_ci": [
+          0.5212387898833981,
+          0.8333543735604105
+        ],
+        "precision_ci": [
+          0.4694123578888073,
+          0.7241078808096105
+        ],
+        "auc": 0.590625
+      },
+      "assistant_judge": {
+        "tp": 32,
+        "fp": 5,
+        "fn": 0,
+        "tn": 25,
+        "n": 62,
+        "recall": 1.0,
+        "precision": 0.8648648648648649,
+        "false_flag_rate": 0.16666666666666666,
+        "f1": 0.927536231884058,
+        "recall_ci": [
+          0.8928172849426366,
+          1.0
+        ],
+        "false_flag_ci": [
+          0.07336434240351683,
+          0.33564705185680177
+        ],
+        "precision_ci": [
+          0.7202227252929444,
+          0.9408679273749238
+        ]
+      },
+      "lint": {
+        "tp": 14,
+        "fp": 5,
+        "fn": 18,
+        "tn": 25,
+        "n": 62,
+        "recall": 0.4375,
+        "precision": 0.7368421052631579,
+        "false_flag_rate": 0.16666666666666666,
+        "f1": 0.5490196078431372,
+        "recall_ci": [
+          0.2816508596944317,
+          0.6067469796877387
+        ],
+        "false_flag_ci": [
+          0.07336434240351683,
+          0.33564705185680177
+        ],
+        "precision_ci": [
+          0.5120803155892935,
+          0.8819376166045982
+        ]
+      },
+      "compile_only": {
+        "tp": 29,
+        "fp": 24,
+        "fn": 3,
+        "tn": 6,
+        "n": 62,
+        "recall": 0.90625,
+        "precision": 0.5471698113207547,
+        "false_flag_rate": 0.8,
+        "f1": 0.6823529411764705,
+        "recall_ci": [
+          0.7578150066422116,
+          0.9675990373736805
+        ],
+        "false_flag_ci": [
+          0.6269395261897256,
+          0.9049502189759876
+        ],
+        "precision_ci": [
+          0.41453742646439184,
+          0.6734263183985253
+        ]
+      }
+    }
+  },
+  "role_flagged_by_new_verdict": {
+    "faithful": {
+      "n": 25,
+      "flagged": 16
+    },
+    "minor_drift": {
+      "n": 13,
+      "flagged": 13
+    },
+    "not_formalizable": {
+      "n": 3,
+      "flagged": 2
+    },
+    "wrong": {
+      "n": 24,
+      "flagged": 24
+    }
+  }
+}

experiments/P0-pilot/run_pilot.py

@@ -50,64 +50,37 @@ def judge(client, passage: str, lean: str) -> dict:
             "reason": str(reply.get("reason", ""))[:300]}
 
 
-def provider_blocked(error: Exception) -> bool:
+def run_item(client, item: dict) -> dict:
-    text = str(error).lower()
+    if not item.get("source_text", "").strip():
-    return any(code in text for code in ("arrearage", "overdue-payment", "invalid_api_key", "http 401", "http 403"))
+        raise ValueError("Missing source_text; use a private source-inclusive export")
-
+    code = item.get("lean_code") or ""
-
+    row: dict = {"id": item["id"], "compiled": bool(item.get("verified")), "errors": {}}
-def complete_row(row: dict) -> bool:
+    proj = project(code)
-    return not row.get("errors") and "role" in row and "judge" in row
+    row["projection"] = proj.as_dict()
-
+    row["lint"] = lint(proj)
-
+    try:
-class ProviderBlocked(RuntimeError):
+        src = srcsimplex.extract_source_simplex(client, item.get("source_text", ""),
-    """A billing or authentication failure requires external recovery before resuming."""
+                                                item.get("label", ""))
-
+        al = align(src, proj)
-    def __init__(self, row):
+        row["source"] = [r.__dict__ for r in src.roles]
-        super().__init__("Provider billing/authentication blocked; partial results were preserved")
+        row["role"] = al.as_dict()
-        self.row = row
+    except CallBudgetExceeded:
+        raise
+    except Exception as error:  # a failed extraction is data, not a crash
+        row["errors"]["role"] = str(error)[:300]
+    try:
+        row["judge"] = judge(client, item.get("source_text", ""), code)
+    except CallBudgetExceeded:
+        raise
+    except Exception as error:
+        row["errors"]["judge"] = str(error)[:300]
+    return row
 
 
 class CallBudgetExceeded(RuntimeError):
     """Stop before issuing a request that would exceed the cumulative budget."""
 
 
-def run_item(client, item: dict, previous: dict | None = None) -> dict:
-    if not item.get("source_text", "").strip():
-        raise ValueError("Missing source_text; use a private source-inclusive export")
-    code = item.get("lean_code") or ""
-    row: dict = {**(previous or {}), "id": item["id"], "compiled": bool(item.get("verified"))}
-    row["errors"] = dict(row.get("errors", {}))
-    proj = project(code)
-    row["projection"] = proj.as_dict()
-    row["lint"] = lint(proj)
-    if "role" not in row:
-        try:
-            src = srcsimplex.extract_source_simplex(client, item["source_text"], item.get("label", ""))
-            al = align(src, proj)
-            row["source"] = [r.__dict__ for r in src.roles]
-            row["role"] = al.as_dict()
-            row["errors"].pop("role", None)
-        except CallBudgetExceeded as error:
-            error.row = row
-            raise
-        except Exception as error:
-            row["errors"]["role"] = str(error)[:300]
-            if provider_blocked(error):
-                raise ProviderBlocked(row) from error
-    if "judge" not in row:
-        try:
-            row["judge"] = judge(client, item["source_text"], code)
-            row["errors"].pop("judge", None)
-        except CallBudgetExceeded as error:
-            error.row = row
-            raise
-        except Exception as error:
-            row["errors"]["judge"] = str(error)[:300]
-            if provider_blocked(error):
-                raise ProviderBlocked(row) from error
-    return row
-
-
 def digest(path: Path) -> str:
     return hashlib.sha256(path.read_bytes()).hexdigest()
 
@@ -133,9 +106,8 @@ def execute(args, items, settings) -> int:
     if args.out.exists():
         rows = [json.loads(x) for x in args.out.read_text(encoding="utf-8").splitlines() if x.strip()]
     ids = {item["id"] for item in items}
-    by_id = {row["id"]: row for row in rows}
+    done = {row["id"] for row in rows}
-    done = {row["id"] for row in rows if complete_row(row)}
+    if len(done) != len(rows) or not done <= ids:
-    if len(by_id) != len(rows) or not set(by_id) <= ids:
         raise ValueError("Results have duplicate or unknown item IDs")
     hashes = {
         "source": hashlib.sha256((srcsimplex.SYSTEM_PROMPT + inspect.getsource(srcsimplex.passage_prompt)).encode()).hexdigest(),
@@ -157,24 +129,11 @@ def execute(args, items, settings) -> int:
     elif rows:
         raise ValueError("Cannot resume results without their audit metadata")
     todo = [item for item in items if item["id"] not in done]
-    missing = sum(2 - int("role" in by_id.get(i["id"], {}))
-                  - int("judge" in by_id.get(i["id"], {})) for i in todo)
     print(f"items={len(items)} done={len(done)} todo={len(todo)} model={settings.llm.model} "
-          f"missing_components={missing} request_attempts={meta['request_attempts']} cap={args.max_calls}")
+          f"nominal_calls={len(todo) * 2} request_attempts={meta['request_attempts']} cap={args.max_calls}")
     print("prompt_hashes:", json.dumps(hashes))
     if args.dry_run:
         return 0
-    if getattr(args, "audit_only", False):
-        meta["completed_items"] = len(done)
-        meta["processed_items"] = len(rows)
-        meta["status"] = ("provider_blocked" if any(provider_blocked(RuntimeError(message))
-                          for row in rows for message in row.get("errors", {}).values())
-                          else "detector_errors" if todo else "complete")
-        if args.out.exists():
-            meta["results_sha256"] = digest(args.out)
-        atomic_json(meta_path, meta)
-        print(json.dumps(meta))
-        return 0 if meta["status"] == "complete" else 2
     if settings.llm.model != "qwen-max" or settings.llm.temperature != 0:
         raise ValueError("P0 is preregistered for qwen-max at temperature 0")
     client = AuditedClient.from_settings(settings.llm)
@@ -183,7 +142,6 @@ def execute(args, items, settings) -> int:
     def checkpoint():
         meta["usage"] = client.usage.as_dict()
         meta["completed_items"] = len(done)
-        meta["processed_items"] = len(by_id)
         atomic_json(meta_path, meta)
 
     def reserve():
@@ -197,30 +155,19 @@ def execute(args, items, settings) -> int:
     meta["max_calls"] = args.max_calls
     meta["status"] = "running"
     checkpoint()
-    def save_row(row):
-        by_id[row["id"]] = row
-        if complete_row(row):
-            done.add(row["id"])
-        temporary = args.out.with_suffix(args.out.suffix + ".tmp")
-        with temporary.open("w", encoding="utf-8") as stream:
-            for item in items:
-                if item["id"] in by_id:
-                    stream.write(json.dumps(by_id[item["id"]], ensure_ascii=False) + "\n")
-            stream.flush()
-            os.fsync(stream.fileno())
-        os.replace(temporary, args.out)
-        checkpoint()
-
     try:
-        for item in todo:
+        with args.out.open("a", encoding="utf-8") as stream:
-            row = run_item(client, item, by_id.get(item["id"]))
+            for item in todo:
-            save_row(row)
+                row = run_item(client, item)
-            print(f"completed={len(done)}/{len(items)} requests={meta['request_attempts']}", flush=True)
+                stream.write(json.dumps(row, ensure_ascii=False) + "\n")
-        meta["status"] = "complete" if len(done) == len(items) else "detector_errors"
+                stream.flush()
-    except (CallBudgetExceeded, ProviderBlocked) as error:
+                os.fsync(stream.fileno())
-        if getattr(error, "row", None) is not None:
+                done.add(item["id"])
-            save_row(error.row)
+                checkpoint()
-        meta["status"] = "provider_blocked" if isinstance(error, ProviderBlocked) else "budget_exhausted"
+                print(f"completed={len(done)}/{len(items)} requests={meta['request_attempts']}", flush=True)
+        meta["status"] = "complete"
+    except CallBudgetExceeded as error:
+        meta["status"] = "budget_exhausted"
         print(str(error), file=sys.stderr)
     except BaseException:
         meta["status"] = "interrupted"
@@ -239,7 +186,6 @@ def main() -> int:
     ap.add_argument("--out", required=True, type=Path)
     ap.add_argument("--max-calls", type=int, default=400)
     ap.add_argument("--dry-run", action="store_true")
-    ap.add_argument("--audit-only", action="store_true", help="Reconcile saved state without making API calls")
     ap.add_argument("--labels", type=Path, help="Frozen labels; their hash is bound to the run")
     args = ap.parse_args()
     if not 1 <= args.max_calls <= 400:

tests/test_assistant_diagnostic.py

@@ -0,0 +1,74 @@
+"""Current-chat review replay is offline, complete and text-free at its public boundary."""
+import copy
+import importlib.util
+from pathlib import Path
+
+import pytest
+
+PATH = Path(__file__).resolve().parents[1] / "experiments/P0-pilot/assistant_diagnostic.py"
+SPEC = importlib.util.spec_from_file_location("assistant_diagnostic", PATH)
+DIAG = importlib.util.module_from_spec(SPEC)
+SPEC.loader.exec_module(DIAG)
+
+ITEM = {"id": "synthetic", "source_text": "Synthetic private prose.",
+        "lean_code": "theorem t (n : Nat) : n = n := rfl", "verified": True}
+ASSESSMENT = {"records": [{"id": "synthetic", "blind_id": "P01", "source": {
+    "roles": [{"kind": "object", "symbols": ["n"], "description": "Private object wording",
+               "keywords": ["natural"]},
+              {"kind": "goal", "description": "Private goal wording", "keywords": ["equal"]}],
+    "goal_has_exists": False},
+    "judge": {"verdict": "faithful", "faithful": True, "errors": [],
+              "reason": "Private reviewer explanation"}}]}
+
+
+def test_offline_replay_and_text_free_public_output(monkeypatch):
+    def no_network(*args, **kwargs):
+        raise AssertionError("Replay must not call an API")
+
+    monkeypatch.setattr("urllib.request.urlopen", no_network)
+    rows = DIAG.evaluate([ITEM], {"P01": "synthetic"}, ASSESSMENT)
+    assert len(rows) == 1 and rows[0]["errors"] == {}
+    public = DIAG.public_items(rows, {"P01": {"verdict": "faithful"}})
+    assert public[0]["assistant_verdict"] == "faithful"
+    assert not any(word in str(public) for word in ["Private", "Synthetic", "explanation"])
+    assert all(key not in public[0] for key in ["source", "judge", "reason", "lean_code", "source_text"])
+
+
+def test_duplicate_or_missing_assessments_are_rejected():
+    assessment = copy.deepcopy(ASSESSMENT)
+    assessment["records"] *= 2
+    with pytest.raises(ValueError, match="Duplicate"):
+        DIAG.evaluate([ITEM], {"P01": "synthetic"}, assessment)
+    with pytest.raises(ValueError, match="same cohort"):
+        DIAG.evaluate([ITEM], {"P01": "synthetic"}, {"records": []})
+
+
+def test_mismatched_item_and_missing_source_are_rejected():
+    assessment = copy.deepcopy(ASSESSMENT)
+    assessment["records"][0]["id"] = "different"
+    with pytest.raises(ValueError, match="mismatched"):
+        DIAG.evaluate([ITEM], {"P01": "synthetic"}, assessment)
+    with pytest.raises(ValueError, match="Missing source"):
+        DIAG.evaluate([{**ITEM, "source_text": ""}], {"P01": "synthetic"}, ASSESSMENT)
+
+
+def test_judge_cannot_disagree_with_its_boolean_flag():
+    assessment = copy.deepcopy(ASSESSMENT)
+    assessment["records"][0]["judge"]["faithful"] = False
+    with pytest.raises(ValueError, match="Invalid authored judgment"):
+        DIAG.evaluate([ITEM], {"P01": "synthetic"}, assessment)
+
+
+def test_invalid_source_schema_is_rejected():
+    assessment = copy.deepcopy(ASSESSMENT)
+    assessment["records"][0]["source"]["roles"] = []
+    with pytest.raises(ValueError, match="goal"):
+        DIAG.evaluate([ITEM], {"P01": "synthetic"}, assessment)
+
+
+def test_agreement_is_explicitly_not_independent_and_has_no_gate():
+    rows = DIAG.evaluate([ITEM], {"P01": "synthetic"}, ASSESSMENT)
+    result = DIAG.agreement(rows, {"P01": {"verdict": "faithful"}})
+    assert result["metrics_are_non_independent_reference_agreement"] is True
+    assert "decision" not in result
+    assert DIAG.finite(float("nan")) is None

tests/test_pilot_scripts.py

@@ -141,82 +141,3 @@ def test_judge_rejects_string_boolean():
     rp = load("run_pilot")
     with pytest.raises(ValueError, match="unusable judge"):
         rp.judge(ScriptedClient(['{"faithful": "false"}']), "passage", "code")
-
-
-def test_partial_resume_keeps_successful_detector_output():
-    rp = load("run_pilot")
-    row = rp.run_item(Stub(), ITEM)
-    expected_role = row["role"]
-    row.pop("judge")
-    row["errors"]["judge"] = "temporary failure"
-
-    class JudgeOnly:
-        calls = 0
-
-        def complete_json(self, messages):
-            self.calls += 1
-            assert "faithful" in messages[0]["content"]
-            return {"faithful": True}
-
-    client = JudgeOnly()
-    resumed = rp.run_item(client, ITEM, row)
-    assert client.calls == 1
-    assert resumed["role"] == expected_role
-    assert rp.complete_row(resumed)
-    assert row["errors"] == {"judge": "temporary failure"}
-
-
-def test_billing_failure_stops_before_next_detector():
-    import pytest
-
-    from leanbench.llm import LLMError
-
-    rp = load("run_pilot")
-
-    class Blocked:
-        calls = 0
-
-        def complete_json(self, messages):
-            self.calls += 1
-            raise LLMError("HTTP 400: Arrearage overdue-payment")
-
-    client = Blocked()
-    with pytest.raises(rp.ProviderBlocked) as caught:
-        rp.run_item(client, ITEM)
-    assert client.calls == 1
-    assert "role" in caught.value.row["errors"]
-    assert "judge" not in caught.value.row["errors"]
-
-
-def test_blocked_run_preserves_and_replaces_partial_row(tmp_path, monkeypatch):
-    import argparse
-    import json
-
-    from leanbench.config import Settings
-
-    rp = load("run_pilot")
-    args = argparse.Namespace(items=tmp_path / "items.jsonl", out=tmp_path / "results.jsonl",
-                              max_calls=400, dry_run=False)
-    args.items.write_text(json.dumps(ITEM) + "\n")
-    partial = {"id": "x1", "compiled": True, "role": {"flagged": False},
-               "errors": {"judge": "Arrearage"}}
-
-    def blocked(client, item, previous):
-        raise rp.ProviderBlocked(partial)
-
-    monkeypatch.setattr(rp, "run_item", blocked)
-    assert rp.execute(args, [ITEM], Settings()) == 2
-    meta = json.loads(args.out.with_suffix(".meta.json").read_text())
-    assert meta["status"] == "provider_blocked"
-    assert meta["completed_items"] == 0
-
-    def recover(client, item, previous):
-        assert previous["role"] == partial["role"]
-        return {**previous, "judge": {"faithful": True}, "errors": {}}
-
-    monkeypatch.setattr(rp, "run_item", recover)
-    assert rp.execute(args, [ITEM], Settings()) == 0
-    rows = [json.loads(line) for line in args.out.read_text().splitlines()]
-    assert len(rows) == 1 and rp.complete_row(rows[0])
-    meta = json.loads(args.out.with_suffix(".meta.json").read_text())
-    assert meta["completed_items"] == 1 and meta["status"] == "complete"