Architecture 9 Cursor strategy and isolated OProver residency

[FluffyAIcode]

Summary

• cut proof orchestration over to Architecture 9 with Cursor SDK advisory strategy and host-owned, content-addressed plan compilation
• add target-context isolation, exact provider provenance, and typed DEFINITION_RESOLUTION_PLAN remediation when no elaborated theorem exists
• reconcile Gemma residency by live executable/model/revision/health/start generation, rejecting stale owners and PID reuse
• add durable target-bound report provenance, exclusive single-use resume leases, and signed resume certificates
• prohibit Proof Search and OProver for definition-remediation certificates until a Research Contract exists
• dispatch consumed definition-remediation certificates directly to the host-owned Definition Resolution gate
• exhaust every configured target-interface, Mathlib, theorem-card, evidence, history, publication, typed-synthesis, and rewrite source before issuing a mathematical terminal blocker

Safety properties

• model memo can select only registered short IDs and cannot set plan or interface content
• planning-only proof skeletons remain infeasible
• remediation certificates route only to DEFINITION_RESOLUTION and explicitly set proof_search_allowed=false and oprover_allowed=false
• certified Definition Resolution stops the current turn before generic model-role dispatch
• underspecified root targets receive a content-addressed exhaustion certificate, typed backjump, and idempotent durable quarantine
• credentials remain Keychain-backed and are never persisted or passed in process arguments
• no candidate, ledger, runtime state, logs, snapshots, caches, weights, model bundles, environment files, or OpenMontage content is included

Test plan

• exact Architecture 9 interface/remediation regression suite: 237 passed / 9 skipped
• mandatory local CI: 1,343 passed / 10 skipped; 100% canonical coverage
• Lean build: 2,793 jobs
• Python compile and staged/unstaged diff checks
• authenticated read-only Cursor Strategy smoke outside CI using exact model gpt-5.6-sol
• all eight GitHub checks green on e8bf5ac
• diff secret/forbidden-artifact scan

Production fixture coverage

• stale residency PID reconciliation, dead identity, and PID reuse rejection
• planning-only to typed remediation without theorem fabrication
• remediation feasibility, host selection, and provider provenance
• report provenance plus lease missing/stale/tampered/conflict handling
• signed certificate issuance/consumption and replay rejection
• four RH-C1 interface schemas with host-only feasibility and circularity guards
• complete reliable-source status inventory and stable exhaustion hashing
• typed root backjump/quarantine and replay idempotency
• Definition Resolution policy keeps OProver unloaded and Proof Search inaccessible
• crash/restart/replay/idempotency paths

Production result

Terminal condition B was reached on RH-C1. Cursor gpt-5.6-sol ranked TI-DISTINGUISH-FUNCTIONS, but every registered interface/rewrite schema failed host feasibility. The pinned Mathlib declarations were verified; all other configured sources returned explicit target-bound exhaustion statuses. The resulting exhaustion hash is 243595a4092b60ea5f5bcfb633052321dab5b90b9313666759a79cb5f92045a1; RH-C1 is quarantined at ledger v95 with backjump ROOT_UNAVAILABLE. Proof Search and OProver were never opened. The PR must not be merged automatically.

Made with Cursor

Architecture 9 runtime hardening (dc44e19)

• reuse flags now derive only from reusable, validated artifact refs bound to the current role, target/context, candidate/plan, ledger/environment, dependency DAG, and content hash; stale or absent refs fail closed with diagnostics
• benchmark completion now waits with bounded backoff for the exact run ID/generation and terminal report version; transient running is not evaluated, and timeout is typed BENCHMARK_FINALIZATION_TIMEOUT
• static CI audit rejects hardcoded production *_reused=true claims while classifying and allowing stable schema constants, typed event literals, tests, and fail-closed defaults
• regressions cover absent/valid/stale/mismatched Critic provenance, delayed completion, typed timeout, failed terminal reports, and concurrent-generation isolation
• local CI: 1,388 passed / 10 skipped, 100% canonical coverage; Lean build 3,148 jobs; frontend/API checks green
• production remained stopped and was not restarted; no proof run was launched

[cursor]

Bugbot is not enabled for your account, so this pull request was not reviewed.

Enable Bugbot in the Cursor dashboard to get automatic reviews on future PRs.

[FluffyAIcode]

Architecture 9 independent reconstruction follow-up is in commits 772d3a1 and 4113c89.

• Added source/environment/theorem-bound reconstruction packages that redact only the target proof body while preserving exact project compilation context.
• Added native OProver prompting, deterministic bounded Pass@K, iterative Lean feedback, robust fenced/plain parsing, isolated exact-project Lean verification, and explicit provider/no-candidate/Lean-rejected/search-exhausted/verified statuses.
• Added four canaries and mocked tests for context preservation, proof non-leakage, parsing, deterministic attempts, feedback, classification, and source immutability.
• Q4 hardware acceptance: 4/4 canaries independently verified on attempt 1. Route Pass@2: 2/8 independently verified (riemannHypothesis_of_allJensenHyperbolic, riemannXiGenusOneHadamardRepresentation); 6/8 search exhausted with per-attempt evidence retained. Existing Lean verification remains unchanged and no theorem was invalidated.
• Measured 45–49k prompt slices timed out at the adapter boundary; 12k bounded slices completed. Full 72–279k Lean compilation prefixes remained intact. Defaults now use the measured 12k/600s bounds.
• OProver unloaded and Gemma/fleet restored healthy. Production ledger unchanged; no certification signer is configured, and the conditional bridge remains conditional.

All PR checks are green. No merge performed.