feat: add external solver replay artifacts

README.md

@@ -29,7 +29,7 @@ Noetheris does not claim quantum advantage, does not assess deployed cryptograph
 | --- | --- |
 | Structural IR validation and hashing | `tests/test_structural_ir.py`, `examples/structural_ir/*.json`, `docs/results/compiled_qubo_solution.json` |
 | QUBO/Ising energy preservation | `tests/test_qubo.py`, `examples/qubo_ising_qaoa.py`, `docs/results/qaoa_hamiltonian_report.json` |
-| D-Wave/Ocean boundary | `tests/test_optional_integrations.py`, `tests/test_external_examples.py`, `examples/dwave_ocean_exchange.py`, `docs/results/compiled_qubo_solution.json`, `docs/dwave_mapping.md` |
+| D-Wave/Ocean boundary | `tests/test_optional_integrations.py`, `tests/test_external_examples.py`, `examples/dwave_ocean_exchange.py`, `examples/external_solver_replay.py`, `docs/results/compiled_qubo_solution.json`, `docs/results/external_solver_replay_examples.json`, `docs/dwave_mapping.md` |
 | IBM/Qiskit oracle boundary | `tests/test_circuits.py`, `tests/test_optional_integrations.py`, `tests/test_external_examples.py`, `examples/qiskit_oracle_export.py`, `docs/results/oracle_truth_table.json` |
 | Certificate replay | `tests/test_certificates.py`, `examples/example_energy_certificate.json`, `docs/results/invariant_witness.json` |
 | CV/GKP diagnostics | `tests/test_cv.py`, `examples/cv_gkp_stabilizer_diagnostics.py`, `docs/results/cv_gkp_diagnostic_certificate.json` |
@@ -81,6 +81,7 @@ python3 examples/threshold_policy_analysis.py
 python3 examples/certificate_validation.py
 python3 examples/qubo_ising_qaoa.py
 python3 examples/dwave_ocean_exchange.py
+python3 examples/external_solver_replay.py
 python3 examples/qiskit_oracle_export.py
 python3 examples/saga_failure_semantics.py
 python3 examples/cv_fock_truncation_diagnostics.py
@@ -142,7 +143,7 @@ The local compiler emits symbolic gates, truth tables, cost metrics, reversibili
 
 ## Certificates
 
-Optimization and diagnostics emit deterministic certificate objects containing problem hashes, compiled model hashes where available, selected variables, witnesses, energy terms, satisfied and violated constraints, proof obligations, reproducibility metadata, and canonical fingerprints. Certificates fail closed: arithmetic mismatches, status inconsistencies, violated constraints, and nondeterministic timestamp strategies are rejected.
+Optimization and diagnostics emit deterministic certificate objects containing problem hashes, compiled model hashes where available, selected variables, witnesses, energy terms, satisfied and violated constraints, proof obligations, reproducibility metadata, and canonical fingerprints. Certificates fail closed: arithmetic mismatches, status inconsistencies, violated constraints, nondeterministic timestamp strategies, and inconsistent external replay evidence are rejected.
 
 ## Benchmarks
 

docs/dwave_mapping.md

@@ -69,8 +69,18 @@ External solver samples are treated as untrusted witnesses. Replay must check:
 - solver metadata;
 - embedding metadata when a hardware or hybrid run supplies it.
 
+The replay artifact schema is `noetheris.external_solver_replay.v1`. It records the candidate id, submitted and expected hashes, BINARY assignment domain, missing or unknown variables, reported energy, recomputed local energy, energy difference, tolerance, solver metadata, embedding metadata, rejection reasons, and an artifact hash. Accepted candidates have `status: "verified"` and an empty rejection list. Rejected candidates carry structured reason codes such as `problem_hash_mismatch`, `compiled_model_hash_mismatch`, `assignment_missing_variables`, `assignment_unknown_variables`, `reported_energy_mismatch`, `solver_metadata_malformed`, and `embedding_metadata_malformed`.
+
 Local baselines use `embedding_status: "not_requested"` and `embedding: null`. Hardware embedding, chain strength, anneal parameters, chain-break fraction, solver topology, and sample provenance must come from an actual external run and are never inferred by Noetheris.
 
+The deterministic replay example is:
+
+```bash
+python3 examples/external_solver_replay.py
+```
+
+It emits one accepted candidate and multiple rejected candidates. The local replay artifact is the verification authority; solver metadata is recorded evidence supplied by the external tool, not a Noetheris assessment of embedding quality.
+
 ## No Hardware Claim
 
 The repository runs without Ocean, D-Wave credentials, or paid APIs. The v0.1.0 benchmark artifacts are local replay baselines. They are not hardware comparisons and do not imply quantum speedup.

docs/dwave_relevance.md

@@ -20,7 +20,7 @@ Structural IR
 - Deterministic seeded annealing baseline for local experiments.
 - Structured D-Wave exchange payload with schema version and model hash.
 - Optional `dimod.BinaryQuadraticModel` construction when Ocean is installed.
-- External-sample replay against `problem_hash`, `compiled_model_hash`, assignment variables, and reported energy.
+- External-sample replay artifacts against `problem_hash`, `compiled_model_hash`, assignment variables, reported energy, solver metadata, and embedding metadata.
 
 ## What Is Deliberately Outside v0.1.0
 
@@ -31,7 +31,7 @@ Structural IR
 - Advantage or Advantage2 performance claims.
 - Hybrid solver benchmarking.
 
-These fields are represented as explicit metadata boundaries. Local artifacts use `embedding_status: "not_requested"`. A future external run must supply solver id, topology, embedding, chain settings, anneal parameters, sample counts, and chain-break statistics before Noetheris can replay the sample as a documented external witness.
+These fields are represented as explicit metadata boundaries. Local artifacts use `embedding_status: "not_requested"`. A future external run must supply solver id, topology, embedding, chain settings, anneal parameters, sample counts, and chain-break statistics before Noetheris can replay the sample as a documented external witness. Noetheris records that metadata but does not infer hardware embedding quality locally.
 
 ## Minimal Local Export
 
@@ -64,6 +64,7 @@ result = replay_external_solution(
     compiled_model_hash=compiled_problem.compiled_model_hash,
 )
 assert result["status"] == "verified"
+assert result["verification_authority"] == "noetheris.local_replay"
 ```
 
 The replay relation is the trust boundary: a solver result is useful only after local deterministic verification.

docs/formal_certificates.md

@@ -27,7 +27,7 @@ Certificates include:
 
 ## Validation
 
-Validation recomputes energy contributions, recomputes total energy, checks constraint polarity, rejects violated constraints for accepted certificates, checks optional problem hash, checks status consistency, and rejects nondeterministic timestamp strategies.
+Validation recomputes energy contributions, recomputes total energy, checks constraint polarity, rejects violated constraints for accepted certificates, checks optional problem hash, checks status consistency, rejects nondeterministic timestamp strategies, and rejects inconsistent external replay evidence embedded in the energy breakdown.
 
 ## Replay
 
@@ -38,6 +38,8 @@ python3 -m noetheris.certificates.replay examples/example_energy_certificate.jso
 
 Replay emits validation status and certificate fingerprint. Stronger model-specific replay is represented by compiled model hashes and strict QUBO energy evaluation in the compiler layer.
 
+When a certificate includes `external_replay_artifact`, `external_replay`, `external_sample_replay`, or `external_solver_replay` in `energy_breakdown`, that artifact must use schema `noetheris.external_solver_replay.v1`, have `status: "verified"`, have local energy recomputation enabled, match the certificate problem hash, match the certificate compiled-model hash when present, carry no rejection reasons, and pass artifact-hash verification. Any violation rejects the certificate.
+
 ## Formal Surface
 
 Lean models a simplified certificate-validity predicate and small true lemmas. The executable Python/Rust validators are the release enforcement path; Lean artifacts define reviewable kernels rather than whole-repository proofs.

docs/limitations.md

@@ -9,6 +9,7 @@ Noetheris v0.1.0 is a bounded research kernel. Its boundaries are part of the sc
 - QUBO penalty calibration remains a modeling responsibility; weak penalties can encode the wrong preference order.
 - Circuit oracle compilation is limited to small Boolean predicates and symbolic reversible circuits.
 - Optional Qiskit and D-Wave adapters are export boundaries, not default hardware benchmark paths.
+- External solver metadata and embedding metadata are recorded as supplied evidence. Noetheris verifies hashes, assignment domains, and energies locally; it does not infer hardware embedding quality.
 - CV/GKP diagnostics use finite Fock cutoffs. Boundary artifacts are measured and certified, not ignored.
 - Approximate GKP states in this release are finite-dimensional diagnostic objects, not production fault-tolerant logical states.
 - Lean and TLA+ artifacts cover simplified kernels and scenario models, not the entire implementation.

docs/results/README.md

@@ -12,6 +12,7 @@ python3 scripts/generate_release_results.py
 - `release_evidence_index.json`: index of generated evidence files.
 - `invariant_witness.json`: bounded consensus-safety counterexample witness with certificate data.
 - `compiled_qubo_solution.json`: Structural IR compilation, exact QUBO solution, energy breakdown, D-Wave exchange payload, and local replay of a solver sample.
+- `external_solver_replay_examples.json`: accepted and rejected external-candidate replay artifacts with explicit hash, assignment-domain, energy, and metadata rejection reasons.
 - `pqc_migration_plan.json`: migration optimizer output, residual risk, dependency analysis, QUBO model, and certificate.
 - `oracle_truth_table.json`: Boolean predicate truth table, reversible compute/apply/uncompute metrics, and QASM-like text.
 - `qaoa_hamiltonian_report.json`: QUBO-to-Ising lowering and exact local QAOA p=1 statevector check.
@@ -20,4 +21,4 @@ python3 scripts/generate_release_results.py
 
 ## Interpretation
 
-These files are release evidence, not hardware benchmark claims. The D-Wave payload is a BINARY QUBO exchange representation; any external solver sample must be replayed locally before it is trusted. The Qiskit-facing oracle artifacts are small-predicate circuit mappings; they do not claim backend advantage. The CV/GKP certificate uses finite Fock truncation and records boundary effects explicitly.
+These files are release evidence, not hardware benchmark claims. The D-Wave payload is a BINARY QUBO exchange representation; any external solver sample must be replayed locally before it is trusted. Solver and embedding metadata are recorded as externally supplied evidence; local replay does not infer hardware embedding quality. The Qiskit-facing oracle artifacts are small-predicate circuit mappings; they do not claim backend advantage. The CV/GKP certificate uses finite Fock truncation and records boundary effects explicitly.

docs/results/compiled_qubo_solution.json

@@ -255,28 +255,58 @@
     }
   },
   "external_sample_replay": {
+    "artifact_hash": "sha256:d1888865d53521446dd39af85d8820ba966ce263e239c921edeeea4911dbecd8",
     "assignment": {
       "path_0": false,
       "path_1": false,
       "path_2": false,
       "path_3": false,
       "path_4": true
     },
+    "assignment_domain": {
+      "expected_variables": [
+        "path_0",
+        "path_1",
+        "path_2",
+        "path_3",
+        "path_4"
+      ],
+      "invalid_value_variables": [],
+      "missing_variables": [],
+      "provided_variables": [
+        "path_0",
+        "path_1",
+        "path_2",
+        "path_3",
+        "path_4"
+      ],
+      "unknown_variables": [],
+      "vartype": "BINARY"
+    },
+    "candidate_id": "sha256:7cdf563bf9035bbbb198dfba8a6995386625014fa84bd49a2e16eae96ffa4c1e",
     "compiled_model_hash": "sha256:eca1158e2ddfdfe196775a49b8ffbcd46a23a33bf61e18e8229dcda0174612d2",
     "embedding_metadata": {
       "embedding": null,
       "embedding_status": "not_requested"
     },
     "energy": 10.0,
+    "energy_difference": 0.0,
     "energy_recomputed": true,
     "problem_hash": "sha256:3cddd03a5881f3b71ba61c3b063f96ec47dba9f9160a634392929eca618d095f",
     "reasons": [],
+    "recomputed_energy": 10.0,
+    "rejection_reasons": [],
     "reported_energy": 10.0,
-    "solver_boundary": "external solver output is an untrusted witness until replay verifies it",
+    "schema": "noetheris.external_solver_replay.v1",
+    "solver_boundary": "external solver output is an untrusted witness until deterministic local replay verifies hashes, domain, and energy",
     "solver_metadata": {
       "source": "local_exact_solver"
     },
-    "status": "verified"
+    "status": "verified",
+    "submitted_compiled_model_hash": "sha256:eca1158e2ddfdfe196775a49b8ffbcd46a23a33bf61e18e8229dcda0174612d2",
+    "submitted_problem_hash": "sha256:3cddd03a5881f3b71ba61c3b063f96ec47dba9f9160a634392929eca618d095f",
+    "tolerance": 1e-09,
+    "verification_authority": "noetheris.local_replay"
   },
   "solution": {
     "assignment": {