Add independent SageMath certificate validation

.github/workflows/ci.yml

@@ -46,3 +46,17 @@ jobs:
           --gate-policy competitive-compression
       - name: Package
         run: cargo package --allow-dirty
+
+  independent-oracle-validation:
+    name: independent Oracle validation
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v7
+      - uses: dtolnay/rust-toolchain@stable
+      - name: Reproduce every finite certificate row with SageMath
+        run: scripts/run_oracle_independent_validation.sh "$RUNNER_TEMP/oracle-evidence"
+      - name: Compare with published machine-readable results
+        run: >
+          python3 scripts/oracle_validation/compare_results.py
+          --expected validation/oracle-v0.4.1/evidence/results.json
+          --actual "$RUNNER_TEMP/oracle-evidence/results.json"

.gitignore

@@ -5,5 +5,6 @@
 .DS_Store
 *.profraw
 *.profdata
+__pycache__/
 
 captures/

CHANGELOG.md

@@ -4,6 +4,21 @@ All notable changes to QATQ are recorded here.
 
 ## Unreleased
 
+### Added
+
+- Added a pinned, network-disabled SageMath 10.6 implementation that separately
+  reproduces all 27 published binary Hamming and spherical Rankin certificate
+  rows without importing QATQ code or expected numeric answers.
+- Added a deterministic differential corpus with requests, certificates,
+  SHA-256 manifests, exact per-row comparisons, environment versions, and a CI
+  gate against the published machine-readable results.
+
+### Changed
+
+- Distinguished certificates that are checkable by QATQ, reproduced by
+  separate software, and externally reviewed by a person. No completed external
+  human review is claimed.
+
 ## 0.4.0 - 2026-08-01
 
 ### Added

Cargo.toml

@@ -21,12 +21,14 @@ include = [
     "SECURITY.md",
     "SUPPORT.md",
     "CODE_OF_CONDUCT.md",
-    "assets/**",
+    "assets/qatq-architecture.svg",
+    "assets/qatqLogoFinal.png",
     "src/**",
     "examples/**",
     "adapters/**",
     "tests/**",
     "scripts/**",
+    "validation/**",
     "docs/ARCHITECTURE.md",
     "docs/oracle/**",
     "docs/CREDITS.md",

README.md

@@ -117,6 +117,11 @@ decisive inequality. Start with [`docs/oracle/README.md`](docs/oracle/README.md)
 then review the [claim boundary](docs/oracle/CLAIM_BOUNDARY.md) and
 [trust boundary](docs/oracle/TRUST_BOUNDARY.md).
 
+The v0.4.1 evidence corpus is also independently reproduced by a separate,
+pinned SageMath implementation. See the
+[machine-readable validation results](validation/oracle-v0.4.1/evidence/results.json)
+and the [precise validation terminology](docs/PUBLIC_RELEASE_0_4_1_EVIDENCE.md).
+
 ## Rust library
 
 ```rust

docs/PUBLIC_RELEASE_0_4_1_EVIDENCE.md

@@ -0,0 +1,79 @@
+# QATQ 0.4.1 Release Evidence
+
+QATQ 0.4.1 independently reproduces the complete published finite-certificate
+corpus with separate SageMath software. It does not add a theorem engine,
+change certificate semantics, or broaden the v0.4.0 claim boundary.
+
+## Differential result
+
+| corpus | rows | QATQ checker | separate SageMath reproduction |
+|---|---:|---|---|
+| binary Hamming | 14 | 14 valid | 14 agree |
+| spherical Rankin, `s = 0` | 5 | 5 valid | 5 agree |
+| spherical Rankin, `s < 0` | 8 | 8 valid | 8 agree |
+| **total** | **27** | **27 valid** | **27 agree** |
+
+The independent program recomputes the witness, exact integer upper bound, and
+decisive inequality from public certificate JSON. It imports no QATQ source or
+expected numeric answers. The run uses SageMath 10.6 from an image pinned by
+SHA-256 digest with networking disabled.
+
+Pinned image: `sagemath/sagemath:10.6@sha256:19995db6194f4a4bab18ce9a88556fd15b9ed5e916b4504fefe618a7796ddbdb`.
+
+Machine-readable evidence, requests, certificates, hashes, raw Sage output,
+and environment versions are published in
+[`validation/oracle-v0.4.1/evidence`](../validation/oracle-v0.4.1/evidence).
+CI regenerates the full corpus and compares its semantic results with the
+published record.
+
+## Release validation
+
+| gate | result |
+|---|---|
+| format, all-target/all-feature check, and all-feature tests | pass |
+| separate SageMath focused tests | pass; 5 tests including false witness and false objective rejection |
+| 27-row QATQ/SageMath differential corpus | pass; every witness, upper bound, and decisive inequality agrees |
+| all-target line coverage | pass; 84.89% overall |
+| RustSec audit | pass; no known vulnerabilities in 40 locked dependencies |
+| duplicate dependency check | pass; no duplicates reported |
+| deterministic KV stress matrix | pass; 4,096 cases and 8,499,064 values, exact restore |
+| public production KV gate | pass; all eight checks below 50 ns/value decode ceilings |
+| public competitive compression gate | pass; all compression-positive exact rows beat zstd/lz4 |
+| crate package and publish dry run | pass |
+
+The codec, QATC container, llama.cpp adapter patch, pinned matrix harness, public
+fixtures, and `Cargo.lock` are unchanged from v0.4.0. Under the documented patch
+release exception, the fresh v0.4.0 llama.cpp matrix is inherited rather than
+rerun. The release candidate reruns the full exact KV stress and both public
+compression gates and makes no new runtime or compression claim.
+
+- adapter patch SHA-256: `88963e6ff635f373e44538acff435d2fe75d2c57c128b3eec6ed020671ed8f65`
+- matrix harness SHA-256: `97b19a36e8971ce58711c95d6325e1551150d8e8fb43641582aa8e4d4416697e`
+- inherited report SHA-256: `133de6ddacd64f2ccf20999447006fed67694370a817c893482acbac36394492`
+
+## Validation levels
+
+| statement | v0.4.1 status | meaning |
+|---|---|---|
+| independently checkable by QATQ | complete | the production checker recomputed and accepted every certificate |
+| independently reproduced by separate software | complete | SageMath independently computed the same witness and upper bound for all 27 rows |
+| externally reviewed by a person | not complete | no attributable human coding-theory review is recorded |
+
+The machine-readable human-review status is
+[`external-review.json`](../validation/oracle-v0.4.1/external-review.json).
+QATQ does not describe v0.4.1 as externally reviewed.
+
+## Compatibility and claim boundary
+
+QATQ payload version 1, QATC container version 2, Oracle request schema 1,
+certificate schema 1, theorem identifiers, codec selection, tensor decoding,
+and runtime behavior are unchanged from v0.4.0.
+
+Supported: QATQ's published binary Hamming and spherical Rankin `s <= 0`
+certificate rows are independently reproduced by a separate SageMath
+implementation.
+
+Not supported: arbitrary KV-cache impossibility, positive-`s` spherical
+certificates, asymptotic-to-finite inference, concrete construction search,
+automatic distortion conversion, universal compression-capacity claims, or a
+claim of completed external human review.

docs/RELEASE_CHECKLIST.md

@@ -18,6 +18,10 @@ Run from the repository root:
 cargo fmt --check
 cargo check --all-targets --all-features
 cargo test --all-features
+scripts/run_oracle_independent_validation.sh /tmp/qatq-oracle-evidence
+python3 scripts/oracle_validation/compare_results.py \
+  --expected validation/oracle-v0.4.1/evidence/results.json \
+  --actual /tmp/qatq-oracle-evidence/results.json
 cargo metadata --locked --format-version 1
 cargo tree -d
 cargo audit
@@ -115,6 +119,8 @@ Do not tag a public release if:
 - the public competitive compression gate fails;
 - docs claim external runtime data is required for QATQ to operate;
 - raw private captures are staged.
+- the independent SageMath corpus does not reproduce every published finite
+  certificate row or differs semantically from the committed results.
 
 ## GitHub Release
 

docs/ROADMAP.md

@@ -125,6 +125,8 @@ not just access to exported tensors.
 - [x] Add exact finite spherical Rankin certificates for `s <= 0`.
 - [x] Add a smaller independent checker and adversarial certificate tests.
 - [x] Add atomic evidence bundles and a separate `qatq-oracle` CLI.
+- [x] Reproduce the published finite-certificate corpus with a separate pinned
+      SageMath implementation and publish machine-readable differential results.
 - [ ] Add positive-`s` Gegenbauer certificates with a complete interval/root
       proof.
 - [ ] Add construction search and an explicitly justified QATQ capture bridge.
@@ -133,3 +135,19 @@ not just access to exported tensors.
 
 The checked items define the first production Capacity Oracle release. Unchecked
 items remain explicit future scope and do not broaden finite claims.
+
+## Capacity Oracle - Geometry Reconnaissance Gate
+
+- [ ] Add a research-only, observation-only `profile-kv` command with bounded
+      exact and deterministic sampled pairwise analysis.
+- [ ] Profile at least two model families across prompt classes, context lengths,
+      dtypes, layers, heads, and pre/post-RoPE representations where exposed.
+- [ ] Preregister the application-level source of `required_states` and required
+      separation rather than deriving either from observed vector count.
+- [ ] Choose positive-`s` finite bounds, freeze Oracle expansion, or pivot to
+      live KV paging based on whether preregistered scenarios receive non-vacuous
+      decisions.
+
+Geometry profiling must emit observations only. It cannot emit
+`INFEASIBLE_UNDER_MODEL`, derive a capacity requirement, or expand the v0.4.x
+certificate semantics.

docs/oracle/CLAIM_BOUNDARY.md

@@ -1,6 +1,6 @@
 # QATQ Capacity Oracle: claim boundary
 
-Status: production finite-certificate contract for QATQ 0.4.0 (2026-08-01).
+Status: production finite-certificate contract for QATQ 0.4.x (2026-08-01).
 This contract covers the Hamming and Rankin engines described below. It does not
 alter the QATQ/QATC formats.
 
@@ -70,3 +70,9 @@ product claims. The scoped novelty claim is:
 > QATQ Capacity Oracle emits independently checkable finite infeasibility
 > certificates under an explicit binary or spherical representation model and
 > fails closed outside its declared finite theorem scope.
+
+QATQ v0.4.1 does not broaden this contract. It adds separate SageMath
+reproduction evidence for the published rows. “Independently checkable by
+QATQ,” “independently reproduced by separate software,” and “externally reviewed
+by a person” are distinct statements; see
+[`PUBLIC_RELEASE_0_4_1_EVIDENCE.md`](../PUBLIC_RELEASE_0_4_1_EVIDENCE.md).

docs/oracle/TRUST_BOUNDARY.md

@@ -16,3 +16,13 @@ QATQ/QATC encoding and decoding do not depend on Oracle code unless the Cargo
 `oracle` feature is explicitly enabled. The cargo-dist production build enables
 that feature so release archives contain `qatq-oracle`; the codec wire formats
 remain unchanged.
+
+QATQ v0.4.1 adds a separate evidence layer outside this production checker
+boundary. A pinned SageMath implementation consumes public certificate JSON and
+reproduces the finite witness and upper bound without importing QATQ code. Its
+agreement is evidence about the checker and producer; SageMath is not a runtime
+dependency and is not added to the trusted production path.
+
+Automated agreement is not human review. A claim of external review additionally
+requires the attributable record defined in
+[`validation/oracle-v0.4.1/external-review.json`](../../validation/oracle-v0.4.1/external-review.json).

scripts/oracle_validation/compare_results.py

@@ -0,0 +1,41 @@
+#!/usr/bin/env python3
+"""Compare the semantic content of two validation result bundles."""
+
+from __future__ import annotations
+
+import argparse
+import json
+from pathlib import Path
+
+
+def semantic_view(value: dict[str, object]) -> dict[str, object]:
+    return {
+        "schema_version": value.get("schema_version"),
+        "claim": value.get("claim"),
+        "corpus_sha256": value.get("corpus_sha256"),
+        "row_count": value.get("row_count"),
+        "all_row_ids_match": value.get("all_row_ids_match"),
+        "all_rows_agree": value.get("all_rows_agree"),
+        "rows": value.get("rows"),
+    }
+
+
+def main() -> int:
+    parser = argparse.ArgumentParser()
+    parser.add_argument("--expected", type=Path, required=True)
+    parser.add_argument("--actual", type=Path, required=True)
+    args = parser.parse_args()
+    expected = semantic_view(json.loads(args.expected.read_text()))
+    actual = semantic_view(json.loads(args.actual.read_text()))
+    if expected != actual:
+        print("independent validation semantic results differ")
+        return 1
+    if actual["all_rows_agree"] is not True:
+        print("independent validation did not agree on every row")
+        return 1
+    print(f"independent validation agrees on {actual['row_count']} rows")
+    return 0
+
+
+if __name__ == "__main__":
+    raise SystemExit(main())