Add a versioned installed proof-carrying exact-query API

[tugrapaydiner]

Scope

Stack this release-engineering checkpoint on draft PR #62 without changing faster-queries, main, the existing automatic engine policy, frozen benchmark evidence, packet formats, native ABI semantics, or research conclusions. No merge or package release is requested by this draft.

The proof-carrying exact-query engine previously lived only in experiments/compiled_query. This PR makes the same ABI-3 implementation available through a documented, versioned installed API while retaining the experiment sources and evidence.

Public contract

• spectra.exact, API version 1 and native ABI 3.
• Immutable ExactProblem construction and strict canonical SBC1/SBQ1 packet decoding.
• Persistent exact sessions and one-call prepared-bank execution with complete SAT witnesses or portable SBP1 contradiction proofs in SCQ2 output.
• Standard-library proof/output replay that does not load the native solver.
• Receipt-bound native loader covering source, compiler/options, Python identity, extension bytes, API and ABI.
• Bundled spectra/_native/exact_binary.cpp; the platform extension is built explicitly on first use rather than shipping an unverified prebuilt binary.
• spectra exact build, spectra exact verify, and updated spectra doctor CLI paths.
• Installed-wheel checker that rejects repository/ML/test dependency leakage and verifies two SAT plus one certified UNSAT decision.
• Dedicated API documentation, security/release guidance, public tests, and integration into the existing public-package contract.

Verification completed

Final cross-platform run: 38797065291.

• Linux x86 Python 3.11: source contracts and isolated installed wheel PASS.
• Linux x86 Python 3.13: source contracts and isolated installed wheel PASS.
• Native Linux ARM64 Python 3.13: source contracts and isolated installed wheel PASS.
• Windows x64/MSVC Python 3.13: 11 public + 156 research contracts PASS; wheel build/install/native execution PASS.
• UBSan: public and research exact contracts PASS.
• ASan + UBSan: public and research exact contracts PASS; leak detection disabled, so no LeakSanitizer claim.
• Release-readiness and workspace audits PASS locally.
• An isolated local wheel check confirms the JSON receipt survives outside the disposable native-build directory.

Two earlier failed workflow runs remain visible. The first loaded the unrelated repository training fixture because the dependency-light public tests were not isolated. The second completed all Windows API checks but failed while deleting a loaded .pyd; the final checker restores its working directory, preserves the requested receipt outside the temporary tree, and treats the Windows extension lock as process-lifetime cleanup.

Boundaries

This is release and portability progress, not a new speed result or algorithmic novelty claim. Native execution requires a supported host C++ compiler at explicit build time. The wheel contains source rather than an opaque prebuilt extension. The prior exposed synthetic timings, negative cells and automatic-policy limitations are unchanged. There is still no operator-defined workload, outside-team replication, maintained adoption, or independent priority determination.

The full public-package workflow is enabled for this stacked review and should be judged separately from the dedicated exact API matrix.