[Wenbobobo]

Summary

• preserve the Phase 1 Builder-Prover evidence architecture: versioned contracts, distinct mathematical/formal/execution graphs, immutable bundles, lease/fencing/CAS recovery, and read-only evidence views
• retain the source-free iFEM census, triage, risk-routing, 21-intent queue, private seed, 27-coordinate ledger, and ModelWork sidecar without promoting synthetic evidence into statement fidelity
• add a bounded first-case formalizer -> fidelity reviewer -> cheating supervisor chain with one durable attempt per stage, strict predecessor gating, private CAS recovery, and 24 out-of-scope coordinates kept pending
• bind every executable chain to a write-once private run-scope record covering the exact public plan, private seed manifest, canonical 27-coordinate run, fixed selection rule, and ordered three-coordinate commitment
• keep Builder statement fidelity, frozen-contract admission, Prover proof search, Lean kernel verification, and release authority as separate gates

Current candidate

Candidate: 1521c4cad4483e81b5e5a79a00e21d64fe635ba8

• clean staged-candidate full gate: 2,247 passed, 13 explicit cache/OS/OCI skips, 0 failed
• scope-binding module: 19 passed
• role-chain + legacy runner + private ledger + ModelWork sidecar: 83 passed
• independent adversarial review reproduced and fixed a plan/private-run identity gap and a read-back/dispatch TOCTOU; final review found no remaining P0/P1
• Ruff: 342 files formatted; lint passed
• strict mypy: contracts, control plane, Builder (46 modules), Prover, Dashboard API, benchmarks/scripts (162 modules), and Library passed
• uv lock, Library lock, Mathlib source lock, provider guard, release evidence, and SPDX SBOM checks passed
• staged/current candidate secret scan: 665 files; reachable-history scan: 1,365 blob/path pairs
• release inventory: 8d6865f1e066e04ac0f1212b35b4223c9e941973570b0fa8cd94efb91ff48e80
• SPDX 2.3 SBOM: d0403723efec1de28105d527363766d34fce58cad63a6e9c1906ee7df1ec3061
• GitHub Actions run 30679203842: Ubuntu/Windows Python-policy and Ubuntu/Windows Dashboard jobs all passed

Scope and recovery boundary

The credential-free plan binds the execution protocol, role order, prompt/schema hashes, cardinalities, and budget ceilings. It deliberately cannot bind a CSPRNG-selected private case before the seed exists.

Before any provider dispatch, the operator persists and reads back an exact private run-scope binding. Every actual sidecar/provider entry reloads it; resume reloads it before recovery; final evidence reloads it before and after state/control-plane checks. Missing, replaced, mixed-root, or rehashed scope state fails closed as private_state_unavailable and cannot yield settled or recovered.

Public output contains only the opaque scope-binding hash. It contains no case ID, coordinate hash, source text, prompt, raw response, model identity, path, credential, or combined score. All authority remains false, machine disposition remains abstain, and Builder freeze / Prover handoff remain forbidden.

Remaining gates

This PR remains deliberately draft / no-RC. It does not claim source-rights closure, textbook fidelity, semantic approval, held-out independence, a three-role real-provider result, a frozen Builder statement, an accepted FATE proof, production signer custody, production readiness, or an Open Problem result.

The next Phase 1 evidence task is a retained, gateway-bound independent OCI execution receipt with an executor-free offline replay path. The next authority-bearing vertical still requires one exact rights-cleared source span, independent semantic admission, an immutable frozen StatementContract revision, unchanged Prover bundle execution, authoritative OCI/Lean verification, gateway evidence, and recovery-bound completion.

[Wenbobobo]

Candidate 705f2c1 remote validation

GitHub Actions run 30612841190 completed with all four jobs passing:

• Dashboard UI, Ubuntu 24.04: 30s
• Dashboard UI, Windows 2022: 1m05s
• Python and policy, Ubuntu 24.04: 3m08s
• Python and policy, Windows 2022: 7m55s

The Python jobs performed a clean locked uv sync --all-packages --all-groups on each OS before running the repository CI gate. This independently confirms cross-platform installation and policy compatibility for the pushed commit.

The PR remains draft/no-RC. These checks do not close semantic admission, source rights, authoritative signer/gateway execution, the 21-node iFEM classification, closure-policy review, or Builder-to-Prover promotion.