Merge pull request 'ci: 仅 main 分支执行 CI/CD' (#10) from codex/main-only-cicd into main

Reviewed-on: #10

.gitea/workflows/ci.yml

@@ -11,8 +11,7 @@ name: ci
 
 on:
   push:
-    branches: [main, "ci/**"]
-  pull_request:
+    branches: [main]
   workflow_dispatch:
 
 env:
@@ -20,6 +19,7 @@ env:
 
 jobs:
   python:
+    if: gitea.ref == 'refs/heads/main'
     runs-on: ubuntu24.04-x64-lean4.35
     timeout-minutes: 20
     steps:
@@ -50,6 +50,7 @@ jobs:
           .venv/bin/lean-bench doctor --skip-llm --env /dev/null
 
   lean:
+    if: gitea.ref == 'refs/heads/main'
     needs: python
     runs-on: ubuntu24.04-x64-lean4.35
     timeout-minutes: 150
@@ -82,7 +83,7 @@ jobs:
 
   image:
     needs: [python, lean]
-    if: github.event_name != 'pull_request'
+    if: ${{ gitea.ref == 'refs/heads/main' && (github.event_name != 'pull_request') }}
     runs-on: ubuntu24.04-x64-lean4.35
     timeout-minutes: 180
     steps:

.gitea/workflows/env-probe.yml

@@ -2,13 +2,14 @@ name: env-probe
 
 on:
   push:
-    branches: ["ci/**"]
+    branches: [main]
     paths:
       - ".gitea/workflows/env-probe.yml"
   workflow_dispatch:
 
 jobs:
   probe:
+    if: gitea.ref == 'refs/heads/main'
     runs-on: ubuntu24.04-x64-lean4.35
     timeout-minutes: 15
     steps:
@@ -29,3 +30,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-probe.yml

@@ -10,6 +10,7 @@ on:
 
 jobs:
   probe:
+    if: gitea.ref == 'refs/heads/main'
     runs-on: gitea-cicd-server-for-CODEX
     timeout-minutes: 10
     steps:

.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: ${{ gitea.ref == 'refs/heads/main' && (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

README.md

@@ -276,6 +276,12 @@ Experiments have IDs (`P0`, `E0`-`E11`); the registry, phases, gates and convent
 [`docs/experiments/README.md`](docs/experiments/README.md). CI runner and environment notes:
 [`docs/infrastructure/runner-lean435.md`](docs/infrastructure/runner-lean435.md).
 
+Browse the [65-item semantic simplex schema review](docs/reviews/simplex-schemas.html)
+by opening that HTML file in a browser after cloning, or downloading it from Git.
+It shows role schemas and Lean signature expressions; textbook passages and full assistant
+judgment explanations remain private. The [schema design and replay instructions](docs/simplex-schema.md)
+explain how the page is generated and which annotations still need review.
+
 ## What this does not claim
 
 Lean says whether the code is *legal*, and — when there is a proof — whether it is
@@ -285,4 +291,5 @@ well-formed statement of the wrong theorem passes every check here. `confidence`
 possible; spot-check before trusting a dataset.
 
 Source books are not committed. `.gitignore` keeps PDFs and extracted text out of
-the repository; only code and the short Lean datasets belong in git.
+the repository. The tracked schema review contains semantic annotations and Lean signatures,
+while source-inclusive inputs remain in the ignored data directory.

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

@@ -0,0 +1,84 @@
+# 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 passed [CI #433](https://gitea.entroia.com/Zayden-Jung/lean-bench/actions/runs/433).
+The recovery changes from PR #6 are consolidated with the semantic schema and review page
+in PR #9; the combined head is checked separately there.
+
+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,7 +2,22 @@
 
 Experiment ID **P0**, Phase 0. Registry and conventions: [README.md](README.md).
 
-Status: **approved 2026-10-22; labels pending. No detector has been run and no API spend has occurred.**
+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.**
+
+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.
+The frozen labels are from one AI annotator, **not human ground truth**. The annotator saw
+the detector implementation and aggregate compile counts before labeling, but did not see
+per-item compiler outcomes or detector outputs. This departs from the original labeling plan;
+any resulting decision is provisional and cannot substitute for an independent human audit.
+Decision thresholds, detector prompts and the concept table remain fixed. Implementation
+repairs before the first paid call restore the complementary-signal PARTIAL rule, exclude
+minor drift from the primary wrong-versus-faithful comparison, enforce the cumulative HTTP
+request budget, and persist run identity and usage. See `experiments/P0-pilot/README.md`.
 Written 2026-10-22. Companion to `docs/research-plan.md` (what and why), `docs/TODO.md` (task list), `docs/acl-2027-bar.md` (bar). Target: ACL 2027 via ARR, deadline 4 Jan 2027 AoE.
 
 ## 1. Decision (approved by the owner on 2026-10-22)

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.

docs/research-plan.md

@@ -8,9 +8,15 @@ Evidence base: repo README and code (`leanbench/`, 4,345 lines incl. tests), pro
 
 ## 0. The idea in one page
 
+**Terminology clarification (2026-10-28).** The owner uses "simplex" for a semantic,
+multi-role relation schema: one statement joins objects, assumptions and a conclusion.
+It does not mean a geometric simplex or assert a mathematical simplicial complex.
+See [the implemented schema design](simplex-schema.md) for scoped slots, storage and
+candidate retrieval. Existing signature projections and AI source annotations remain partial.
+
 **Simplex, as it exists in the archived code.**
 - `Role(name, context, choices)`: a named semantic slot with a description and an optional closed set of allowed values (`is_constrained`, `validate_value`).
-- `Simplex(name, roles: {alias: Role})`: a reusable unit of **at least two** roles. A Simplex is itself a `Role`, so simplices nest; nesting gives a *simplicial complex*. `Equivalence` is the two-role special case.
+- `Simplex(name, roles: {alias: Role})`: a reusable unit of **at least two** roles. A Simplex is itself a `Role`, so explicitly supplied schemas can be nested as semantic composition. `Equivalence` is the two-role special case.
 - `State` / `Fact` / `Goal`: a role plus a value. A `Fact` has a value, a `Goal` does not; `SolvingTask.is_completed()` is "every goal resolved".
 - `SchemaRegistry` (SQLite): `set_role`, `set_simplex`, `search_roles`, `find_by_roles(known_roles)`, `find_solvable(known_role_names)`.
 - `SchemaParserAgent`: turns a query into a Simplex through a forced tool call whose JSON schema says `minItems: 2`, with a **search-first, reuse-before-create** rule for roles. `AnalogySchemaMiner`: proposes new simplices by the ratio *Simplex B : Role B :: Simplex A : Role A*.
@@ -19,11 +25,11 @@ Evidence base: repo README and code (`leanbench/`, 4,345 lines incl. tests), pro
 
 | Lean | Simplex view |
 |---|---|
-| `(G : Type*) [Group G]` | role `G`, `context` = "carrier", `choices` = admissible type/class constraints |
+| `(G : Type*) [Group G]` | role `G`, `context` = "carrier", type/class constraints as attributes; `choices` only for explicit finite value sets |
 | `(h : P x)` hypothesis | `Fact` role |
 | conclusion after the final `:` | `Goal` role |
 | `def` / `structure` being introduced | `own` role (what the thing *is*) |
-| a lemma used inside a proof | nested simplex (edge in the complex) |
+| a lemma used inside a proof | explicit nested schema reference (when recorded) |
 
 `leanbench/typeindex.py` already extracts exactly this split: `input` (binders and hypotheses), `goal` (the conclusion), `own` (definitions). So the type index is a simplex index in all but name. The new work is to make it a **first-class schema that steers inference** instead of a passive index.
 

docs/simplex-schema.md

@@ -0,0 +1,170 @@
+# Simplex schema: a semantic relation joining roles
+
+Here **simplex** means the owner's multi-role relation pattern: one statement relates
+objects, assumptions and a conclusion. The implementation does not construct geometric
+simplices, faces, boundaries or a mathematical simplicial complex.
+
+## The model
+
+| Concept | Representation | Meaning |
+|---|---|---|
+| Reusable role definition | `Role` | A semantic slot type with optional textual type/context and finite `choices` |
+| Statement/relation pattern | `Simplex` | A named mapping from at least two local aliases to roles |
+| Object or assumption supplied by a caller | `Fact` | A role plus a non-None value |
+| Requested result | `Goal` | A role whose value is not supplied yet |
+| Application to particular objects | `SimplexInstance` | Facts and goals bound by local slot alias |
+| Explicit composition | A `Simplex` used as a role | A supplied nested pattern; no proof dependency is discovered automatically |
+| Persistent catalog | `SchemaRegistry` | JSON/SQLite nodes and alias-to-definition references |
+
+`kind` separates `object`, `fact`, `goal`, `own` and nested `simplex` roles.
+A role's `attrs.references` may name other aliases in the same simplex; unknown aliases
+are rejected. These references can describe the objects mentioned in an assumption or
+conclusion. They are not geometric edges. Their provenance must distinguish manually
+supplied relationships from incomplete syntactic candidates.
+
+`type_text` is descriptive Lean/mathematical text, not an executable type checker.
+`choices` is a finite set of admissible values, not a replacement for arbitrary Lean typeclass
+constraints. Supplied fact and resolved goal values are checked against explicit choices.
+No registry method establishes that a string is a proof or that a mathematical premise is true.
+
+## Concrete example: two groups and a homomorphism
+
+One schema joins these slots:
+
+| Local alias | Role | Type/claim | References |
+|---|---|---|---|
+| `left` | object | group carrier | none |
+| `right` | object | group carrier | none |
+| `map` | object | `left →* right` | left, right |
+| `bijective` | fact | `Bijective map` | map |
+| `goal` | goal | `Nonempty (left ≃* right)` | left, right |
+
+The simplex is this complete relation pattern, not an individual role or an asserted
+geometric object. `left` and `right` may explicitly reuse the same `role:group` definition
+while binding to different group objects. Reusing a role definition does not equate their values.
+
+Run the synthetic, offline example:
+
+```sh
+PYTHONPATH=. python3 examples/simplex_registry.py
+```
+
+It binds symbolic caller values for the input slots, leaves the goal unresolved, and returns
+a structurally ready candidate. It does not run a Lean proof.
+
+## Scope, persistence and reuse
+
+`SchemaRegistry.set_simplex` assigns every child a scoped key by default:
+`<schema-key>/slot/<escaped-alias>`. Thus `G` in one theorem is not the same object as `G`
+in another. Corpus keys also include the frozen annotation hash and item identity.
+
+To reuse a definition, register it with `set_role` and explicitly pass a `role_keys` mapping
+to `set_simplex`. The referenced definition must match the supplied role exactly. A shared
+definition still has distinct occurrence keys for every alias. No role is semantically merged
+merely because its spelling, type text or keywords resemble another role.
+
+Keys are immutable within a registry. Identical registration is idempotent; changed content
+or changed definition references require a new version key. `get_role` and `get_simplex`
+resolve exact keys, not ambiguous bare names. `search_roles` returns literal-substring candidates
+for a caller to review; it does not approve semantic reuse.
+
+Serialization includes names, kinds, context, types, choices, attributes and nested aliases.
+`role_from_dict` restores JSON snapshots. SQLite uses one connection and one transaction per
+nested registration, foreign keys and JSON payloads; it does not load archived pickle blobs.
+Cyclic nesting and failed reuse checks roll back the complete write. Returned objects are
+restored snapshots; changing one does not silently update a registered definition.
+
+## Query and binding APIs
+
+```python
+from leanbench.schema_registry import SchemaRegistry, slot_key
+
+with SchemaRegistry("private-registry.sqlite") as registry:
+    schema = registry.get_simplex("schema:example")
+    matches = registry.search_roles("group")
+    containers = registry.find_by_roles(["role:group"], match_all=True)
+    candidates = registry.find_solvable([
+        slot_key("schema:example", "left"),
+        slot_key("schema:example", "right"),
+        slot_key("schema:example", "map"),
+        slot_key("schema:example", "bijective"),
+    ])
+```
+
+`find_by_roles` searches definition references, including descendants of nested schemas.
+`find_solvable` retains the archived API name but implements **structural readiness only**:
+all input occurrences must be supplied and at least one marked goal/own occurrence must
+remain unresolved. It returns `structural_candidate_only: true`, not a proof or a computed value.
+Having one `role:group` definition cannot satisfy two distinct group slots. A nested input
+must itself be explicitly supplied; the registry does not apply its internal theorem automatically.
+
+`SimplexInstance(schema, facts=..., goals=...)` binds local aliases. Facts and goals must be
+distinct declared slots. Omitting `goals` uses roles marked `goal` or `own`; `resolve` checks
+a supplied goal value against choices. Completion means that declared goals have values,
+not that Lean verified them. Value unification, dependent type checking and proof search
+remain outside this implementation.
+
+## Materialization of the 65 P0 items
+
+The builder consumes the frozen current-chat GPT diagnostic's source descriptions and
+unchanged Lean strings. It makes no model request, revises no assessment and performs no
+Lean compilation. Results:
+
+| Artifact | Count |
+|---|---:|
+| Source annotation seed schemas | 65 |
+| Lean signature schema seeds | 50 |
+| Items with fewer than two projected Lean roles | 15 |
+| Stored schemas | 115 |
+| Scoped role records / slot occurrences | 483 / 483 |
+
+These 115 seeds deliberately do not auto-reuse definitions across statements. Explicit reuse
+is supported and tested by the synthetic example; a reviewed shared ontology is future work.
+The 15 incomplete Lean sides remain in the index with status `insufficient_projected_roles`.
+A closed declaration may mention concrete objects inside its conclusion that the binder-based
+projector misses. No object roles were invented to hide this limitation.
+
+Source schemas are marked `unreviewed_annotation_seed`. Existing `given` tags are preserved
+with `quantifier_status: unreviewed`; they are not silently converted to universal/existential
+quantifiers. References on the source side use explicit symbol candidates; Lean references
+are syntactic identifier candidates. Neither is a complete dependency analysis.
+For example, P11's source seed lists a named size while Lean uses `Fintype.card G` inline.
+The materializer preserves both representations; it does not invent a validated cardinality
+binding or repair the old alignment result. Annotation quality and semantic normalization
+still require a separate review.
+
+Private outputs under `experiments/P0-pilot/data/simplex-schemas-v1/`:
+
+- `registry.sqlite`: queryable catalog with the 115 schemas and scoped slots.
+- `schemas.json`: all 65 source/Lean pairs, retaining incomplete Lean projections.
+- `schemas.html`: a local generated copy of the schema-only review tracked below.
+- `schema-inputs.json`: input hashes; an existing directory rejects changed inputs.
+
+Tracked outputs:
+
+- `experiments/P0-pilot/results/simplex-schema-index.json`: 65 item IDs, schema keys,
+  role counts, coverage status and reference-candidate counts.
+- `experiments/P0-pilot/results/simplex-schema-summary.json`: coverage, limitations and hashes.
+- [65-item schema review](reviews/simplex-schemas.html): an owner-approved, self-contained
+  HTML view of all 65 source/Lean pairs. It includes schema role descriptions and Lean
+  signature expressions, but no textbook paragraphs or full assistant judgment explanations.
+  Open the file in a browser after cloning, or download it from the repository; the Git web
+  interface may display HTML source instead of rendering it. The JSON indexes above remain
+  text-free counts/keys. Full source-inclusive inputs and assessment files remain gitignored.
+
+Replay from the repository root with private inputs present:
+
+```sh
+PYTHONPATH=. python3 experiments/P0-pilot/build_schemas.py \
+  --items experiments/P0-pilot/data/simplex-schemas-v1/items.jsonl \
+  --assessments experiments/P0-pilot/data/simplex-schemas-v1/assistant-assessments.json \
+  --key experiments/P0-pilot/labels/key.json \
+  --private-out experiments/P0-pilot/data/simplex-schemas-v1 \
+  --index experiments/P0-pilot/results/simplex-schema-index.json \
+  --summary experiments/P0-pilot/results/simplex-schema-summary.json \
+  --review-page docs/reviews/simplex-schemas.html
+```
+
+The original annotations, judgments, Qwen results and matcher thresholds remain unchanged.
+The registry is a usable schema foundation, not evidence of a validated theorem, a working
+prover, independently measured faithfulness, or a completed Phase 1 experiment.

examples/simplex_registry.py

@@ -0,0 +1,35 @@
+"""Synthetic example: one isomorphism schema relates two groups and a map."""
+from __future__ import annotations
+
+import json
+
+from leanbench.schema import KIND_FACT, KIND_GOAL, Role, Simplex, SimplexInstance
+from leanbench.schema_registry import SchemaRegistry, slot_key
+
+
+def example():
+    group = Role("group", type_text="group carrier", context="Reusable group role definition")
+    schema = Simplex("group_isomorphism", {
+        "left": group,
+        "right": group,
+        "map": Role("homomorphism", type_text="left →* right",
+                    attrs={"references": ["left", "right"]}),
+        "bijective": Role("bijective", KIND_FACT, type_text="Bijective map",
+                          attrs={"references": ["map"]}),
+        "goal": Role("isomorphic", KIND_GOAL, type_text="Nonempty (left ≃* right)",
+                     attrs={"references": ["left", "right"]}),
+    }, context="A bijective homomorphism supplies a group isomorphism")
+    with SchemaRegistry() as registry:
+        registry.set_role(group, "role:group")
+        key = registry.set_simplex(schema, role_keys={"left": "role:group", "right": "role:group"})
+        instance = SimplexInstance(schema, facts={
+            "left": "group A", "right": "group B", "map": "f", "bijective": "supplied evidence"})
+        candidates = registry.find_solvable([slot_key(key, alias) for alias in instance.facts])
+        return {"schema": registry.get_simplex(key).as_dict(), "definition_keys": registry.slots(key),
+                "bindings": {alias: fact.value for alias, fact in instance.facts.items()},
+                "structural_candidates": candidates, "completed": instance.is_completed(),
+                "note": "Evidence is symbolic user input; this example does not run a Lean proof."}
+
+
+if __name__ == "__main__":
+    print(json.dumps(example(), indent=2, ensure_ascii=False))

experiments/P0-pilot/README.md

@@ -16,16 +16,78 @@ unfaithful formalizations better than a single LLM judge, compile-only, or stati
 
 ## Steps
 
-    cp runs/p85-110/items.jsonl experiments/P0-pilot/data/items.jsonl
+    # Default exports omit source_text. Restore it from the matching private review.
+    python experiments/P0-pilot/prepare_items.py --items runs/p85-110/items.jsonl \
+        --review runs/p85-110/review.json --out experiments/P0-pilot/data/items.jsonl
     python experiments/P0-pilot/make_sheet.py --items experiments/P0-pilot/data/items.jsonl \
         --out experiments/P0-pilot/data --key-dir experiments/P0-pilot/labels --seed 7
     # a person opens data/labelsheet.html, labels all 65 items, downloads labels.json into labels/
     python experiments/P0-pilot/run_pilot.py --items experiments/P0-pilot/data/items.jsonl \
         --out experiments/P0-pilot/data/results.jsonl --dry-run
     python experiments/P0-pilot/run_pilot.py --items experiments/P0-pilot/data/items.jsonl \
-        --out experiments/P0-pilot/data/results.jsonl
+        --out experiments/P0-pilot/data/results.jsonl --labels experiments/P0-pilot/labels/labels.json
     python experiments/P0-pilot/score.py --results experiments/P0-pilot/data/results.jsonl \
         --labels experiments/P0-pilot/labels/labels.json --key experiments/P0-pilot/labels/key.json \
         --summary experiments/P0-pilot/results/summary.json
 
 Labeling must be finished before anyone opens `results.jsonl`.
+
+## Execution safeguards
+
+- Every item must have a nonempty source passage. `prepare_items.py` restores passages only
+  when all exported fields match the archived review; the exported cohort and Lean code stay intact.
+- Freeze all labels before the paid run. The owner changed the labeler to the Codex assistant
+  on 2026-10-28. These are **AI labels, not human gold**; see the metadata in `labels/labels.json`.
+- `--max-calls` counts actual HTTP attempts, including transport and JSON retries, cumulatively
+  across resumes. The hard ceiling is 400. A reservation is saved before each request; an interrupted
+  request may consume a reservation without a known response or token count.
+- 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
+  comparison is wrong versus faithful; minor drift is included as positive in the secondary analysis.
+  The complementary-signal PARTIAL rule counts wrong items flagged by role alignment but missed
+  by the judge. No threshold, concept table or detector prompt was tuned for these labels.
+- Raw passages, labeling HTML and model responses remain in the ignored `data/` directory.
+  Verdicts, abstract annotation notes, hashes and text-free summaries belong in Git;
+  the owner-approved schema-only HTML review is also tracked separately under docs/reviews/.
+
+## Qwen execution snapshot
+
+The 2026-10-28 run was blocked by DashScope `Arrearage`: 42 items are complete, 23 need
+42 detector components, and 131 of the 400 request reservations have been consumed.
+The owner requested fixes and a report now, with paid resumption deferred.
+See `docs/experiments/P0-execution-2026-10-28.md` and `results/execution.json`.
+No gate decision has been issued. Restore provider billing before resuming the same run.
+
+## Separate GPT-assisted diagnostic
+
+The owner requested a complete 65-item reassessment by the current GPT assistant on
+2026-10-28. This is separate from the incomplete Qwen run: no outputs are mixed and
+neither the earlier labels nor Qwen files are overwritten. The assistant had prior
+exposure to the reference labels and Lean; this is not blind or independent validation.
+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.
+
+## Semantic simplex registry
+
+The current 65-item annotation cohort is materialized as multi-role relation schemas:
+65 source seeds, 50 Lean signature seeds and 15 explicitly incomplete Lean projections.
+See `docs/simplex-schema.md` for the data model, scoped identities, explicit role reuse,
+structural candidate queries, bindings and replay command. Private SQLite/JSON/HTML outputs
+stay under `data/simplex-schemas-v1/`; tracked `results/simplex-schema-*.json` files contain
+only counts, opaque keys, provenance hashes and coverage status. This does not change the
+frozen diagnostic or claim complete semantic extraction or proof verification.
+
+The owner-approved schema-only HTML review is tracked at
+`docs/reviews/simplex-schemas.html`. Regenerate it with the builder's `--review-page` option;
+the raw inputs, full assessment explanations and SQLite snapshot remain gitignored.

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/build_schemas.py

@@ -0,0 +1,193 @@
+"""Materialize scoped multi-role relation schemas from the frozen 65-item review.
+
+The schema is the relation joining its slots. No geometric faces, inferred proof
+links or cross-theorem object identities are constructed.
+"""
+from __future__ import annotations
+
+import argparse
+import hashlib
+import html
+import json
+import re
+from collections import Counter
+from pathlib import Path
+
+from leanbench.project import project
+from leanbench.schema import KIND_OBJECT, Role, Simplex, role_from_dict
+from leanbench.schema_registry import SchemaRegistry, slot_key
+from leanbench.srcsimplex import parse_source_simplex
+
+
+def digest(path):
+    return hashlib.sha256(path.read_bytes()).hexdigest()
+
+
+def source_schema(name, payload):
+    source = parse_source_simplex(payload)
+    symbol_slots = {}
+    for role in source.roles:
+        if role.kind == KIND_OBJECT:
+            for symbol in role.symbols:
+                symbol_slots.setdefault(symbol, []).append(role.alias)
+    roles = {}
+    for role in source.roles:
+        references = sorted({alias for symbol in role.symbols for alias in symbol_slots.get(symbol, [])
+                             if alias != role.alias and len(symbol_slots[symbol]) == 1})
+        roles[role.alias] = Role(
+            role.symbols[0] if len(role.symbols) == 1 else role.alias,
+            role.kind, context=role.description,
+            attrs={"symbols": role.symbols, "keywords": role.keywords,
+                   "introduced": role.introduced, "quantifier_status": "unreviewed",
+                   "references": references,
+                   "reference_status": "explicit_symbol_candidates" if references else "unknown",
+                   "origin": "frozen_current_chat_annotation"})
+    return Simplex(name, roles, attrs={"side": "source", "goal_has_exists": source.goal_has_exists,
+                                      "reference_completeness": "partial"})
+
+
+def lean_schema(name, code):
+    projection = project(code)
+    if projection.simplex is None:
+        return None, projection
+    originals = projection.simplex.roles
+    by_name = {}
+    for alias, role in originals.items():
+        by_name.setdefault(role.name, []).append(alias)
+    roles = {}
+    for alias, role in originals.items():
+        identifiers = set(re.findall(r"[^\W\d]\w*'?", role.type_text, flags=re.UNICODE))
+        references = sorted({target for symbol in identifiers for target in by_name.get(symbol, [])
+                             if len(by_name[symbol]) == 1 and target != alias})
+        roles[alias] = Role(role.name, role.kind, type_text=role.type_text, context=role.context,
+                           choices=role.choices, attrs={**role.attrs, "references": references,
+                           "reference_status": "syntactic_candidates",
+                           "origin": "deterministic_signature_projection"})
+    return Simplex(name, roles, attrs={"side": "lean", "reference_completeness": "syntactic_only"}), projection
+
+
+def build(items, assessment, key, registry, namespace="p0-v1"):
+    by_id = {item["id"]: item for item in items}
+    records = {row["blind_id"]: row for row in assessment["records"]}
+    if (not key or len(by_id) != len(items) or len(records) != len(assessment["records"])
+            or len(set(key.values())) != len(key) or set(by_id) != set(key.values())
+            or set(records) != set(key)):
+        raise ValueError("Items, assessments and blind key must match exactly once")
+    index, snapshots = [], []
+    for blind, item_id in key.items():
+        record = records[blind]
+        if record["id"] != item_id:
+            raise ValueError("Assessment identity mismatch")
+        source_key = f"schema:{namespace}:{item_id}:source:v1"
+        lean_key = f"schema:{namespace}:{item_id}:lean:v1"
+        source = source_schema(source_key, record["source"])
+        lean, projection = lean_schema(lean_key, by_id[item_id]["lean_code"])
+        registry.set_simplex(source, source_key)
+        if lean is not None:
+            registry.set_simplex(lean, lean_key)
+        source_restored = registry.get_simplex(source_key)
+        if source_restored.as_dict() != source.as_dict():
+            raise ValueError("Source schema persistence roundtrip failed")
+        if lean is not None and registry.get_simplex(lean_key).as_dict() != lean.as_dict():
+            raise ValueError("Lean schema persistence roundtrip failed")
+        index.append({"blind_id": blind, "source_schema": source_key,
+                      "source_status": "unreviewed_annotation_seed",
+                      "source_slots": len(source.roles),
+                      "lean_schema": lean_key if lean is not None else None,
+                      "lean_slots": len(projection.roles),
+                      "lean_status": "materialized" if lean is not None else "insufficient_projected_roles",
+                      "source_role_counts": dict(Counter(r.kind for r in source.roles.values())),
+                      "lean_role_counts": dict(Counter(r.kind for r in projection.roles)),
+                      "source_slots_with_reference_candidates": sum(bool(r.attrs["references"]) for r in source.roles.values())})
+        snapshots.append({"blind_id": blind, "source": source.as_dict(),
+                          "lean": lean.as_dict() if lean is not None else None,
+                          "lean_projection": projection.as_dict(),
+                          "source_slot_keys": [slot_key(source_key, alias) for alias in source.roles]})
+    return index, snapshots
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("--items", required=True, type=Path)
+    parser.add_argument("--assessments", required=True, type=Path)
+    parser.add_argument("--key", required=True, type=Path)
+    parser.add_argument("--private-out", required=True, type=Path)
+    parser.add_argument("--index", required=True, type=Path)
+    parser.add_argument("--summary", required=True, type=Path)
+    parser.add_argument("--review-page", type=Path,
+                        help="Also export the owner-approved schema-only HTML review into the project")
+    args = parser.parse_args()
+    if "data" not in args.private_out.parts:
+        parser.error("Private schemas must remain in the gitignored data/ directory")
+    assessment = json.loads(args.assessments.read_text())
+    key = json.loads(args.key.read_text())["key"]
+    if (assessment["provenance"]["items_sha256"] != digest(args.items)
+            or assessment["provenance"]["key_sha256"] != digest(args.key)):
+        parser.error("Frozen assessment hashes do not match inputs/key")
+    items = [json.loads(line) for line in args.items.read_text().splitlines() if line.strip()]
+    args.private_out.mkdir(parents=True, exist_ok=True)
+    identity = {"items": digest(args.items), "assessments": digest(args.assessments),
+                "key": digest(args.key)}
+    manifest = args.private_out / "schema-inputs.json"
+    if manifest.exists() and json.loads(manifest.read_text()) != identity:
+        parser.error("Existing schema output belongs to different inputs; choose a new directory")
+    temporary = args.private_out / "registry.sqlite.tmp"
+    if temporary.exists():
+        temporary.unlink()
+    with SchemaRegistry(temporary) as registry:
+        index, snapshots = build(items, assessment, key, registry,
+                                 namespace=f"p0-{identity['assessments'][:12]}")
+        info = registry.info()
+    temporary.replace(args.private_out / "registry.sqlite")
+    manifest.write_text(json.dumps(identity, indent=2) + "\n")
+    (args.private_out / "schemas.json").write_text(json.dumps(snapshots, indent=2, ensure_ascii=False) + "\n")
+    sections = []
+    for row in snapshots:
+        sides = []
+        for side in ["source", "lean"]:
+            value = row[side]
+            content = (json.dumps(value, indent=2, ensure_ascii=False) if value is not None
+                       else "Insufficient projected roles; no object roles were invented.")
+            sides.append(f'<h3>{side}</h3><pre>{html.escape(content)}</pre>')
+        sections.append(f'<section id="{row["blind_id"]}"><h2>{row["blind_id"]}</h2>'
+                        + ''.join(sides) + '</section>')
+    review_page = (
+        '<!doctype html><html lang="en"><meta charset="utf-8"><title>P0 semantic simplex schemas</title>'
+        '<style>body{font:16px/1.5 system-ui;max-width:1050px;margin:32px auto;padding:16px}'
+        'pre{white-space:pre-wrap;background:#f5f5f5;padding:16px}section{border-top:1px solid #ccc}</style>'
+        '<h1>65 semantic multi-role relation schemas</h1>'
+        '<p>Schema annotation seeds, not independently validated mathematical statements. '
+        'A simplex joins the objects, assumptions and conclusion in its slots. '
+        'References are partial symbol/syntax candidates. '
+        'This review contains schema annotations and Lean signature text, not textbook passages '
+        'or full assistant judgment explanations.</p>' + ''.join(sections) + '</html>')
+    (args.private_out / "schemas.html").write_text(review_page, encoding="utf-8")
+    if args.review_page is not None:
+        args.review_page.parent.mkdir(parents=True, exist_ok=True)
+        args.review_page.write_text(review_page, encoding="utf-8")
+    # JSON-only reload is independently checked; it does not use pickle.
+    for row in snapshots:
+        for side in ["source", "lean"]:
+            if row[side] is not None:
+                if role_from_dict(row[side]).as_dict() != row[side]:
+                    raise ValueError("JSON schema roundtrip failed")
+    summary = {"representation": "semantic_multi_role_relation_schema_v1", "items": len(items),
+               "source_schemas": len(index), "lean_schemas": sum(r["lean_schema"] is not None for r in index),
+               "lean_incomplete": sum(r["lean_schema"] is None for r in index), "registry": info,
+               "hashes": {"items": digest(args.items), "assessments": digest(args.assessments),
+                          "key": digest(args.key), "builder": digest(Path(__file__)),
+                          "schema_module": digest(Path(__file__).resolve().parents[2] / "leanbench/schema.py"),
+                          "registry_module": digest(Path(__file__).resolve().parents[2] / "leanbench/schema_registry.py")},
+               "limitations": ["Source annotations come from a non-independent current-chat diagnostic.",
+                               "Source quantifiers are preserved as unreviewed; existing given tags are not repaired.",
+                               "References are symbol/syntax candidates, not complete semantic dependencies.",
+                               "No cross-theorem identity or proof dependency is inferred.",
+                               "Fewer than two projected Lean roles is a projection limitation, not proof that objects are absent."]}
+    for path, value in [(args.index, index), (args.summary, summary)]:
+        path.parent.mkdir(parents=True, exist_ok=True)
+        path.write_text(json.dumps(value, indent=2, allow_nan=False) + "\n")
+    print(json.dumps({k: summary[k] for k in ["items", "source_schemas", "lean_schemas", "lean_incomplete", "registry"]}))
+
+
+if __name__ == "__main__":
+    main()

experiments/P0-pilot/labels/labels.json

@@ -0,0 +1,427 @@
+{
+  "labeler": "Codex AI assistant (this chat; exact deployed model identifier unavailable)",
+  "labeler_type": "AI; not human gold",
+  "frozen_at": "2026-10-28T10:42:10.032234+00:00",
+  "items_sha256": "487ecd22919a5e3b0174a2846ab8fe7c0daf4d3feccccf8ea6571aec04c41bed",
+  "key_sha256": "f827cac92ee4e907554fadcc7c0e006ef2b829350f74e7f8b54ca11945e62836",
+  "method": "Single-pass semantic annotation in shuffled blind-ID order; per-item compiler outcomes and detector outputs hidden. Pure syntax/proof defects are ignored when meaning is recoverable. No compiler/API-name audit. Full extracted-span coverage is assessed; unspecified design tasks or unresolved contextual references are not formalizable.",
+  "limitations": [
+    "Single AI annotator; no human adjudication or inter-annotator agreement.",
+    "The annotator reviewed detector implementation and aggregate compilation counts before labeling; only per-item outputs were hidden.",
+    "AI labels replace the originally planned human/Kimi labels by explicit owner instruction in this chat; the original human-ground-truth protocol is therefore not fully satisfied."
+  ],
+  "labels": {
+    "P01": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The field axioms and nontriviality match the stated definition."
+    },
+    "P02": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The whole carrier and identity singleton are the two specified subgroups; API spelling is not assessed."
+    },
+    "P03": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Every integer unit is constrained to the two specified values."
+    },
+    "P04": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Generated subgroup is equated with all integer powers; escaped notation is treated as a syntax defect."
+    },
+    "P05": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Existence of a bijective multiplication-preserving map matches the definition."
+    },
+    "P06": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The theorem statement gives exactly the inverse-of-product identity; proof validity is not assessed."
+    },
+    "P07": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_conclusion",
+        "degenerate"
+      ],
+      "notes": "Only already-assumed prime factors are asserted to exist; no recovery from the totient is specified."
+    },
+    "P08": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Both identity preservation and inverse preservation are stated under a multiplicative equivalence."
+    },
+    "P09": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_type",
+        "wrong_conclusion"
+      ],
+      "notes": "The multiplicative ring carrier does not encode the additive cyclic group, and the second extracted exercise is omitted."
+    },
+    "P10": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Both left and right equations have unique solutions."
+    },
+    "P11": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The group cardinality is the exponent, with the correct identity and quantification."
+    },
+    "P12": {
+      "verdict": "not_formalizable",
+      "errors": [
+        "other"
+      ],
+      "notes": "The extracted design question provides no formal security or authentication specification for a fidelity comparison."
+    },
+    "P13": {
+      "verdict": "minor_drift",
+      "errors": [
+        "wrong_type"
+      ],
+      "notes": "The intended modular identity is retained, but the integer variable is supplied to a natural-number coprimality predicate."
+    },
+    "P14": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_conclusion"
+      ],
+      "notes": "Only existence of a ring structure is stated; the identity and unit characterization are omitted."
+    },
+    "P15": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Unique solvability in both factors expresses the row and column permutation property."
+    },
+    "P16": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Passing to the product representation preserves the order-divisibility claim; capitalization and namespace errors are not semantic changes."
+    },
+    "P17": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_conclusion"
+      ],
+      "notes": "An independent non-field example in the extracted passage is omitted."
+    },
+    "P18": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The norm-one complex carrier and multiplication describe the specified subgroup; bundling/API validity is not assessed."
+    },
+    "P19": {
+      "verdict": "minor_drift",
+      "errors": [
+        "wrong_type"
+      ],
+      "notes": "The natural-valued order convention needs an infinite-order convention absent from the cardinality definition."
+    },
+    "P20": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "A single left-identity action on one group element forces equality to the identity."
+    },
+    "P21": {
+      "verdict": "minor_drift",
+      "errors": [
+        "wrong_type"
+      ],
+      "notes": "The intended commutativity equivalence is visible, but the left operation lacks the carrier annotation needed to identify G."
+    },
+    "P22": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The two quantified unique-solvability claims express the specified table property."
+    },
+    "P23": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Prime factors, modulus, lcm exponent and coprimality reproduce the extracted claim; no unstated distinctness assumption is introduced."
+    },
+    "P24": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_conclusion",
+        "degenerate"
+      ],
+      "notes": "An arbitrary group satisfying an order condition is not identified with the geometric symmetry group."
+    },
+    "P25": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The two declarations cover both cancellation directions."
+    },
+    "P26": {
+      "verdict": "wrong",
+      "errors": [
+        "extra_hypothesis",
+        "missing_hypothesis"
+      ],
+      "notes": "The inserted divisibility assumption does not express the RSA relationship required by the argument."
+    },
+    "P27": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_conclusion"
+      ],
+      "notes": "The isomorphism is asserted for a quotient of the ambient group instead of the stabilizer subgroup."
+    },
+    "P28": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_type",
+        "wrong_conclusion"
+      ],
+      "notes": "Natural exponent division fails to express a square root, and the homomorphism target does not encode the specified automorphism."
+    },
+    "P29": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "A bijective homomorphism supplies the isomorphism assumption and both power assertions are retained."
+    },
+    "P30": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_type"
+      ],
+      "notes": "An unordered finite product is used for an arbitrary semigroup, losing the ordered nonempty product required by the exercise."
+    },
+    "P31": {
+      "verdict": "not_formalizable",
+      "errors": [
+        "other"
+      ],
+      "notes": "The isolated instruction refers to an earlier map whose definition is absent; the actual proposition cannot be recovered from this span."
+    },
+    "P32": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_conclusion",
+        "degenerate"
+      ],
+      "notes": "The result merely supplies an unspecified ring homomorphism and does not constrain it to evaluation at the matrix parameter."
+    },
+    "P33": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The cardinality assumption and the nonidentity involution conclusion match; the missing instance binder is a compilation defect."
+    },
+    "P34": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The contrasting abelian properties encode the reason these specified groups are not isomorphic."
+    },
+    "P35": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_type",
+        "quantifier"
+      ],
+      "notes": "One fixed-arity function is applied at incompatible arities instead of specifying a coherent family of products."
+    },
+    "P36": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_type",
+        "wrong_conclusion"
+      ],
+      "notes": "The ring carrier replaces the concrete root-of-unity group, and neither its order nor the specified generator is stated."
+    },
+    "P37": {
+      "verdict": "wrong",
+      "errors": [
+        "degenerate",
+        "wrong_conclusion"
+      ],
+      "notes": "The declaration has no defining expression for the requested subgroup."
+    },
+    "P38": {
+      "verdict": "wrong",
+      "errors": [
+        "missing_hypothesis"
+      ],
+      "notes": "Nonemptiness is missing, so the empty subset satisfies both closure assumptions."
+    },
+    "P39": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_type",
+        "wrong_conclusion"
+      ],
+      "notes": "Laurent series replace finite Laurent polynomials, and the requested units are not characterized."
+    },
+    "P40": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The supplied structure body fixes the function to the canonical integer residue map."
+    },
+    "P41": {
+      "verdict": "wrong",
+      "errors": [
+        "extra_hypothesis"
+      ],
+      "notes": "The cardinality assertion is restricted to the range where noncommutativity holds, dropping the smaller symmetric groups."
+    },
+    "P42": {
+      "verdict": "wrong",
+      "errors": [
+        "missing_hypothesis",
+        "wrong_conclusion"
+      ],
+      "notes": "A necessary closure condition is promoted to sufficiency without inverse closure."
+    },
+    "P43": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Any two groups of the specified size are related by a multiplicative equivalence."
+    },
+    "P44": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The defining field is exactly commutativity of the group operation."
+    },
+    "P45": {
+      "verdict": "wrong",
+      "errors": [
+        "quantifier",
+        "wrong_conclusion"
+      ],
+      "notes": "Literal uniqueness of a carrier/structure replaces uniqueness up to group isomorphism."
+    },
+    "P46": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_type",
+        "wrong_conclusion"
+      ],
+      "notes": "Univariate polynomials over a product ring replace three-variable real polynomials; the units question is omitted."
+    },
+    "P47": {
+      "verdict": "minor_drift",
+      "errors": [
+        "wrong_conclusion"
+      ],
+      "notes": "The integer-span equality captures the generated set, but the equality for opposite generators is not explicitly stated."
+    },
+    "P48": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The one-sided inverse hypothesis gives the specified inverse element."
+    },
+    "P49": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The theorem statement is exactly involutivity of group inversion."
+    },
+    "P50": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The custom structure supplies additive commutative group, associative multiplication and both distributive laws without imposing a unit."
+    },
+    "P51": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The carrier, multiplication and identity encode the specified finite group; existence of the chosen API is not audited."
+    },
+    "P52": {
+      "verdict": "minor_drift",
+      "errors": [
+        "wrong_conclusion",
+        "degenerate"
+      ],
+      "notes": "Ring structure and unit-to-constant direction are present, but identity characterization is replaced by reflexivity."
+    },
+    "P53": {
+      "verdict": "minor_drift",
+      "errors": [
+        "extra_hypothesis"
+      ],
+      "notes": "Cardinality is represented only for finite groups although the definition is not restricted to them."
+    },
+    "P54": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_type"
+      ],
+      "notes": "Multiplicative subgroup closure of a residue is used in place of the additive cyclic subgroup generated by it."
+    },
+    "P55": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The abelian-property equivalence is stated under an isomorphism."
+    },
+    "P56": {
+      "verdict": "not_formalizable",
+      "errors": [
+        "other"
+      ],
+      "notes": "The design question does not specify an authenticity predicate or formal adversarial model."
+    },
+    "P57": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_conclusion"
+      ],
+      "notes": "The homomorphism criterion is retained but the separate isomorphism definition is absent."
+    },
+    "P58": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_type"
+      ],
+      "notes": "A multiplicative equivalence on the full residue ring does not represent the additive cyclic group in the comparison."
+    },
+    "P59": {
+      "verdict": "minor_drift",
+      "errors": [
+        "wrong_type"
+      ],
+      "notes": "The inherited-group criterion is recognizable, but operations on the subset are not specified as restricted operations."
+    },
+    "P60": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_type",
+        "missing_hypothesis"
+      ],
+      "notes": "Global bijections with local differentiability conditions do not specify self-diffeomorphisms of the open subset."
+    },
+    "P61": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The homeomorphism type supplies the intended carrier and group structure under composition; notation validity is not assessed."
+    },
+    "P62": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Both least-positive exponent and the bounded-power description are retained, ignoring set-minimum API syntax."
+    },
+    "P63": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Both two-sided identity hypotheses and their equality are stated."
+    },
+    "P64": {
+      "verdict": "wrong",
+      "errors": [
+        "missing_hypothesis",
+        "extra_hypothesis"
+      ],
+      "notes": "The exponent relation uses the ciphertext modulus where the RSA exponent modulus is required."
+    },
+    "P65": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_conclusion",
+        "degenerate"
+      ],
+      "notes": "The arbitrary finite group is unrelated to the requested geometric symmetries, with the classification left in a comment."
+    }
+  }
+}

experiments/P0-pilot/make_sheet.py

@@ -154,6 +154,10 @@ def main() -> int:
 
     items = [json.loads(line) for line in args.items.read_text(encoding="utf-8").splitlines()
              if line.strip()]
+    if not items or any(not item.get("source_text", "").strip() for item in items):
+        parser.error("Every item needs nonempty source_text; use a private source-inclusive export.")
+    if len({item["id"] for item in items}) != len(items):
+        parser.error("Item IDs must be unique.")
     order = list(range(len(items)))
     random.Random(args.seed).shuffle(order)
     blind_ids = [f"P{n:02d}" for n in range(1, len(items) + 1)]

experiments/P0-pilot/prepare_items.py

@@ -0,0 +1,45 @@
+"""Restore source passages from a private archived review without changing the cohort."""
+from __future__ import annotations
+
+import argparse
+import json
+from pathlib import Path
+
+
+def restore(items: list[dict], review: dict) -> list[dict]:
+    archived = review["items"]
+    by_id = {row["id"]: row for row in archived}
+    if len(by_id) != len(archived) or len({row["id"] for row in items}) != len(items):
+        raise ValueError("Duplicate item IDs")
+    restored = []
+    for item in items:
+        original = by_id[item["id"]]
+        comparable = dict(original)
+        if isinstance(comparable.get("imports"), str):
+            comparable["imports"] = json.loads(comparable["imports"])
+        if any(comparable.get(k) != v for k, v in item.items()):
+            raise ValueError(f"Archived review does not match item {item['id']}")
+        passage = original.get("source_text", "")
+        if not passage.strip():
+            raise ValueError(f"Missing archived passage for {item['id']}")
+        restored.append({**item, "source_text": passage})
+    return restored
+
+
+def main() -> None:
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("--items", required=True, type=Path)
+    parser.add_argument("--review", required=True, type=Path)
+    parser.add_argument("--out", required=True, type=Path)
+    args = parser.parse_args()
+    if args.out.parent.name != "data":
+        parser.error("Source-inclusive output must go in a gitignored data/ directory")
+    items = [json.loads(line) for line in args.items.read_text().splitlines() if line.strip()]
+    rows = restore(items, json.loads(args.review.read_text()))
+    args.out.parent.mkdir(parents=True, exist_ok=True)
+    args.out.write_text("".join(json.dumps(row, ensure_ascii=False) + "\n" for row in rows))
+    print(f"Restored {len(rows)} passages; all exported fields are unchanged")
+
+
+if __name__ == "__main__":
+    main()

experiments/P0-pilot/results/execution.json

@@ -0,0 +1,72 @@
+{
+  "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": "https://gitea.entroia.com/Zayden-Jung/lean-bench/actions/runs/433",
+    "consolidated_pull_request": "https://gitea.entroia.com/Zayden-Jung/lean-bench/pulls/9"
+  }
+}

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/results/simplex-schema-summary.json

@@ -0,0 +1,27 @@
+{
+  "representation": "semantic_multi_role_relation_schema_v1",
+  "items": 65,
+  "source_schemas": 65,
+  "lean_schemas": 50,
+  "lean_incomplete": 15,
+  "registry": {
+    "roles": 483,
+    "simplices": 115,
+    "slots": 483
+  },
+  "hashes": {
+    "items": "487ecd22919a5e3b0174a2846ab8fe7c0daf4d3feccccf8ea6571aec04c41bed",
+    "assessments": "f12735802ba0d4d94b776a91581a13a508eab0ce90ba8973a6c9c4e4d1390272",
+    "key": "f827cac92ee4e907554fadcc7c0e006ef2b829350f74e7f8b54ca11945e62836",
+    "builder": "7b3a982101f620c1480d95b5e483ca6186a7e9c32ce587fb132a90bfb38a01bc",
+    "schema_module": "958b81e89c0befeb32d24036c130f2b37bd2e881bd5b009acf873cbcdada50ae",
+    "registry_module": "7b434b1eb178f597d4f60591a5ab74eff0c96a40fa751cb0ba75589b52e56271"
+  },
+  "limitations": [
+    "Source annotations come from a non-independent current-chat diagnostic.",
+    "Source quantifiers are preserved as unreviewed; existing given tags are not repaired.",
+    "References are symbol/syntax candidates, not complete semantic dependencies.",
+    "No cross-theorem identity or proof dependency is inferred.",
+    "Fewer than two projected Lean roles is a projection limitation, not proof that objects are absent."
+  ]
+}

experiments/P0-pilot/run_pilot.py

@@ -15,8 +15,11 @@ Hard stops: --max-calls bounds API calls; a rerun skips items already in --out.
 from __future__ import annotations
 
 import argparse
+import fcntl
 import hashlib
+import inspect
 import json
+import os
 import sys
 from pathlib import Path
 
@@ -24,7 +27,7 @@ from leanbench import srcsimplex
 from leanbench.align import align
 from leanbench.config import Settings
 from leanbench.lint import lint
-from leanbench.llm import OpenAICompatibleClient
+from leanbench.llm import OpenAICompatibleClient, Usage
 from leanbench.project import project
 
 JUDGE_PROMPT_VERSION = "judge-v1"
@@ -41,69 +44,228 @@ def judge(client, passage: str, lean: str) -> dict:
         {"role": "system", "content": JUDGE_SYSTEM},
         {"role": "user", "content": f"Passage:\n{passage}\n\nLean:\n{lean}"},
     ])
-    if not isinstance(reply, dict) or "faithful" not in reply:
+    if not isinstance(reply, dict) or type(reply.get("faithful")) is not bool:
         raise ValueError(f"unusable judge reply: {str(reply)[:200]}")
-    return {"faithful": bool(reply["faithful"]), "confidence": reply.get("confidence"),
+    return {"faithful": reply["faithful"], "confidence": reply.get("confidence"),
             "reason": str(reply.get("reason", ""))[:300]}
 
 
-def run_item(client, item: dict) -> dict:
+def provider_blocked(error: Exception) -> bool:
+    text = str(error).lower()
+    return any(code in text for code in ("arrearage", "overdue-payment", "invalid_api_key", "http 401", "http 403"))
+
+
+def complete_row(row: dict) -> bool:
+    return not row.get("errors") and "role" in row and "judge" in row
+
+
+class ProviderBlocked(RuntimeError):
+    """A billing or authentication failure requires external recovery before resuming."""
+
+    def __init__(self, row):
+        super().__init__("Provider billing/authentication blocked; partial results were preserved")
+        self.row = 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 = {"id": item["id"], "compiled": bool(item.get("verified")), "errors": {}}
+    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)
-    try:
-        src = srcsimplex.extract_source_simplex(client, item.get("source_text", ""),
-                                                item.get("label", ""))
-        al = align(src, proj)
-        row["source"] = [r.__dict__ for r in src.roles]
-        row["role"] = al.as_dict()
-    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 Exception as error:
-        row["errors"]["judge"] = str(error)[:300]
+    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()
+
+
+def atomic_json(path: Path, value: dict) -> None:
+    temporary = path.with_suffix(path.suffix + ".tmp")
+    temporary.write_text(json.dumps(value, indent=2, allow_nan=False) + "\n", encoding="utf-8")
+    os.replace(temporary, path)
+
+
+class AuditedClient(OpenAICompatibleClient):
+    """Persist reservations before HTTP requests, including transport and JSON retries."""
+
+    def complete(self, *args, **kwargs):
+        try:
+            return super().complete(*args, **kwargs)
+        finally:
+            self.checkpoint()
+
+
+def execute(args, items, settings) -> int:
+    rows = []
+    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 if complete_row(row)}
+    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(),
+        "judge": hashlib.sha256(JUDGE_SYSTEM.encode()).hexdigest(),
+    }
+    identity = {"model": settings.llm.model, "base_url": settings.llm.base_url,
+                "temperature": settings.llm.temperature, "items_sha256": digest(args.items),
+                "prompt_hashes": hashes,
+                "prompts": [srcsimplex.PROMPT_VERSION, JUDGE_PROMPT_VERSION]}
+    labels = getattr(args, "labels", None)
+    if labels is not None:
+        identity["labels_sha256"] = digest(labels)
+    meta_path = args.out.with_suffix(".meta.json")
+    meta = {**identity, "request_attempts": 0, "usage": Usage().as_dict(), "status": "ready"}
+    if meta_path.exists():
+        meta = json.loads(meta_path.read_text(encoding="utf-8"))
+        if any(meta.get(k) != v for k, v in identity.items()):
+            raise ValueError("Run identity changed; use a new output path instead of mixing runs")
+    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}")
+    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)
+    client.usage = Usage(**meta["usage"])
+
+    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():
+        if meta["request_attempts"] >= args.max_calls:
+            raise CallBudgetExceeded("Cumulative request cap reached; no further HTTP request was sent")
+        meta["request_attempts"] += 1
+        checkpoint()
+
+    client.checkpoint = checkpoint
+    client.request_guard = reserve
+    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:
+            row = run_item(client, item, by_id.get(item["id"]))
+            save_row(row)
+            print(f"completed={len(done)}/{len(items)} requests={meta['request_attempts']}", flush=True)
+        meta["status"] = "complete" if len(done) == len(items) else "detector_errors"
+    except (CallBudgetExceeded, ProviderBlocked) as error:
+        if getattr(error, "row", None) is not None:
+            save_row(error.row)
+        meta["status"] = "provider_blocked" if isinstance(error, ProviderBlocked) else "budget_exhausted"
+        print(str(error), file=sys.stderr)
+    except BaseException:
+        meta["status"] = "interrupted"
+        raise
+    finally:
+        if args.out.exists():
+            meta["results_sha256"] = digest(args.out)
+        checkpoint()
+    print(json.dumps(meta))
+    return 0 if meta["status"] == "complete" else 2
+
+
 def main() -> int:
     ap = argparse.ArgumentParser(description=__doc__.splitlines()[0])
     ap.add_argument("--items", required=True, type=Path)
     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:
+        ap.error("P0 requires a request cap between 1 and 400")
     items = [json.loads(x) for x in args.items.read_text(encoding="utf-8").splitlines() if x.strip()]
-    done = set()
-    if args.out.exists():
-        done = {json.loads(x)["id"] for x in args.out.read_text(encoding="utf-8").splitlines() if x.strip()}
-    todo = [i for i in items if i["id"] not in done]
-    settings = Settings.from_env()
-    est = len(todo) * 3  # extract (<=2 tries) + judge
-    print(f"items={len(items)} done={len(done)} todo={len(todo)} model={settings.llm.model} "
-          f"est_calls<={est} (extract x2 + judge) cap={args.max_calls}")
-    print("prompts:", srcsimplex.PROMPT_VERSION, JUDGE_PROMPT_VERSION,
-          hashlib.sha256((srcsimplex.SYSTEM_PROMPT + JUDGE_SYSTEM).encode()).hexdigest()[:12])
-    if args.dry_run:
-        return 0
-
-    client = OpenAICompatibleClient.from_settings(settings.llm)
+    if not items or len({item["id"] for item in items}) != len(items):
+        ap.error("Input must contain unique item IDs")
+    if any(not item.get("source_text", "").strip() for item in items):
+        ap.error("Every item needs nonempty source_text; use a private source-inclusive export")
+    if not args.dry_run and args.labels is None:
+        ap.error("Freeze all blind labels first, then pass --labels")
+    if args.labels is not None:
+        annotation = json.loads(args.labels.read_text(encoding="utf-8"))
+        key_path = args.labels.with_name("key.json")
+        key = json.loads(key_path.read_text(encoding="utf-8"))["key"]
+        verdicts = {"faithful", "minor_drift", "wrong", "not_formalizable"}
+        if (set(key.values()) != {item["id"] for item in items}
+                or set(annotation["labels"]) != set(key)
+                or any(row.get("verdict") not in verdicts for row in annotation["labels"].values())
+                or annotation.get("items_sha256") != digest(args.items)
+                or annotation.get("key_sha256") != digest(key_path)):
+            ap.error("Frozen labels, key and source-inclusive items must be complete and match")
     args.out.parent.mkdir(parents=True, exist_ok=True)
-    with args.out.open("a", encoding="utf-8") as fh:
-        for item in todo:
-            if client.usage.calls >= args.max_calls:
-                print("call cap reached; rerun to resume", file=sys.stderr)
-                break
-            fh.write(json.dumps(run_item(client, item), ensure_ascii=False) + "\n")
-            fh.flush()
-    meta = {"model": settings.llm.model, "usage": client.usage.as_dict(),
-            "prompts": [srcsimplex.PROMPT_VERSION, JUDGE_PROMPT_VERSION]}
-    (args.out.parent / "run_meta.json").write_text(json.dumps(meta, indent=2), encoding="utf-8")
-    print(json.dumps(meta))
-    return 0
+    with args.out.with_suffix(args.out.suffix + ".lock").open("w") as lock:
+        fcntl.flock(lock, fcntl.LOCK_EX | fcntl.LOCK_NB)
+        return execute(args, items, Settings.from_env())
 
 
 if __name__ == "__main__":

experiments/P0-pilot/score.py

@@ -1,9 +1,9 @@
-"""Score the pilot: detectors vs. the blind human labels, with the pre-registered decision.
+"""Score the pilot against frozen blind labels using the pre-registered decision.
 
     python experiments/P0-pilot/score.py --results experiments/P0-pilot/data/results.jsonl \
         --labels experiments/P0-pilot/labels/labels.json --key experiments/P0-pilot/labels/key.json --summary experiments/P0-pilot/results/summary.json
 
-Positive class = unfaithful. Primary: verdict == "wrong", over ALL labeled items (role alignment and
+Positive class = unfaithful. Primary: wrong versus faithful, excluding minor drift (role alignment and
 the judge do not need Lean to accept the code; only 10 of the 65 pilot items compiled, too few to
 decide on). Secondary: wrong or minor_drift; and the compiled-only subset (the paper's claim, reported
 with its interval, not used to decide). "not_formalizable" items are excluded. Decision (fixed before
@@ -19,22 +19,35 @@ With ~65 items every number carries a wide Wilson interval; the pilot checks for
 from __future__ import annotations
 
 import argparse
+import hashlib
 import json
+import math
 from pathlib import Path
 
-from leanbench.evalstats import auc, confusion
+from leanbench.evalstats import auc, confusion, wilson
 
 
 def load(args):
-    results = {json.loads(x)["id"]: json.loads(x) for x in args.results.read_text(encoding="utf-8").splitlines() if x.strip()}
+    result_rows = [json.loads(x) for x in args.results.read_text(encoding="utf-8").splitlines() if x.strip()]
+    results = {row["id"]: row for row in result_rows}
     labels = json.loads(args.labels.read_text(encoding="utf-8"))["labels"]
     key = json.loads(args.key.read_text(encoding="utf-8"))["key"]
+    if not key or len(set(key.values())) != len(key):
+        raise ValueError("The blind key must contain unique item IDs")
+    if len(results) != len(result_rows) or set(results) != set(key.values()):
+        raise ValueError("Results must cover every keyed item exactly once")
+    if set(labels) != set(key):
+        raise ValueError("Labels must cover every blind ID exactly once")
     rows = []
     for blind, item_id in key.items():
         lab = labels.get(blind) or {}
-        if item_id in results and lab.get("verdict"):
-            rows.append({**results[item_id], "blind": blind, "verdict": lab["verdict"],
-                         "human_errors": lab.get("errors", [])})
+        if lab.get("verdict") not in {"faithful", "minor_drift", "wrong", "not_formalizable"}:
+            raise ValueError(f"Missing or invalid verdict for {blind}")
+        row = results[item_id]
+        if row.get("errors") or "judge" not in row or "role" not in row:
+            raise ValueError(f"Unresolved detector failure for {blind}; no decision can be issued")
+        rows.append({**row, "blind": blind, "verdict": lab["verdict"],
+                     "human_errors": lab.get("errors", [])})
     return rows
 
 
@@ -51,19 +64,24 @@ def report(rows, positive):
     out = {}
     for name in ("compile_only", "lint", "role", "judge"):
         out[name] = confusion([flags(r)[name] for r in rows], [positive(r) for r in rows]).as_dict()
+        out[name]["precision_ci"] = wilson(out[name]["tp"], out[name]["tp"] + out[name]["fp"])
     out["role"]["auc_score"] = auc([-(r.get("role", {}).get("score", 1.0)) for r in rows],
                                    [positive(r) for r in rows])
+    out["role"]["complementary_wrong"] = sum(
+        positive(r) and flags(r)["role"] and not flags(r)["judge"] for r in rows
+    )
     return out
 
 
 def decide(sub):
     role, judge = sub["role"], sub["judge"]
-    if role["tp"] + role["fn"] == 0:
-        return "INSUFFICIENT: no wrong items in the labels"
+    if role["tp"] + role["fn"] == 0 or role["fp"] + role["tn"] == 0:
+        return "INSUFFICIENT: both wrong and faithful items are required"
     go = (role["recall"] >= 0.5 and role["false_flag_rate"] <= 0.2
           and role["recall"] >= judge["recall"] + 0.10
           and role["false_flag_rate"] <= judge["false_flag_rate"])
-    partial = (role["recall"] >= 0.4 and role["false_flag_rate"] <= 0.3)
+    partial = ((role["recall"] >= 0.4 and role["false_flag_rate"] <= 0.3)
+               or role.get("complementary_wrong", 0) >= 3)
     return "GO" if go else "PARTIAL" if partial else "NO-GO"
 
 
@@ -75,19 +93,51 @@ def main() -> int:
     ap.add_argument("--summary", type=Path, default=None,
                     help="also write the (text-free) summary here, e.g. results/summary.json")
     args = ap.parse_args()
-    rows = [r for r in load(args) if r["verdict"] != "not_formalizable"]
-    compiled = [r for r in rows if r["compiled"]]
+    meta = json.loads(args.results.with_suffix(".meta.json").read_text(encoding="utf-8"))
+    if (meta.get("status") != "complete"
+            or meta.get("labels_sha256") != hashlib.sha256(args.labels.read_bytes()).hexdigest()
+            or meta.get("results_sha256") != hashlib.sha256(args.results.read_bytes()).hexdigest()):
+        ap.error("Scoring requires a complete run with unchanged frozen labels and results")
+    all_rows = load(args)
+    rows = [r for r in all_rows if r["verdict"] != "not_formalizable"]
+    primary = [r for r in rows if r["verdict"] != "minor_drift"]
+    compiled = [r for r in primary if r["compiled"]]
     summary = {
-        "n_labeled": len(rows), "n_compiled": len(compiled),
+        "run_metadata": meta,
+        "n_labeled": len(all_rows), "n_evaluable": len(rows), "n_primary": len(primary),
+        "n_compiled": len(compiled),
         "verdicts": {v: sum(r["verdict"] == v for r in rows) for v in
-                     ("faithful", "minor_drift", "wrong")},
+                     ("faithful", "minor_drift", "wrong", "not_formalizable")},
         "compiled_but_wrong": sum(r["verdict"] == "wrong" for r in compiled),
-        "primary_all": report(rows, lambda r: r["verdict"] == "wrong"),
+        "primary_all": report(primary, lambda r: r["verdict"] == "wrong"),
         "secondary_all": report(rows, lambda r: r["verdict"] in ("wrong", "minor_drift")),
         "compiled_only": report(compiled, lambda r: r["verdict"] == "wrong"),
     }
+    summary["verdicts"]["not_formalizable"] = len(all_rows) - len(rows)
+    summary["role_recall_by_error"] = {
+        error: {"flagged": sum(flags(r)["role"] for r in rows
+                                if r["verdict"] == "wrong" and error in r["human_errors"]),
+                "total": sum(r["verdict"] == "wrong" and error in r["human_errors"] for r in rows)}
+        for error in sorted({e for r in rows for e in r["human_errors"]})
+    }
+    summary["degenerate_projection"] = {
+        "total": sum(bool(r.get("projection", {}).get("degenerate")) for r in all_rows),
+        "wrong": sum(r["verdict"] == "wrong" and bool(r.get("projection", {}).get("degenerate"))
+                     for r in all_rows),
+    }
+    summary["disagreements"] = [
+        {"blind": r["blind"], "verdict": r["verdict"], "flags": flags(r)}
+        for r in primary if any(f != (r["verdict"] == "wrong") for f in flags(r).values())
+    ]
     summary["decision"] = decide(summary["primary_all"])
-    text = json.dumps(summary, indent=2, default=str)
+    def finite_json(value):
+        if isinstance(value, dict):
+            return {k: finite_json(v) for k, v in value.items()}
+        if isinstance(value, (list, tuple)):
+            return [finite_json(v) for v in value]
+        return None if isinstance(value, float) and not math.isfinite(value) else value
+
+    text = json.dumps(finite_json(summary), indent=2, allow_nan=False)
     if args.summary:
         args.summary.parent.mkdir(parents=True, exist_ok=True)
         args.summary.write_text(text + "\n", encoding="utf-8")

leanbench/llm.py

@@ -14,7 +14,7 @@ import re
 import time
 import urllib.error
 import urllib.request
-from collections.abc import Iterable
+from collections.abc import Callable, Iterable
 from dataclasses import dataclass, field
 from typing import Any, Protocol
 
@@ -66,6 +66,7 @@ class OpenAICompatibleClient:
     max_retries: int = 4
     temperature: float = 0.0
     usage: Usage = field(default_factory=Usage)
+    request_guard: Callable[[], None] | None = field(default=None, repr=False)
 
     @classmethod
     def from_settings(cls, settings: LLMSettings) -> OpenAICompatibleClient:
@@ -97,6 +98,8 @@ class OpenAICompatibleClient:
         }
         last: Exception | None = None
         for attempt in range(self.max_retries + 1):
+            if self.request_guard is not None:
+                self.request_guard()
             request = urllib.request.Request(url, data=body, headers=headers, method="POST")
             try:
                 with urllib.request.urlopen(request, timeout=self.timeout) as response:

leanbench/schema.py

@@ -1,4 +1,4 @@
-"""Roles and simplices: the parameters of a declaration as a small typed schema.
+"""Semantic multi-role relation schemas, not geometric simplices.
 
 A Lean declaration is a bundle of roles: the objects it is about (``(G : Type*)``),
 the facts it assumes (``(h : a ∣ b)``), and the goal it asserts or the thing it
@@ -8,8 +8,8 @@ be read off the prose of a book, so the two can be compared role by role.
 Design notes (from the archived ``schema-simplex`` prototype):
 
 * a role may be *constrained* to a closed set of allowed values (``choices``);
-* a simplex is itself a role, so simplices nest (a lemma used by another is a role
-  of it), which is how a dependency structure appears;
+* a simplex is itself a role, so explicitly supplied schemas can be composed;
+  nesting does not discover a proof dependency;
 * validation lives in ``__init__``. The prototype put it in a dataclass
   ``__post_init__`` next to a hand-written ``__init__``, where it never ran.
 """
@@ -41,7 +41,7 @@ class Role:
         choices: Sequence[Any] | None = None,
         attrs: dict[str, Any] | None = None,
     ) -> None:
-        if not name:
+        if not isinstance(name, str) or not name.strip():
             raise ValueError("a role needs a name")
         if kind not in KINDS:
             raise ValueError(f"unknown role kind {kind!r}; expected one of {KINDS}")
@@ -49,6 +49,8 @@ class Role:
         self.kind = kind
         self.type_text = type_text
         self.context = context
+        if isinstance(choices, (str, bytes)):
+            raise ValueError("choices must be a value sequence, not a string")
         self.choices: list[Any] | None = list(choices) if choices is not None else None
         self.attrs: dict[str, Any] = dict(attrs or {})
 
@@ -83,12 +85,21 @@ class Role:
 class Simplex(Role):
     """A reusable bundle of at least two roles, keyed by alias. Itself a role."""
 
-    def __init__(self, name: str, roles: dict[str, Role], *, context: str = "") -> None:
-        super().__init__(name, KIND_SIMPLEX, context=context)
+    def __init__(self, name: str, roles: dict[str, Role], *, context: str = "",
+                 attrs: dict[str, Any] | None = None) -> None:
+        super().__init__(name, KIND_SIMPLEX, context=context, attrs=attrs)
         if len(roles) < MIN_ROLES:
             raise ValueError(
                 f"simplex {name!r} needs at least {MIN_ROLES} roles, got {len(roles)}"
             )
+        if any(not isinstance(alias, str) or not alias or not isinstance(role, Role)
+               for alias, role in roles.items()):
+            raise ValueError("simplex slots need nonempty aliases and Role values")
+        for role in roles.values():
+            references = role.attrs.get("references", [])
+            if (not isinstance(references, list)
+                    or any(not isinstance(alias, str) or alias not in roles for alias in references)):
+                raise ValueError("role references must name slots in this simplex")
         self.roles = dict(roles)
 
     def by_kind(self, kind: str) -> list[Role]:
@@ -105,16 +116,16 @@ class Simplex(Role):
         return out
 
     def as_dict(self) -> dict[str, Any]:
-        return {
-            "name": self.name,
-            "roles": {alias: role.as_dict() for alias, role in self.roles.items()},
-        }
+        return {**super().as_dict(),
+                "roles": {alias: role.as_dict() for alias, role in self.roles.items()}}
 
 
 class State:
     """A role together with a value; unresolved until it has one."""
 
     def __init__(self, role: Role, value: Any = None) -> None:
+        if value is not None:
+            role.check_value(value)
         self.role = role
         self.value = value
 
@@ -133,3 +144,41 @@ class Fact(State):
 
 class Goal(State):
     """To be resolved."""
+
+
+def role_from_dict(data: dict[str, Any]) -> Role:
+    """Restore JSON role/schema data without executing code or loading pickle."""
+    kind = data.get("kind", KIND_SIMPLEX if "roles" in data else KIND_OBJECT)
+    if kind == KIND_SIMPLEX:
+        return Simplex(data["name"], {alias: role_from_dict(role)
+                                   for alias, role in data["roles"].items()},
+                       context=data.get("context", ""), attrs=data.get("attrs"))
+    return Role(data["name"], kind, type_text=data.get("type", ""),
+                context=data.get("context", ""), choices=data.get("choices"),
+                attrs=data.get("attrs"))
+
+
+class SimplexInstance:
+    """Values bind local slot aliases; a resolved goal is supplied, not proved here."""
+
+    def __init__(self, schema: Simplex, facts: dict[str, Any] | None = None,
+                 goals: Sequence[str] | None = None) -> None:
+        self.schema = schema
+        facts = facts or {}
+        goal_aliases = list(goals) if goals is not None else [
+            alias for alias, role in schema.roles.items() if role.kind in (KIND_GOAL, KIND_OWN)]
+        if (len(set(goal_aliases)) != len(goal_aliases)
+                or not (set(facts) | set(goal_aliases)) <= set(schema.roles)
+                or set(facts) & set(goal_aliases)):
+            raise ValueError("facts/goals need distinct, declared slot aliases")
+        self.facts = {alias: Fact(schema.roles[alias], value) for alias, value in facts.items()}
+        self.goals = {alias: Goal(schema.roles[alias]) for alias in goal_aliases}
+
+    def resolve(self, alias: str, value: Any) -> None:
+        if alias not in self.goals or value is None:
+            raise ValueError("resolve needs a declared goal and a non-None value")
+        self.goals[alias].role.check_value(value)
+        self.goals[alias].value = value
+
+    def is_completed(self) -> bool:
+        return bool(self.goals) and all(goal.is_resolved() for goal in self.goals.values())

leanbench/schema_registry.py

@@ -0,0 +1,208 @@
+"""JSON/SQLite registry of semantic relation schemas and scoped slot occurrences.
+
+A role definition may be reused deliberately. Occurrences remain local to a
+simplex: sharing a role definition never equates the objects bound to its aliases.
+"""
+from __future__ import annotations
+
+import fnmatch
+import json
+import sqlite3
+from collections.abc import Iterable, Mapping
+from pathlib import Path
+from urllib.parse import quote
+
+from .schema import KIND_GOAL, KIND_OWN, KIND_SIMPLEX, Role, Simplex, role_from_dict
+
+
+def slot_key(parent: str, alias: str) -> str:
+    """An occurrence identity, distinct even when two slots reuse one definition."""
+    return f"{parent}/slot/{quote(alias, safe='')}"
+
+
+class SchemaRegistry:
+    """Immutable versioned records; reusing a key with changed content is rejected."""
+
+    def __init__(self, path: str | Path = ":memory:") -> None:
+        self.connection = sqlite3.connect(str(path))
+        self.connection.execute("PRAGMA foreign_keys = ON")
+        self.connection.executescript("""
+            CREATE TABLE IF NOT EXISTS schema_nodes (
+                key TEXT PRIMARY KEY,
+                kind TEXT NOT NULL CHECK(kind IN ('role', 'simplex')),
+                payload TEXT NOT NULL
+            );
+            CREATE TABLE IF NOT EXISTS schema_slots (
+                parent TEXT NOT NULL REFERENCES schema_nodes(key) ON DELETE CASCADE,
+                alias TEXT NOT NULL,
+                child TEXT NOT NULL REFERENCES schema_nodes(key) ON DELETE RESTRICT,
+                position INTEGER NOT NULL,
+                PRIMARY KEY(parent, alias),
+                UNIQUE(parent, position)
+            );
+            CREATE INDEX IF NOT EXISTS schema_slots_child ON schema_slots(child);
+        """)
+
+    def __enter__(self):
+        return self
+
+    def __exit__(self, *_):
+        self.close()
+
+    def close(self) -> None:
+        self.connection.close()
+
+    def _insert(self, key: str, kind: str, payload: dict) -> None:
+        if not isinstance(key, str) or not key:
+            raise ValueError("a registry key must be nonempty")
+        if (kind == "simplex") != (payload.get("kind") == KIND_SIMPLEX):
+            raise ValueError("nested simplex roles must use a Simplex object")
+        encoded = json.dumps(payload, sort_keys=True, ensure_ascii=False, allow_nan=False)
+        existing = self.connection.execute(
+            "SELECT kind, payload FROM schema_nodes WHERE key = ?", (key,)).fetchone()
+        if existing is not None and existing != (kind, encoded):
+            raise ValueError(f"key {key!r} already has different content; use a new version key")
+        self.connection.execute("INSERT OR IGNORE INTO schema_nodes VALUES (?, ?, ?)",
+                                (key, kind, encoded))
+
+    def set_role(self, role: Role, key: str | None = None) -> str:
+        if isinstance(role, Simplex):
+            raise ValueError("use set_simplex for nested schemas")
+        key = key or f"role:{role.name}"
+        with self.connection:
+            self._insert(key, "role", role.as_dict())
+        return key
+
+    def set_simplex(self, simplex: Simplex, key: str | None = None,
+                    role_keys: Mapping[str, str] | None = None) -> str:
+        """Default children are scoped. role_keys explicitly opts into definition reuse."""
+        key = key or f"schema:{simplex.name}"
+        role_keys = dict(role_keys or {})
+        if not set(role_keys) <= set(simplex.roles):
+            raise ValueError("reuse map has an unknown alias")
+        with self.connection:
+            self._put_simplex(simplex, key, role_keys, set())
+        return key
+
+    def _put_simplex(self, simplex: Simplex, key: str, reuse: dict[str, str],
+                     active: set[int]) -> None:
+        if id(simplex) in active:
+            raise ValueError("cyclic simplex nesting")
+        active = active | {id(simplex)}
+        # Metadata only; children live in a relational slot table, not pickle blobs.
+        payload = Role.as_dict(simplex)
+        existing = self.connection.execute(
+            "SELECT key FROM schema_nodes WHERE key = ?", (key,)).fetchone()
+        if existing:
+            restored = self.get_simplex(key)
+            if restored is None or restored.as_dict() != simplex.as_dict():
+                raise ValueError(f"key {key!r} already has different content; use a new version key")
+            expected = {alias: reuse.get(alias, slot_key(key, alias)) for alias in simplex.roles}
+            if self.slots(key) != expected:
+                raise ValueError("same schema key cannot change its role-definition references")
+            return
+        self._insert(key, "simplex", payload)
+        for position, (alias, child) in enumerate(simplex.roles.items()):
+            child_key = reuse.get(alias, slot_key(key, alias))
+            if alias in reuse:
+                restored = self.get(child_key)
+                if restored is None or restored.as_dict() != child.as_dict():
+                    raise ValueError(f"reused role definition does not match slot {alias!r}")
+            elif isinstance(child, Simplex):
+                self._put_simplex(child, child_key, {}, active)
+            else:
+                self._insert(child_key, "role", child.as_dict())
+            self.connection.execute("INSERT INTO schema_slots VALUES (?, ?, ?, ?)",
+                                    (key, alias, child_key, position))
+
+    def get(self, key: str) -> Role | None:
+        return self._get(key, set())
+
+    def _get(self, key: str, active: set[str]) -> Role | None:
+        if key in active:
+            raise ValueError("cyclic schema references in registry")
+        row = self.connection.execute(
+            "SELECT kind, payload FROM schema_nodes WHERE key = ?", (key,)).fetchone()
+        if row is None:
+            return None
+        kind, encoded = row
+        payload = json.loads(encoded)
+        if kind == "role":
+            return role_from_dict(payload)
+        slots = self.slots(key)
+        children = {alias: self._get(child, active | {key}) for alias, child in slots.items()}
+        return Simplex(payload["name"], children, context=payload.get("context", ""),
+                       attrs=payload.get("attrs"))
+
+    def get_role(self, key: str) -> Role | None:
+        value = self.get(key)
+        return value if not isinstance(value, Simplex) else None
+
+    def get_simplex(self, key: str) -> Simplex | None:
+        value = self.get(key)
+        return value if isinstance(value, Simplex) else None
+
+    def slots(self, key: str) -> dict[str, str]:
+        return dict(self.connection.execute(
+            "SELECT alias, child FROM schema_slots WHERE parent = ? ORDER BY position", (key,)))
+
+    def keys(self, pattern: str = "*") -> list[str]:
+        return [key for (key,) in self.connection.execute("SELECT key FROM schema_nodes ORDER BY key")
+                if fnmatch.fnmatchcase(key, pattern)]
+
+    def search_roles(self, query: str, limit: int = 10) -> list[dict]:
+        """Literal substring candidates; search does not authorize semantic reuse."""
+        if not query.strip() or limit < 1:
+            return []
+        found = []
+        for key, payload in self.connection.execute(
+                "SELECT key, payload FROM schema_nodes WHERE kind = 'role' ORDER BY key"):
+            if query.casefold() in (key + payload).casefold():
+                found.append({"key": key, "role": json.loads(payload)})
+                if len(found) == limit:
+                    break
+        return found
+
+    def find_by_roles(self, role_keys: Iterable[str], match_all: bool = False) -> list[str]:
+        """Find schema keys containing definition keys, including nested descendants."""
+        wanted = set(role_keys)
+        if not wanted:
+            return []
+        found = []
+        for key in self._simplex_keys():
+            descendants = {row[0] for row in self.connection.execute("""
+                WITH RECURSIVE descendants(child) AS (
+                    SELECT child FROM schema_slots WHERE parent = ?
+                    UNION
+                    SELECT slots.child FROM schema_slots slots JOIN descendants d ON slots.parent = d.child
+                ) SELECT child FROM descendants
+            """, (key,))}
+            matches = wanted <= descendants if match_all else bool(wanted & descendants)
+            if matches:
+                found.append(key)
+        return found
+
+    def find_solvable(self, known_slots: Iterable[str]) -> list[dict]:
+        """Structural readiness by scoped occurrences, not proof or value unification."""
+        known = set(known_slots)
+        candidates = []
+        for key in self._simplex_keys():
+            schema = self.get_simplex(key)
+            inputs, outputs = [], []
+            for alias, role in schema.roles.items():
+                target = outputs if role.kind in (KIND_GOAL, KIND_OWN) else inputs
+                target.append(slot_key(key, alias))
+            missing_outputs = [output for output in outputs if output not in known]
+            if missing_outputs and set(inputs) <= known:
+                candidates.append({"schema_key": key, "input_slots": inputs,
+                                   "target_slots": missing_outputs, "structural_candidate_only": True})
+        return candidates
+
+    def _simplex_keys(self) -> list[str]:
+        return [row[0] for row in self.connection.execute(
+            "SELECT key FROM schema_nodes WHERE kind = 'simplex' ORDER BY key")]
+
+    def info(self) -> dict[str, int]:
+        counts = dict(self.connection.execute("SELECT kind, count(*) FROM schema_nodes GROUP BY kind"))
+        return {"roles": counts.get("role", 0), "simplices": counts.get("simplex", 0),
+                "slots": self.connection.execute("SELECT count(*) FROM schema_slots").fetchone()[0]}

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

@@ -36,3 +36,187 @@ def test_run_item_and_score(tmp_path):
     out = sc.report(rows, lambda r: r["verdict"] == "wrong")
     assert out["judge"]["n"] == 4
     assert sc.decide(out) in {"GO", "PARTIAL", "NO-GO"}
+
+
+def test_complementary_signal_is_partial():
+    sc = load("score")
+    rows = [
+        {"compiled": True, "lint": [], "role": {"flagged": i < 3, "score": 0.1},
+         "judge": {"faithful": False if 3 <= i < 8 else True}, "verdict": "wrong"}
+        for i in range(10)
+    ] + [
+        {"compiled": True, "lint": [], "role": {"flagged": False, "score": 1},
+         "judge": {"faithful": True}, "verdict": "faithful"}
+    ]
+    summary = sc.report(rows, lambda row: row["verdict"] == "wrong")
+    assert summary["role"]["recall"] == 0.3
+    assert summary["role"]["complementary_wrong"] == 3
+    assert sc.decide(summary) == "PARTIAL"
+
+
+def test_score_rejects_missing_labels_and_detector_failures(tmp_path):
+    import argparse
+    import json
+
+    import pytest
+
+    sc = load("score")
+    args = argparse.Namespace(results=tmp_path / "results.jsonl", labels=tmp_path / "labels.json",
+                              key=tmp_path / "key.json")
+    args.key.write_text(json.dumps({"key": {"P01": "x1"}}))
+    args.labels.write_text(json.dumps({"labels": {"P01": {"verdict": None}}}))
+    args.results.write_text(json.dumps({"id": "x1"}) + "\n")
+    with pytest.raises(ValueError, match="verdict"):
+        sc.load(args)
+    args.labels.write_text(json.dumps({"labels": {"P01": {"verdict": "wrong"}}}))
+    with pytest.raises(ValueError, match="detector failure"):
+        sc.load(args)
+    args.results.write_text("")
+    with pytest.raises(ValueError, match="every keyed item"):
+        sc.load(args)
+
+
+def test_request_budget_survives_resume_and_transport_retries(tmp_path, monkeypatch):
+    import argparse
+    import json
+    import urllib.error
+
+    import pytest
+
+    from leanbench.config import Settings
+
+    rp = load("run_pilot")
+    args = argparse.Namespace(items=tmp_path / "items.jsonl", out=tmp_path / "results.jsonl",
+                              max_calls=2, dry_run=False)
+    args.items.write_text(json.dumps(ITEM) + "\n")
+    monkeypatch.setenv("DASHSCOPE_API_KEY", "test-only")
+    settings = Settings()
+    settings.llm.max_retries = 5
+    requests = []
+
+    def fail(*args, **kwargs):
+        requests.append(1)
+        raise urllib.error.URLError("offline test")
+
+    monkeypatch.setattr("urllib.request.urlopen", fail)
+    monkeypatch.setattr("leanbench.llm.time.sleep", lambda *_: None)
+    assert rp.execute(args, [ITEM], settings) == 2
+    assert len(requests) == 2
+    assert rp.execute(args, [ITEM], settings) == 2
+    assert len(requests) == 2
+    meta = json.loads(args.out.with_suffix(".meta.json").read_text())
+    assert meta["request_attempts"] == 2
+    assert len(meta["prompt_hashes"]["judge"]) == 64
+    assert meta["status"] == "budget_exhausted"
+    settings.llm.model = "other-model"
+    with pytest.raises(ValueError, match="identity changed"):
+        rp.execute(args, [ITEM], settings)
+
+
+def test_run_rejects_missing_source_passage():
+    import pytest
+
+    rp = load("run_pilot")
+    with pytest.raises(ValueError, match="Missing source_text"):
+        rp.run_item(Stub(), {**ITEM, "source_text": ""})
+
+
+def test_restore_passages_checks_cohort_and_normalizes_archived_imports():
+    import pytest
+
+    prepare = load("prepare_items")
+    item = {"id": "x", "lean_code": "example : True := trivial", "imports": ["Mathlib"]}
+    original = {**item, "imports": '["Mathlib"]', "source_text": "A private passage."}
+    restored = prepare.restore([item], {"items": [original]})
+    assert restored == [{**item, "source_text": "A private passage."}]
+    with pytest.raises(ValueError, match="does not match"):
+        prepare.restore([{**item, "lean_code": "changed"}], {"items": [original]})
+
+
+def test_judge_rejects_string_boolean():
+    import pytest
+
+    from leanbench.llm import ScriptedClient
+
+    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"

tests/test_schema_registry.py

@@ -0,0 +1,162 @@
+"""Semantic role definitions, scoped occurrences and structural candidate retrieval."""
+import json
+
+import pytest
+
+from leanbench.schema import (
+    KIND_FACT,
+    KIND_GOAL,
+    Fact,
+    Role,
+    Simplex,
+    SimplexInstance,
+    role_from_dict,
+)
+from leanbench.schema_registry import SchemaRegistry, slot_key
+
+
+def theorem(name="t"):
+    return Simplex(name, {"G": Role("group", context="A group carrier"),
+                          "g": Role("element", type_text="G", attrs={"references": ["G"]}),
+                          "finite": Role("finite", KIND_FACT, type_text="Finite G",
+                                         attrs={"references": ["G"]}),
+                          "goal": Role("claim", KIND_GOAL, type_text="P G g",
+                                       attrs={"references": ["G", "g"]})},
+                   context="A multi-object claim", attrs={"provenance": "synthetic"})
+
+
+def test_json_roundtrip_keeps_metadata_and_nesting():
+    outer = Simplex("outer", {"lemma": theorem(), "goal": Role("result", KIND_GOAL)},
+                    context="Composed relation", attrs={"version": 1})
+    encoded = json.loads(json.dumps(outer.as_dict()))
+    restored = role_from_dict(encoded)
+    assert restored.as_dict() == outer.as_dict()
+    assert restored.roles["lemma"].roles["g"].attrs["references"] == ["G"]
+
+
+def test_registry_persists_nested_schemas_in_one_transaction(tmp_path):
+    path = tmp_path / "registry.sqlite"
+    outer = Simplex("outer", {"lemma": theorem(), "goal": Role("result", KIND_GOAL)})
+    with SchemaRegistry(path) as registry:
+        registry.set_simplex(outer)
+        registry.set_simplex(outer)
+        assert registry.info() == {"roles": 5, "simplices": 2, "slots": 6}
+    with SchemaRegistry(path) as registry:
+        assert registry.get_simplex("schema:outer").as_dict() == outer.as_dict()
+        leaf = slot_key(slot_key("schema:outer", "lemma"), "g")
+        assert registry.find_by_roles([leaf], match_all=True) == [
+            "schema:outer", slot_key("schema:outer", "lemma")]
+
+
+def test_same_names_in_different_theorems_are_scoped():
+    with SchemaRegistry() as registry:
+        registry.set_simplex(theorem("first"))
+        registry.set_simplex(theorem("second"))
+        first_group = slot_key("schema:first", "G")
+        assert registry.find_by_roles([first_group]) == ["schema:first"]
+        assert registry.get_role(first_group).name == "group"
+        assert registry.slots("schema:first")["G"] != registry.slots("schema:second")["G"]
+
+
+def test_explicit_reuse_does_not_equate_local_bindings_or_multiplicity():
+    group = Role("group")
+    schema = Simplex("isomorphism", {"left": group, "right": group,
+                                    "goal": Role("equivalence", KIND_GOAL)})
+    with SchemaRegistry() as registry:
+        registry.set_role(group, "role:group")
+        registry.set_simplex(schema, role_keys={"left": "role:group", "right": "role:group"})
+        assert registry.slots("schema:isomorphism")["left"] == "role:group"
+        assert registry.find_solvable(["role:group"]) == []
+        assert registry.find_solvable([slot_key("schema:isomorphism", "left")]) == []
+        candidate = registry.find_solvable([slot_key("schema:isomorphism", x) for x in ["left", "right"]])
+        assert candidate[0]["target_slots"] == [slot_key("schema:isomorphism", "goal")]
+    instance = SimplexInstance(schema, {"left": "C2", "right": "C3"})
+    assert instance.facts["left"].value != instance.facts["right"].value
+    assert not instance.is_completed()
+    instance.resolve("goal", "a supplied result, not checked by the registry")
+    assert instance.is_completed()
+
+
+def test_premise_is_required_and_known_goal_is_not_a_missing_target():
+    with SchemaRegistry() as registry:
+        registry.set_simplex(theorem())
+        inputs = [slot_key("schema:t", alias) for alias in ["G", "g", "finite"]]
+        assert registry.find_solvable(inputs[:-1]) == []
+        assert registry.find_solvable(inputs)[0]["structural_candidate_only"]
+        assert registry.find_solvable(inputs + [slot_key("schema:t", "goal")]) == []
+
+
+def test_failed_write_rolls_back_every_child():
+    with SchemaRegistry() as registry:
+        registry.set_role(Role("incompatible"), "role:shared")
+        before = registry.info()
+        with pytest.raises(ValueError, match="does not match"):
+            registry.set_simplex(theorem(), role_keys={"goal": "role:shared"})
+        assert registry.info() == before
+        assert registry.get_simplex("schema:t") is None
+
+
+def test_cyclic_nesting_is_rejected_without_partial_write():
+    schema = Simplex("cycle", {"a": Role("a"), "b": Role("b")})
+    schema.roles["b"] = schema
+    with SchemaRegistry() as registry:
+        with pytest.raises(ValueError, match="cyclic"):
+            registry.set_simplex(schema)
+        assert registry.info() == {"roles": 0, "simplices": 0, "slots": 0}
+
+
+def test_keys_are_immutable_and_reuse_map_cannot_silently_change():
+    with SchemaRegistry() as registry:
+        registry.set_role(Role("G"), "role:G")
+        with pytest.raises(ValueError, match="different content"):
+            registry.set_role(Role("H"), "role:G")
+        schema = theorem()
+        registry.set_simplex(schema)
+        registry.set_role(schema.roles["G"], "role:shared")
+        with pytest.raises(ValueError, match="cannot change"):
+            registry.set_simplex(schema, role_keys={"G": "role:shared"})
+        assert registry.search_roles("%") == []
+        assert registry.search_roles("group", limit=1)[0]["role"]["name"] == "group"
+
+
+def test_instance_constraints_unknown_slots_and_invalid_references():
+    role = Role("parity", choices=["even", "odd"])
+    with pytest.raises(ValueError, match="not allowed"):
+        Fact(role, "prime")
+    schema = Simplex("pair", {"input": role, "goal": Role("result", KIND_GOAL, choices=[True])})
+    instance = SimplexInstance(schema, {"input": "even"})
+    with pytest.raises(ValueError, match="not allowed"):
+        instance.resolve("goal", False)
+    with pytest.raises(ValueError, match="declared"):
+        SimplexInstance(schema, {"unknown": "value"})
+    with pytest.raises(ValueError, match="references"):
+        Simplex("invalid", {"x": Role("x", attrs={"references": ["missing"]}), "y": Role("y")})
+    with pytest.raises(ValueError, match="name"):
+        Role(" ")
+    with pytest.raises(ValueError, match="sequence"):
+        Role("choice", choices="even")
+    with SchemaRegistry() as registry, pytest.raises(ValueError, match="Simplex object"):
+        registry.set_role(Role("fake", "simplex"))
+
+
+def test_pilot_materialization_keeps_partial_lean_projection_explicit():
+    import importlib.util
+    from pathlib import Path
+
+    path = Path(__file__).resolve().parents[1] / "experiments/P0-pilot/build_schemas.py"
+    spec = importlib.util.spec_from_file_location("build_schemas", path)
+    builder = importlib.util.module_from_spec(spec)
+    spec.loader.exec_module(builder)
+    items = [{"id": "closed", "lean_code": "theorem t : True := trivial"}]
+    assessment = {"records": [{"id": "closed", "blind_id": "P01", "source": {
+        "roles": [{"kind": "object", "symbols": ["G"], "description": "group"},
+                  {"kind": "goal", "description": "A synthetic claim"}]}}]}
+    with SchemaRegistry() as registry:
+        index, snapshots = builder.build(items, assessment, {"P01": "closed"}, registry)
+        assert registry.info()["simplices"] == 1
+        assert index[0]["source_status"] == "unreviewed_annotation_seed"
+        assert index[0]["lean_schema"] is None
+        assert index[0]["lean_status"] == "insufficient_projected_roles"
+        assert snapshots[0]["lean_projection"]["roles"][0]["kind"] == "goal"
+        with pytest.raises(ValueError, match="exactly once"):
+            builder.build(items, {"records": []}, {"P01": "closed"}, registry)