Experiment ID P0. Spec, hypotheses, decision rule and costs: docs/experiments/P0-pilot.md. Registry of all experiments: docs/experiments/README.md.

Question: on the 65 existing items, does role alignment (passage simplex vs. Lean simplex) find unfaithful formalizations better than a single LLM judge, compile-only, or static lint?

Layout

data/      ignored by git: items.jsonl (copy of the 65 items), labelsheet.html, results.jsonl
           (all contain or paraphrase passages from a copyrighted book)
labels/    tracked: key.json (blind id -> item id, no text), labels.json (verdicts and error
           types only; do not paste passage text into the notes field)
results/   tracked: summary.json written by score.py (numbers only)

Steps

# Default exports omit source_text. Restore it from the matching private review.
python experiments/P0-pilot/prepare_items.py --items runs/p85-110/items.jsonl \
    --review runs/p85-110/review.json --out experiments/P0-pilot/data/items.jsonl
python experiments/P0-pilot/make_sheet.py --items experiments/P0-pilot/data/items.jsonl \
    --out experiments/P0-pilot/data --key-dir experiments/P0-pilot/labels --seed 7
# a person opens data/labelsheet.html, labels all 65 items, downloads labels.json into labels/
python experiments/P0-pilot/run_pilot.py --items experiments/P0-pilot/data/items.jsonl \
    --out experiments/P0-pilot/data/results.jsonl --dry-run
python experiments/P0-pilot/run_pilot.py --items experiments/P0-pilot/data/items.jsonl \
    --out experiments/P0-pilot/data/results.jsonl --labels experiments/P0-pilot/labels/labels.json
python experiments/P0-pilot/score.py --results experiments/P0-pilot/data/results.jsonl \
    --labels experiments/P0-pilot/labels/labels.json --key experiments/P0-pilot/labels/key.json \
    --summary experiments/P0-pilot/results/summary.json

Labeling must be finished before anyone opens results.jsonl.

Execution safeguards

Every item must have a nonempty source passage. prepare_items.py restores passages only when all exported fields match the archived review; the exported cohort and Lean code stay intact.
Freeze all labels before the paid run. The owner changed the labeler to the Codex assistant on 2026-10-28. These are AI labels, not human gold; see the metadata in labels/labels.json.
--max-calls counts actual HTTP attempts, including transport and JSON retries, cumulatively across resumes. The hard ceiling is 400. A reservation is saved before each request; an interrupted request may consume a reservation without a known response or token count.
Metadata is stored beside the output as results.meta.json. Model, endpoint, temperature, input hash, frozen-label hash and prompt hashes must match on resume. Usage is cumulative. A file lock prevents concurrent writers. A budget stop returns exit status 2.
Billing/authentication failures stop immediately. Resume retries only missing detector components, keeping both complete items and the successful side of partial items. Rows are replaced atomically. --audit-only reconciles saved completion counts and status without any API request.
The nominal successful path uses 130 calls (one source extraction and one judge per item); malformed replies and network retries may increase the actual count.
Scoring requires complete labels and results and no unresolved detector errors. The primary comparison is wrong versus faithful; minor drift is included as positive in the secondary analysis. The complementary-signal PARTIAL rule counts wrong items flagged by role alignment but missed by the judge. No threshold, concept table or detector prompt was tuned for these labels.
Raw passages, labeling HTML and model responses remain in the ignored data/ directory. Verdicts, abstract annotation notes, hashes and text-free summaries belong in Git; the owner-approved schema-only HTML review is also tracked separately under docs/reviews/.

Qwen execution snapshot

The 2026-10-28 run was blocked by DashScope Arrearage: 42 items are complete, 23 need 42 detector components, and 131 of the 400 request reservations have been consumed. The owner requested fixes and a report now, with paid resumption deferred. See docs/experiments/P0-execution-2026-10-28.md and results/execution.json. No gate decision has been issued. Restore provider billing before resuming the same run.

Separate GPT-assisted diagnostic

The owner requested a complete 65-item reassessment by the current GPT assistant on 2026-10-28. This is separate from the incomplete Qwen run: no outputs are mixed and neither the earlier labels nor Qwen files are overwritten. The assistant had prior exposure to the reference labels and Lean; this is not blind or independent validation. No GO/PARTIAL/NO-GO decision is issued.

See docs/experiments/P0-gpt-diagnostic.md for all counts, limitations, artifact locations and the offline replay command. The tracked results/gpt-diagnostic-*.json files contain only categorical/numeric outputs and audit metadata. The authored source structures, reasons and full review page stay in the ignored data/gpt-diagnostic/ directory.

Semantic simplex registry

The current 65-item annotation cohort is materialized as multi-role relation schemas: 65 source seeds, 50 Lean signature seeds and 15 explicitly incomplete Lean projections. See docs/simplex-schema.md for the data model, scoped identities, explicit role reuse, structural candidate queries, bindings and replay command. Private SQLite/JSON/HTML outputs stay under data/simplex-schemas-v1/; tracked results/simplex-schema-*.json files contain only counts, opaque keys, provenance hashes and coverage status. This does not change the frozen diagnostic or claim complete semantic extraction or proof verification.

The owner-approved schema-only HTML review is tracked at docs/reviews/simplex-schemas.html. Regenerate it with the builder's --review-page option; the raw inputs, full assessment explanations and SQLite snapshot remain gitignored.