proof-obligation-registry

# Proof Obligation Registry ## Purpose Extract, merge, and maintain a persistent proof state whose omissions and stale evidence are mechanically visible. ## Inputs Problem statement, source artifact paths/hashes, optional draft, domain profile, optional prior registry, strictness, and run workspace. ## Procedure 1. Inventory definitions, quantified claims, external theorems, algorithms/reductions, complexity claims, and document references. 2. Assign stable IDs; merge prior records by ID and preserve history. 3. Build the hypothesis ledger and connect each use. 4. Build the use-site audit with exact substitutions, side conditions, signs, domains, and path tuples. 5. Instantiate every profile boundary row; require evidence or a reasoned N/A. 6. Populate random-distribution and convergence ledgers when expectations/limits occur. 7. Populate exact-arithmetic/bit-complexity rows for oracle or rational reductions. 8. Populate theorem-reference targets and uses. 9. For every selected module, populate each ledger named by `profile.requiredLedgers`, link at least one record to that module's applicable obligation, and close every such record before publication; an empty required ledger fails. 10. Mark uncertain records open; never self-certify them verified. 11. Run `python validators/validate_registry.py ...` as an `expectedExitCode: 0` shell gate; publication always uses `--strict publication`. ## Failure handling - Missing source/hash: stop before extraction. - Prior required ID removed: restore it as stale and trigger scope breakpoint. - Rejection: append reason/history, reopen affected records, refine, and rerun validation. - Unjustified N/A, unresolved dependency, or verified-without-evidence: hard failure. ## Output Registry JSON, edge-matrix JSON, unresolved IDs, scope changes, and validation transcript. Agent prose cannot override the gate.