Add semantic simplex schemas, review page and resumable pilot recovery #9

Merged

Zayden-Jung merged 5 commits from codex/simplex-registry into main 2026-10-28 13:55:56 +00:00

Conversation 0 Commits 5 Files Changed 17

+11783 -56

codex-bot commented 2026-10-28 13:28:00 +00:00

Collaborator

Copy Link

Copy Source

Consolidates the pilot recovery changes from PR #6 with the semantic simplex schema and project review page in this PR. Both branches' commits are preserved by merge commit 3453d5c; no shared history was rewritten. PR #6 is closed as superseded; its branch and commits are retained.

The pilot originally lacked source-inclusive inputs and later stopped producing complete detector results when DashScope returned Arrearage. The recovery now stops immediately on billing/authentication failures, preserves successful components of partial items, resumes only missing components, and records cumulative request usage and hashes. The Qwen run remains at 42 complete items plus 23 incomplete items, with 131 requests consumed; no paid calls were resumed and no gate decision was issued.

The owner defines simplex as a semantic multi-role relation pattern joining objects, assumptions and a conclusion. Add scoped role definitions/occurrences, explicit fact/goal bindings, JSON/SQLite persistence, deliberate reuse, nesting, search and structural candidate retrieval. Readiness is not a proof or value-unification engine. Materialize the separate frozen GPT-assisted diagnostic into 65 source seeds and 50 Lean seeds; keep 15 insufficient Lean projections explicit. Existing annotations and evaluations are not changed or mixed across models.

Include the owner-approved, self-contained 65-item schema review at docs/reviews/simplex-schemas.html, linked from the README and reproducible with --review-page. It publishes semantic role annotations and Lean signature text; textbook paragraphs, source-inclusive inputs, full judgment explanations and SQLite snapshots remain gitignored.

The only merge conflict was experiments/P0-pilot/README.md; retain Qwen execution status, GPT diagnostic, schema registry and review instructions together. Update the recovery report/audit to point to this consolidated delivery while keeping its historical run facts.

Validation: 165 offline unit tests, repository-wide Ruff and git diff --check passed on the combined branch. Earlier full-cohort materialization/roundtrip checks and HTML coverage checks passed. Combined CI #51 (API run ID 458) passed Python checks and real Lean verification for commit 3453d5c on ubuntu24.04-x64-lean4.35 (runner 7). The image job was skipped for this PR. Checks: https://gitea.entroia.com/Zayden-Jung/lean-bench/actions/runs/458 No local Lean/Docker build or new model call was performed.

Limitations remain explicit: source annotations are non-independent and unreviewed, role references are partial symbol/syntax candidates, no cross-theorem identity is inferred, and the Qwen gate is incomplete. The schemas are a foundation rather than a validated prover or Phase 1 result.

Please review and merge this single PR manually; no automatic merge is enabled.

Consolidates the pilot recovery changes from PR #6 with the semantic simplex schema and project review page in this PR. Both branches' commits are preserved by merge commit 3453d5c; no shared history was rewritten. PR #6 is closed as superseded; its branch and commits are retained. The pilot originally lacked source-inclusive inputs and later stopped producing complete detector results when DashScope returned Arrearage. The recovery now stops immediately on billing/authentication failures, preserves successful components of partial items, resumes only missing components, and records cumulative request usage and hashes. The Qwen run remains at 42 complete items plus 23 incomplete items, with 131 requests consumed; no paid calls were resumed and no gate decision was issued. The owner defines simplex as a semantic multi-role relation pattern joining objects, assumptions and a conclusion. Add scoped role definitions/occurrences, explicit fact/goal bindings, JSON/SQLite persistence, deliberate reuse, nesting, search and structural candidate retrieval. Readiness is not a proof or value-unification engine. Materialize the separate frozen GPT-assisted diagnostic into 65 source seeds and 50 Lean seeds; keep 15 insufficient Lean projections explicit. Existing annotations and evaluations are not changed or mixed across models. Include the owner-approved, self-contained 65-item schema review at docs/reviews/simplex-schemas.html, linked from the README and reproducible with --review-page. It publishes semantic role annotations and Lean signature text; textbook paragraphs, source-inclusive inputs, full judgment explanations and SQLite snapshots remain gitignored. The only merge conflict was experiments/P0-pilot/README.md; retain Qwen execution status, GPT diagnostic, schema registry and review instructions together. Update the recovery report/audit to point to this consolidated delivery while keeping its historical run facts. Validation: 165 offline unit tests, repository-wide Ruff and git diff --check passed on the combined branch. Earlier full-cohort materialization/roundtrip checks and HTML coverage checks passed. Combined CI #51 (API run ID 458) passed Python checks and real Lean verification for commit 3453d5c on ubuntu24.04-x64-lean4.35 (runner 7). The image job was skipped for this PR. Checks: https://gitea.entroia.com/Zayden-Jung/lean-bench/actions/runs/458 No local Lean/Docker build or new model call was performed. Limitations remain explicit: source annotations are non-independent and unreviewed, role references are partial symbol/syntax candidates, no cross-theorem identity is inferred, and the Qwen gate is incomplete. The schemas are a foundation rather than a validated prover or Phase 1 result. Please review and merge this single PR manually; no automatic merge is enabled.

codex-bot added 1 commit 2026-10-28 13:28:01 +00:00

feat(schema): persist and instantiate scoped multi-role relation schemas 29fe3e1aa5

codex-bot added 1 commit 2026-10-28 13:42:51 +00:00

docs(schema): track the 65-item schema review page 4eee78be09

codex-bot added 3 commits 2026-10-28 13:48:30 +00:00

fix(pilot): preserve partial results and stop on provider billing errors 16e49df764

docs(pilot): link the recovery audit to the follow-up PR 1c265609d5

Merge pilot recovery into the semantic simplex schema delivery 3453d5c961

codex-bot changed title from Add persistent semantic simplex schemas with scoped role bindings to Add semantic simplex schemas, review page and resumable pilot recovery 2026-10-28 13:49:49 +00:00

codex-bot referenced this pull request 2026-10-28 13:50:59 +00:00

Superseded by #9: Preserve P0 partial results and report the billing interruption #6

Zayden-Jung merged commit a80448ae36 into main 2026-10-28 13:55:56 +00:00

Sign in to join this conversation.

Reviewers

No Reviewers

Labels

No items

No Label

Milestone

No items

No Milestone

Projects

Clear projects

No project

Assignees

Clear assignees

claude-bot codex-bot yilin-codex-bot Zayden-Jung

No Assignees

1 Participants

Notifications

Subscribe

Due Date

No due date set.

Dependencies

No dependencies set.

Reference: Zayden-Jung/lean-bench#9