# Contribution Map
This map connects SCI-Q2 paper claims to repository evidence. The generated
`target/paper-results/claim-to-test-matrix.csv` is the machine-readable summary.
## Primary P222 Manuscript Route: Certified Valuation-Sparse p-adic GEMM
This contribution map is synchronized through P236. The current primary
manuscript route is C10 certified valuation-sparse p-adic GEMM; C1-C9 remain
supporting traceability, proof-evidence, nonstandard-domain, and reproducibility
claims.
The current manuscript route is no longer broad claim-boundary or
release-gate language. The primary contribution is the concrete
algorithm-system claim:
> certified valuation-sparse p-adic GEMM with skip certificates, dense CPU
> oracle, certified sparse CPU oracle, ROCm/HIP execution, and audit-gated
> non-claims.
Prior-art boundary:
- p-adic precision tracking is known
- exact and p-adic linear algebra are known
- GPU finite-field and exact arithmetic are known
- GPU use inside p-adic-adjacent workflows is known
- release gates and artifact traces are supporting evidence, not the main claim
Current supporting artifact:
- `docs/prior_art_certified_valuation_sparse_padic_gemm.md`
- `docs/rocm_padic_stratified_benchmarks.md`
- `docs/certified_padic_gemm_release_gate.md`
- `docs/paper/certified_padic_gemm_manuscript_delta.md`
- `target/paper-results/padic-stratified-benchmarks/padic-stratified-benchmarks.json`
The claim is now implemented as a narrow contribution package: CPU dense and
certified sparse oracles exist, scalar/dot/matrix theorem boundaries exist,
the Q_5[3] 2x3x2 ROCm/HIP pilot executes under `rocm-hip`, benchmark artifacts
cover deterministic valuation distributions and fallback rows, and P221 gates
fail closed when theorem, certificate, benchmark, audit, or non-claim evidence
is missing.
## C1. Trace-Bound Semantic Evidence
Claim: accepted Tokitai traces bind execution plans, proof replay reports,
proof-assistant summaries, adapter registries, native admissions, checker
outputs, checker result indexes, and manifests.
Code:
- `src/verify/mod.rs`
- `docs/paper/formal_model.md`
- `docs/paper/proof_assistant_scope.md`
Tests:
- `tests/operator_registry.rs`
- `tests/audit_traces_example.rs`
- `tests/paper_artifacts.rs`
Artifacts:
- `target/paper-results/tamper-matrix.csv`
- `target/paper-results/trace-architecture.csv`
Prior-art distinction: proof-carrying code and supply-chain attestations bind
programs or build artifacts; Tokitai binds theorem-result fingerprints inside
adaptive mathematical operator traces.
## C2. Nonstandard-Domain Planning
Claim: p-adic valuation and finite sheaf locality are first-class planning and
verification resources, not storage dtype aliases.
Code:
- `src/domain.rs`
- `src/object/sheaf.rs`
- `src/planner.rs`
- `src/backend`
Tests:
- `tests/padic.rs`
- `tests/sheaf.rs`
- `tests/generic_backend.rs`
Artifacts:
- `target/paper-results/paper-results.csv`
- `target/paper-results/measurement-summary.csv`
- `target/paper-results/baseline-scale-comparison.csv`
Prior-art distinction: tensor libraries dispatch on dtype and shape; Tokitai
uses mathematical domain contracts to generate planning evidence and
verification obligations.
Limitation: p-adic arithmetic is fixed precision and the sheaf implementation
is a finite-site prototype, so the manuscript should claim nonstandard-domain
evidence rather than a comprehensive computer algebra system.
## C3. Native Checker Admission Binding
Claim: proof-assistant checker outputs can be represented as trace-bound native
admissions and rejected when stale or mismatched.
Code:
- `src/verify/mod.rs`
- `docs/paper/proof_assistant_scope.md`
Tests:
- `tests/operator_registry.rs`
- `tests/audit_traces_example.rs`
Artifacts:
- `target/paper-results/tamper-matrix.csv`
- `target/paper-results/trace-architecture.csv`
Prior-art distinction: the contribution is not Lean integration alone; it is
the runtime trace binding across checker output, admission artifact, adapter
capability, and theorem-result fingerprint.
Limitation: the current artifact does not generate full Lean, Coq, or Isabelle
proof terms for every Tokitai obligation; it exposes a scoped external checker
admission path.
## C4. Authenticity Versus Semantic Failure Taxonomy
Claim: validation reports distinguish authenticity failures from semantic
validation failures.
Code:
- `TraceValidationFailureClass`
- `TraceValidationFailureBroadClass`
- `classify_trace_validation_error`
- `docs/paper/trust_model.md`
Tests:
- `tests/operator_registry.rs`
- `tests/audit_traces_example.rs`
- `tests/paper_artifacts.rs`
Artifacts:
- `target/paper-results/claim-to-test-matrix.csv`
Prior-art distinction: the project does not claim new cryptography. It uses
standard signatures and digests, then separates those failures from
theorem-level registry/admission failures.
Limitation: key rotation and external key management are policy concerns, not
integrated infrastructure.
## C5. Canonical Artifact Normalization
Claim: paper-critical version-1 JSON artifacts can be imported from ordinary
JSON object ordering and normalized back to Tokitai's canonical semantic bytes
without changing theorem-level trace evidence.
Code:
- `src/verify/mod.rs`
- `docs/paper/serialization_strategy.md`
- `docs/paper/formal_model.md`
Tests:
- `tests/json_parser_regression.rs`
- `tests/paper_artifacts.rs`
- `tests/paper_benchmarks_example.rs`
Artifacts:
- `target/paper-results/claim-to-test-matrix.csv`
- `target/paper-results/trace-architecture.csv`
Prior-art distinction: schema validation alone does not establish stable
reviewer-facing evidence. Tokitai separates permissive import syntax from
canonical renderer output and binds that normalization to proof-trace claims.
Limitation: paper-critical renderers are deterministic and dependency-light,
but broad serde-derived audit serialization remains future work.
## C6. Selected Native Shape Witness
Claim: Tokitai can expose selected shape-equality proof metadata as
reviewer-visible Lean checkable witness evidence.
Code:
- `src/verify/mod.rs`
- `docs/paper/proof_assistant_scope.md`
Tests:
- `tests/operator_registry.rs`
- `tests/audit_traces_example.rs`
- `tests/paper_artifacts.rs`
Artifacts:
- `target/paper-results/claim-to-test-matrix.csv`
- `target/paper-results/trace-architecture.csv`
- `target/paper-results/paper-results.json`
Prior-art distinction: the claim is not that Tokitai replaces Lean shape
libraries. The novelty is binding selected shape witness metadata to replayed
runtime proof artifacts and checker-result fingerprints.
Limitation: this is a selected witness family, not a complete proof-assistant
encoding of all shape obligations.
## C7. Selected Nonstandard p-adic Witness
Claim: Tokitai can expose a selected p-adic precision-cutoff witness family
that connects nonstandard-domain planning evidence to the proof-assistant
trace chain.
Code:
- `src/verify/mod.rs`
- `docs/paper/proof_assistant_scope.md`
- `src/domain.rs`
Tests:
- `tests/padic.rs`
- `tests/paper_artifacts.rs`
- `tests/paper_benchmarks_example.rs`
Artifacts:
- `target/paper-results/claim-to-test-matrix.csv`
- `target/paper-results/trace-architecture.csv`
- `target/paper-results/paper-results.json`
Prior-art distinction: p-adic libraries provide arithmetic; Tokitai connects
valuation and precision-cutoff evidence to adaptive operator proof traces.
Limitation: the witness family covers precision-cutoff evidence, not broad
p-adic algebra or sheaf proof coverage.
## C8. Reviewer-Visible Witness Metadata
Claim: selected proof-assistant witness metadata is visible in schema
documentation, generated JSON, benchmark measurements, and tamper ablations.
Code:
- `docs/paper/schema_inventory.md`
- `ARTIFACT.md`
- `examples/paper_benchmarks.rs`
Tests:
- `tests/schema_guards.rs`
- `tests/paper_artifacts.rs`
- `tests/paper_benchmarks_example.rs`
Artifacts:
- `target/paper-results/paper-results.json`
- `target/paper-results/measurement-summary.csv`
- `target/paper-results/tamper-matrix.csv`
- `target/paper-results/claim-to-test-matrix.csv`
Prior-art distinction: proof metadata is not merely embedded in comments; it is
schema-visible, generated, and included in reviewer-facing validation checks.
Limitation: selected witness metadata overhead is measured with deterministic
proxy rows and does not include external Lean runtime benchmarking.
## C9. Controlled Baseline And Scale Evaluation
Claim: Tokitai's paper artifact evaluates ordinary tensor, p-adic valuation,
finite sheaf, proof-trace, and selected witness metadata paths against explicit
controlled baselines and scale points.
Code:
- `examples/paper_benchmarks.rs`
- `docs/paper/evaluation_methodology.md`
- `docs/schemas/tokitai-paper-csv-v1.schema.json`
Tests:
- `tests/paper_benchmarks_example.rs`
- `tests/paper_artifacts.rs`
- `tests/schema_guards.rs`
Artifacts:
- `target/paper-results/baseline-scale-comparison.csv`
- `target/paper-results/measurement-summary.csv`
- `target/paper-results/paper-results.json`
Prior-art distinction: the table is a controlled artifact evaluation, not a
claim of production performance against mature tensor compilers.
Limitation: deterministic proxy timings and small CPU reference workloads make
the evidence suitable for SCI-Q2 artifact review, not for production throughput claims.
## C10. Certified Valuation-Sparse p-adic GEMM
Claim: Tokitai implements a certified valuation-sparse fixed-precision p-adic
GEMM path where valuation lower bounds justify skipped products, per-output
certificates record the skip evidence, dense CPU and certified sparse CPU
oracles validate the result, and a feature-gated ROCm/HIP pilot executes the
Q_5[3] 2x3x2 workload with audit-gated non-claims.
Code:
- `src/domain/padic.rs`
- `src/backend/hip_padic_matmul.rs`
- `src/backend/hip_padic_benchmarks.rs`
- `src/verify/release_gate.rs`
- `src/verify/support_matrix.rs`
Tests:
- `tests/padic.rs`
- `tests/padic_valuation_skip_theorem.rs`
- `tests/rocm_padic_stratified_matmul.rs`
- `tests/rocm_padic_stratified_benchmarks.rs`
- `tests/theory_release_gate.rs`
Artifacts:
- `docs/prior_art_certified_valuation_sparse_padic_gemm.md`
- `docs/rocm_padic_stratified_benchmarks.md`
- `docs/certified_padic_gemm_release_gate.md`
- `target/paper-results/padic-stratified-benchmarks/padic-stratified-benchmarks.json`
- `target/paper-results/padic-stratified-benchmarks/padic-stratified-benchmarks.csv`
- `target/paper-results/padic-stratified-benchmarks/padic-stratified-benchmarks.md`
Prior-art distinction: p-adic arithmetic, exact linear algebra, sparse GEMM,
GPU finite-field kernels, and release gates are known separately. The defended
contribution is the combined certified valuation-sparse p-adic GEMM pipeline
with theorem-bound skip certificates, CPU dense/sparse oracle evidence,
feature-gated ROCm/HIP execution, benchmark distribution coverage, and
fail-closed non-claim gates.
Limitation: the ROCm/HIP pilot is narrow Q_5[3] 2x3x2 local hardware evidence.
It does not claim arbitrary precision p-adic fields, full p-adic algebra,
portable AMD GPU support, verified HIP machine code, or production speedup.
## Manuscript Narrative Anchors
The manuscript skeleton in `docs/paper/manuscript_skeleton.md` assembles these
claims into sections for abstract, introduction, system model, formal theorem,
proof assistant evidence, nonstandard domains, baseline evaluation,
reproducibility, related work, limitations, and conclusion.
Required manuscript evidence:
- Formal theorem: `docs/paper/formal_model.md`
- Proof assistant scope: `docs/paper/proof_assistant_scope.md`
- Evaluation methodology: `docs/paper/evaluation_methodology.md`
- Readiness audit and related-work risk: `docs/paper/readiness_audit.md`
- Reproducibility: `ARTIFACT.md`
- Generated tables: `target/paper-results/claim-to-test-matrix.csv`,
`target/paper-results/trace-architecture.csv`,
`target/paper-results/baseline-scale-comparison.csv`,
`target/paper-results/padic-stratified-benchmarks/padic-stratified-benchmarks.csv`
## P236 Prior-Art And Novelty Boundary Matrix
Tokitai's SCI-Q2 novelty claim is now a scoped algorithm-system claim:
certified valuation-sparse fixed-precision p-adic GEMM with theorem-bound skip
certificates, dense CPU and certified sparse CPU oracle agreement,
feature-gated ROCm/HIP pilot evidence, deterministic benchmark distributions,
and fail-closed non-claim gates connected in one reproducible artifact. The
following matrix keeps that claim separate from standard components and keeps
the older trace-bound runtime machinery as supporting infrastructure.
| Nearby prior-art family | Established strengths | Tokitai distinction | Evidence anchors | Non-novelty / no-overclaim boundary |
| --- | --- | --- | --- | --- |
| Tensor compilers and operator runtimes | MLIR, XLA, TVM, Triton, JAX, PyTorch, and TensorFlow optimize tensor programs, dispatch kernels, and manage layouts at production scale. | Tokitai treats mathematical domain contracts, proof obligations, theorem-result fingerprints, and trace validation as planner/runtime artifacts, including fixed-precision p-adic and finite-sheaf examples. | `src/planner`, `src/op/registry.rs`, `tests/operator_registry.rs`, `tests/padic.rs`, `tests/sheaf.rs`, `target/paper-results/baseline-scale-comparison.csv` | Do not claim production performance superiority, production tensor compiler maturity, or broad accelerator support; current backend evidence is CPU reference and controlled artifact evaluation. |
| Proof assistants and SMT/verification tools | Lean, Coq, Isabelle, Why3, Dafny, SMT solvers, and proof ecosystems provide proof languages, kernels, automation, and verified reasoning infrastructure. | Tokitai does not replace theorem provers; it binds selected checker outputs, native admissions, adapter capabilities, checker result indexes, and theorem-result fingerprints to runtime operator traces. | `docs/paper/proof_assistant_scope.md`, `docs/paper/formal_model.md`, `tests/audit_traces_example.rs`, `tests/operator_registry.rs`, `target/paper-results/trace-architecture.csv` | Do not claim full proof-assistant replacement, full Lean/Coq/Isabelle theorem generation, or a mechanically verified Rust validator. |
| p-adic libraries and computer algebra systems | SageMath, PARI/GP, Magma-style systems, and algebra libraries provide p-adic arithmetic, number-theory operations, and mature symbolic functionality. | Tokitai uses p-adic valuation, precision cutoff, and precision-bounded equality as operator planning and verification resources tied to proof traces. | `src/domain/padic.rs`, `tests/padic.rs`, `tests/properties.rs`, `docs/paper/proof_assistant_scope.md`, `padic_precision_cutoff_witness_v1` | Do not claim novel p-adic mathematics, arbitrary precision p-adic field coverage, or complete p-adic algebra formalization. |
| Sheaf/category-theory tools and mathematical libraries | Category-theory, topology, and theorem-prover libraries model abstract sheaves, restrictions, covers, and categorical constructions. | Tokitai models finite-site sheaf covers as planner-visible locality and compatibility evidence for operator execution, with cover glue checks in audit paths. | `src/object/sheaf.rs`, `tests/sheaf.rs`, `tests/properties.rs`, `docs/paper/formal_model.md`, `target/paper-results/paper-results.csv` | Do not claim complete sheaf theory, sheaf cohomology, general categorical formalization, or production distributed-system semantics. |
| Verified compilers and translation validators | CompCert, Alive2, verified compiler passes, and translation validators establish semantic preservation for compiler transformations under explicit formal models. | Tokitai's theorem is trace-bound semantic evidence preservation for accepted operator artifacts, not full compiler correctness; it focuses on registry-aware lowering evidence, proof replay, and native admission binding. | `docs/paper/formal_model.md`, `tests/adaptive_planning.rs`, `tests/operator_registry.rs`, `tests/json_parser_regression.rs` | Do not claim fully verified compiler status, full backend machine-code verification, or mechanical verification of the Rust implementation. |
| Artifact reproducibility and supply-chain frameworks | SLSA, in-toto, Sigstore, TUF, archival DOI practices, JSON schemas, checksums, and release checklists provide packaging, provenance, and integrity workflows. | Tokitai uses reproducibility and authenticity machinery to support theorem-level semantic trace validation, canonical artifact normalization, and reviewer-visible proof evidence. | `docs/paper/release_checklist.md`, `docs/paper/release_bundle_manifest.md`, `docs/paper/trust_model.md`, `tests/schema_guards.rs`, `tests/json_parser_regression.rs` | Do not claim new cryptography, novel JSON schema technology, or that optional Lean checks and CPU reference execution are themselves research novelty. |
### Integrated Novelty Statement
The manuscript should describe Tokitai's contribution as:
"Tokitai integrates certified valuation-sparse fixed-precision p-adic GEMM with trace-bound proof evidence: valuation lower bounds justify skipped products, per-output certificates expose theorem assumptions, dense CPU and certified sparse CPU oracles validate supported rows, feature-gated ROCm/HIP pilot rows record local execution evidence, and release gates prevent unsupported claims about arbitrary precision, full p-adic algebra, portability, verified machine code, or production speedup."
This is distinct from claiming novelty for SHA-256, JSON schemas, Cargo-based
reproducibility, optional Lean invocation, CPU reference execution, p-adic
arithmetic, sheaf theory, or tensor kernels in isolation.
In short: the contribution is not SHA-256, not JSON schemas, not optional Lean
invocation, not CPU reference execution, not p-adic arithmetic alone, not sheaf
theory alone, and not tensor kernels in isolation.
### P154 No-Overclaim Checklist
- Do not claim outperforming mature tensor compilers.
- Do not claim replacement of Lean, Coq, Isabelle, SMT solvers, or verified
compilers.
- Do not claim novel p-adic or sheaf mathematics.
- Do not claim production deployment packaging, production benchmark maturity,
or production accelerator support.
- Do not claim cryptographic novelty for signatures, SHA-256 digests, schemas,
or release checklists.
- Do claim the integrated trace-bound operator evidence architecture when
backed by `docs/paper/formal_model.md`, `docs/paper/evaluation_methodology.md`,
`docs/paper/proof_assistant_scope.md`, and generated paper-result artifacts.
## Generated Tables
Run:
```bash
cargo run --quiet --example paper_benchmarks
```
Expected generated files:
- `target/paper-results/paper-results.json`
- `target/paper-results/paper-results.csv`
- `target/paper-results/measurement-summary.csv`
- `target/paper-results/baseline-scale-comparison.csv`
- `target/paper-results/tamper-matrix.csv`
- `target/paper-results/claim-to-test-matrix.csv`
- `target/paper-results/trace-architecture.csv`
## P354 Functional-Expansion Operator Surface
P335-P354 added 30+ new operators (8 arithmetic, 9 shape, 6 NN/activation,
5 index, 9 reduction), a closure-based graph DSL, 82 facade doctests, 4
book-chapter tutorials, 5 proptest files, and a Mermaid diagram set. The
new operators are CPU-reference execution with oracle parity tests; they
do not change the primary C10 paper route (certified valuation-sparse
p-adic GEMM), nor do they enable any of the seven blocked claim flags
in `CLAIMS.md`. The new surface is supporting infrastructure for
developer ergonomics and reference-path coverage; the C1-C9 and C11-C15
supporting claims continue to be the cross-cutting traceability and
non-claim machinery. C10 certified valuation-sparse p-adic GEMM remains
the only surviving strong paper route.