Merge pilot recovery into the semantic simplex schema delivery

Reviewed-on: #8

.gitea/workflows/env-probe.yml

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

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

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

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

@@ -70,7 +70,9 @@ hash and the frozen-label hash did not change during the offline audit.
 Ruff and diff checks passed. These checks did not compile Lean or build Docker locally.
 The initial PR revision passed Python tests and real Lean validation on
 `ubuntu24.04-x64-lean4.35`, runner 7, in [CI #427](https://gitea.entroia.com/Zayden-Jung/lean-bench/actions/runs/427).
-The image job was skipped by the PR workflow. The recovery revision's remote result is reported separately in the PR checks.
+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.

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/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

@@ -54,12 +54,40 @@ Labeling must be finished before anyone opens `results.jsonl`.
   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.
-  Only verdicts, abstract annotation notes, hashes and text-free summaries belong in Git.
+  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/.
 
-## Current execution
+## 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/results/execution.json

@@ -66,6 +66,7 @@
     "remote_runner_tag": "ubuntu24.04-x64-lean4.35",
     "initial_remote_ci": "https://gitea.entroia.com/Zayden-Jung/lean-bench/actions/runs/427",
     "initial_remote_ci_status": "success; image job skipped for PR",
-    "recovery_remote_ci": "See follow-up PR #6 checks for the delivered head revision"
+    "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."
+  ]
+}

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_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)