# Tokitai Operator Claim Trace
This file maps implemented mechanisms to research claims, patent claim candidates, tests, audit artifacts, and prior-art concerns. It is not a legal filing; it is an engineering trace that keeps novelty claims grounded in executable code.
## P440 Validation-Maintenance Claim Audit
This trace is synchronized through P440. P248-P269 have hardened previously
smoke, scaffold, narrow-pilot, and claim-boundary gaps: runtime-shape ROCm/HIP
p-adic GEMM fixtures, repeated p-adic benchmark summaries, planner-selected
ROCm/HIP p-adic valuation lowering, public prefer-gpu dense integer add
selection, multi-overlap finite-site sheaf locality evidence, optional Lean
success transcripts, JSC target verification packet blockers, selected theorem
strict profiles, bounded p-adic algebra and finite-site sheaf evidence, and
post-P264 validation-maintenance guards are now explicit repository evidence.
Machine-checkable evidence list: runtime-shape ROCm/HIP p-adic GEMM fixtures, repeated p-adic benchmark summaries, planner-selected ROCm/HIP p-adic valuation lowering, public prefer-gpu dense integer add selection, multi-overlap finite-site sheaf locality evidence, optional Lean success transcripts, JSC target verification packet blockers, selected theorem strict profiles, bounded p-adic algebra and finite-site sheaf evidence, and post-P264 validation-maintenance guards.
```tokitai-claim-status-v1
phase=P440
sync_through=P440
current_paper_route=certified_valuation_sparse_fixed_precision_padic_gemm
primary_claim_allowed=true
production_speedup_claim_allowed=false
portable_rocm_claim_allowed=false
verified_hip_machine_code_claim_allowed=false
full_formalization_claim_allowed=false
sci_q2_claim_allowed=false
submission_readiness_claim_allowed=false
acceptance_probability_claim_allowed=false
external_venue_evidence_status=missing_author_evidence
```
The resulting claim boundary is still conservative. Tokitai may claim scoped
tested functionality for these paths, but it must not claim generic GPU
execution, production speedup, portable ROCm support, verified HIP machine
code, arbitrary precision p-adic fields, complete p-adic algebra, complete
sheaf theory, full proof-assistant formalization, current SCI-Q2 status,
submission readiness, or acceptance probability without new external evidence
and phase-specific validation.
## P257 Speed Evidence Claim Gate
P257 adds external-baseline and profiler-evidence fields to the p-adic
stratified benchmark artifacts. These fields are currently claim guards, not
speedup evidence: production speedup remains blocked unless reviewed external
baseline metadata, profiler capture, correctness checks, certificate coverage,
repeated timings, and measured speedup all pass together.
## P258 ROCm Portability Claim Gate
P258 adds a ROCm portability matrix shape with device, gfx, HIP version,
driver version, capability fingerprint, status, and claim guard fields. The
current matrix records local or unreviewed evidence only. Portable ROCm support
remains blocked until at least two reviewed passing device/compiler
combinations support the exact scoped claim.
## P440 Current Paper Claim Route
This claim trace is synchronized through P440. For paper drafting, the current
primary route remains 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 audit-gated non-claims.
The claim index below remains an engineering and patent-claim trace. It should
not be read as the current manuscript claim numbering. The current manuscript
route is the C10 package in `docs/paper/contribution_map.md` and
`docs/paper/certified_padic_gemm_manuscript_delta.md`; older proof-aware
operator-runtime mechanisms are supporting evidence.
## Claim Index
| ID | Implemented mechanism | Paper claim | Patent claim candidate | Evidence in code/tests | Prior-art concern |
| --- | --- | --- | --- | --- | --- |
| C1 | Domain contracts and obligations drive planning and verification. | Operator planning can be made proof-aware by treating algebraic contracts and unresolved obligations as IR/planner data. | A method for selecting and verifying operators using mathematical contracts, evidence logs, and proof obligations as planning inputs. | `src/domain/contract.rs`, `src/planner/obligation.rs`, `tests/semantic_planner.rs` | MLIR/XLA/TVM already have graph rewrites; novelty depends on contract/evidence/obligation coupling. |
| C2 | p-adic domains expose valuation, precision, non-Archimedean contracts, and precision-bounded equality. | Non-Archimedean structure can be represented directly in an operator library instead of encoded as ordinary integer arithmetic. | A valuation-aware execution method for p-adic or non-Archimedean computations with precision-bounded verification. | `src/domain/padic.rs`, `src/verify/equality.rs`, `tests/padic.rs` | SageMath and proof assistants cover p-adics; novelty is adaptive operator planning and backend execution integration. |
| C3 | p-adic valuation skip is a planner-visible rewrite with evidence and semantic cost. | Valuation thresholds can guide operator execution while preserving auditable precision semantics. | A method for skipping p-adic sum-product terms using valuation cutoff, estimated skipped/evaluated terms, and verification obligations. | `HeuristicPlanner::plan_padic_sum_products_skip`, `tests/padic.rs` | Compiler cost models are common; claim must emphasize non-Archimedean valuation semantics and correctness audit. |
| C4 | Finite sheaf sites, covers, restriction checks, and gluing appear as operator verification artifacts. | Sheaf-local computation can model local-to-global operator execution and consistency checking. | A method for cover-local operator execution with restriction compatibility validation and gluing verification. | `src/object/sheaf.rs`, `HeuristicPlanner::plan_cover_glue_check`, `tests/sheaf.rs` | Distributed/block computation exists; novelty depends on explicit sheaf semantics and cover/glue verification. |
| C5 | Semantic operator registry is separated from backend lowering rules. | Backends should not define mathematical semantics; lowering is valid only when tied to semantic entries and obligations. | A registry architecture linking semantic operator declarations, backend lowering rules, and verification obligations. | `src/op/registry.rs`, `HeuristicPlanner::plan_with_registry`, `tests/operator_registry.rs` | MLIR dialects and TVM schedules have registries; distinction is contract/evidence/obligation-aware lowering. |
| C6 | Contracts produce executable property checks and generated samples. | Mathematical laws can drive verification workloads and audit output. | A method for deriving property checks and sample sets from domain contracts, then attaching results to operator audits. | `src/verify/properties.rs`, `src/verify/samples.rs`, `tests/properties.rs` | QuickCheck/proptest/Hypothesis generate tests; novelty is contract-derived mathematical sample generation and audit integration. |
| C7 | First-of-kind hypotheses are stored as guarded evidence entries with prior-art boundaries, repository artifacts, tests, non-claims, and residual risks. | Tokitai's novelty is an implementation-backed integration hypothesis, not a broad firstness assertion. | A claim-screening workflow that admits patent/paper language only when it is tied to executable artifacts and explicit non-claims. | `src/verify/novelty.rs`, `docs/first_of_kind_novelty_evidence.md`, `tests/novelty_dossier.rs` | Prior art may cover each ingredient independently; the dossier keeps claims scoped to the integrated runtime contract. |
| C8 | p-adic, finite-site sheaf, and categorical law evidence share a theory contract model. | Mathematical theories can be engineered as reusable runtime contracts that feed planner evidence and audit-only obligations. | A theory-evidence interface that maps domain constraints, law witnesses, theorem assumptions, and audit evidence into execution plans. | `src/theory.rs`, `tests/theory_contracts.rs`, `docs/theory_contract_core.md` | The model is an engineering contract layer, not full p-adic algebra, general sheaf theory, category theory, or runtime formal verification. |
| C9 | Lean theorem packages are discoverable through a structured theorem binding registry. | Proof-assistant theorems can be connected to runtime evidence through explicit assumption maps, checker transcripts, and missing-evidence errors. | A theorem-binding registry linking theorem IDs, Lean files, transcript status, runtime evidence requirements, and non-claims. | `src/verify/theorems.rs`, `tests/theorem_binding_registry.rs`, `docs/theorem_binding_registry.md` | The registry is metadata and validation plumbing; it does not prove the Rust runtime or broaden theorem scope. |
| C10 | Rewrites and lowerings declare certified theory-law requirements. | Mathematical rewrites and backend lowerings can name their required theory laws, theorem bindings, runtime evidence, and structured missing-evidence reports. | A certified contract layer for rewrite/lowering admission that records theory-law requirements and fallback evidence. | `src/theory.rs`, `src/ir/contract.rs`, `src/op/registry.rs`, `src/planner/mod.rs`, `tests/certified_contracts.rs`, `docs/certified_rewrite_lowering_contracts.md` | This is explicit contract evidence, not a proof of every backend kernel or a full formalization of all admissible rewrites. |
| C11 | Additional p-adic and finite-site sheaf workflows consume the shared theory contract model directly. | Theory contracts are executable operator evidence, not only planner annotations. | Operator workflows that return theory evidence for fixed-precision p-adic multiplication and finite-site sheaf obstruction localization. | `src/theory.rs`, `tests/theory_operator_hardening.rs`, `docs/theory_specific_operator_hardening.md` | These workflows remain fixed-precision and finite-site scoped; they do not implement full p-adic algebra, general sheaf repair, or cohomology. |
| C12 | Semantic conformance reports join CPU oracle, property, theorem-binding, fallback, and audit-trace evidence. | Runtime conformance can be reported as one theory-indexed evidence chain rather than independent logs. | A semantic conformance report that separates theorem-checked evidence from runtime-tested evidence and records fallback or missing-theory-evidence status per mathematical theory. | `src/verify/semantic_conformance.rs`, `tests/semantic_conformance_report.rs`, `docs/semantic_conformance_report.md` | This is a deterministic evidence report, not full formal verification of the Rust runtime or a general theorem about p-adic, sheaf, or categorical semantics. |
| C13 | A generated theory-aware support matrix states supported, fallback-only, feature-gated, and unsupported combinations. | Tokitai can make its mathematical and hardware support boundaries machine-checkable instead of prose-only. | A generated support matrix linking domains, operators, theory constraints, theorem packages, backend capability, fallback mode, public API exposure, tests, and non-claims. | `src/verify/support_matrix.rs`, `tests/theory_support_matrix.rs`, `docs/theory_support_matrix.md`, `target/paper-results/theory-support-matrix.json` | The matrix is support-boundary evidence, not a claim of complete p-adic algebra, general sheaf theory, broad GPU acceleration, or production compiler maturity. |
| C14 | A theory-engineering release gate checks contracts, theorem bindings, semantic conformance, support rows, facade examples, validations, and known limits. | Tokitai is ready for external positioning only when executable theory evidence and scoped non-claims pass a generated release gate. | A release-gate report that records pass/fail checks, blockers, required validation commands, deferred work, and known limitations for theory-engineered runtime evidence. | `src/verify/release_gate.rs`, `tests/theory_release_gate.rs`, `docs/theory_engineering_release_gate.md`, `target/paper-results/theory-release-gate.json` | Passing the gate is scoped release evidence, not full formal verification, complete mathematics, broad accelerator support, or production performance proof. |
| C15 | Prior-art validation identifies certified valuation-sparse p-adic GEMM as the only surviving strong paper route. | Tokitai's next defensible paper claim is a concrete algorithm-system claim: valuation-sparse p-adic GEMM with skip certificates, CPU dense/sparse oracles, ROCm/HIP execution, and audit-gated non-claims. | A method for executing fixed-precision p-adic GEMM by valuation-derived skip certificates and validating hardware execution against dense and certified sparse oracles. | `docs/prior_art_certified_valuation_sparse_padic_gemm.md`, `todo.json`, `tests/paper_artifacts.rs` | p-adic precision tracking, exact linear algebra, GPU finite-field arithmetic, and p-adic-adjacent GPU workloads already exist; novelty depends on the full certified valuation-sparse GEMM pipeline, not any component alone. |
## Audit Artifacts For Paper Figures
Use `cargo run --example audit_traces` to print representative audit text for:
1. p-adic valuation skip with semantic cost rationale.
2. sheaf cover glue check.
3. registry-aware semantic lowering.
These traces are intended as raw material for paper figures and patent disclosure diagrams. They show that the claimed mechanisms are not only type definitions; they are observable in planner output and tests.
## Defensive Notes
- Avoid claiming a generic graph compiler, kernel registry, or property-testing framework as novel.
- Emphasize the combination of mathematical domains, contracts, proof obligations, valuation/precision cost, and auditable backend lowering.
- For the next paper route, do not lead with release gates or claim-boundary infrastructure. Lead with certified valuation-sparse p-adic GEMM and use audit/release evidence only to make the claim falsifiable.
- Required non-claims from `docs/prior_art_certified_valuation_sparse_padic_gemm.md`: not first p-adic arithmetic, not first exact linear algebra, not first GPU exact arithmetic, not first GPU use in p-adic-adjacent computation, not arbitrary precision p-adics, and not production speedup without scoped benchmark evidence.
- For patent drafting, strongest current mechanisms are C3 and C5. C1 and C6 support system-level claims. C4 is promising but still finite-site prototype level.
- For paper drafting, frame the library around certified valuation-sparse
p-adic GEMM with theorem-bound skip certificates, dense and certified sparse
CPU oracle evidence, feature-gated ROCm/HIP pilot evidence, deterministic
benchmark distributions, and audit-gated non-claims. Treat proof-aware
operator-runtime machinery and finite-sheaf examples as supporting evidence,
not the primary paper claim.
- For first-of-kind language, use `docs/first_of_kind_novelty_evidence.md` and keep FOK1-FOK4 as evidence-backed hypotheses unless a separate prior-art review upgrades them.
## P354 Functional-Expansion Documentation Sync
The P335-P354 phases add 30+ new operators, a closure-based graph DSL, a
4-chapter example book, 82 new facade doctests, 5 proptest test files, and
a Mermaid architecture-diagram set. The implementation files touched are
exclusively in the operator surface, public facade, doctests, examples,
and test directories. The paper-claim flags above (`primary_claim_allowed`,
`production_speedup_claim_allowed`, `portable_rocm_claim_allowed`,
`verified_hip_machine_code_claim_allowed`, `full_formalization_claim_allowed`,
`sci_q2_claim_allowed`, `submission_readiness_claim_allowed`,
`acceptance_probability_claim_allowed`) are unchanged: all 7 blocked flags
remain `false` and the primary claim remains certified valuation-sparse
fixed-precision p-adic GEMM.
The new operators, doctests, and examples are CPU-reference execution
with parity-tested oracles. They do not enable a production speedup
claim, a portable ROCm claim, a verified HIP machine-code claim, a
full formalization claim, an SCI-Q2 status claim, a submission-readiness
claim, or an acceptance-probability claim. They are supporting
infrastructure that strengthens the developer ergonomics of the
Tokitai reference path; they are not the primary paper route.
The new operator surface is registered in `src/op/{arithmetic,shape,nn,
index,reductions}.rs` with matching `LoweringRule` entries in
`src/op/registry.rs`; each operator has a `required-evidence` text and
an `obligation` text that the audit layer can read and the verifier
can re-check. The `audit_report` and `claim_status` machinery remains
the only path to claim-boundary code; the new ops route through it.
## P381 CI Hygiene Claim Boundary
P381 adds `.github/workflows/ci.yml`. The CI workflow runs
`cargo fmt --check`, `cargo build --offline`, `cargo test --offline`,
verifies the `tokitai-claim-status-v1` block (7 `=false` + 1 `=true`),
and verifies the `tokitai-validation-status-v1` block. None of the
8 `*_claim_allowed` flags change: P381 is paper-submission hygiene,
not a claim-boundary change. The workflow triggers on push, pull_request,
and workflow_dispatch. Concurrency group cancels in-flight runs on the
same ref.
## P382 Support-Matrix Dedup Classification
P382 adds `src/verify/support_matrix_dedup_classify.rs` and
`tests/support_matrix_dedup_classify.rs`. After P369 the support
matrix has 8 irreducible duplicate (domain, operator, backend)
triples; P382 classifies them with a `DupKind` enum
(`MultiState`, `MultiRule`, `Other`) and a `matrix_dedup_summary`
function. The 8 dups split into 4 `MultiState` (pilot+unavailable
or pilot+fallback pairs that share a `lowering_rule_id`) and
4 `MultiRule` (distinct `lowering_rule_id`s that share the same
domain+operator+backend triple, e.g. the 3 Q_* matmul rules).
None of the 8 `*_claim_allowed` flags change. The matrix format
and dedup policy are unchanged; P382 is documentation + visibility
of the irreducible dup kinds.
## P383 Fail-Closed Audit Example
P383 adds `examples/fail_closed_audit.rs` and registers it in
`Cargo.toml`. The example demonstrates the 3 main fail-closed
paths by deliberately triggering each one and printing the
pre-execution audit (showing the obligation) and the
post-execution error (showing the fail-closed response):
1. Shape contract violation: ReshapeOp 2x3 -> 2x2 produces
`Error::Backend("reshape: target dims product 4 does not match
data length 6")`.
2. Lowering-rule obligation violation: an unregistered op
(`UnregisteredDemoOp`) yields a Required+Unresolved obligation
`"operator demo_unregistered_op must be registered before
backend lowering"` and the executor returns
`Error::Backend("cpu scalar reference backend does not support
op demo_unregistered_op")`.
3. Backend-error violation: DivOp with a zero divisor returns
`Error::Backend("div by zero")`.
None of the 8 `*_claim_allowed` flags change. P383 is developer
ergonomics (DX companion to the release-gate tests); the fail-closed
guarantees were already in place and exercised by the release-gate
tests; the example just makes the paths inspectable from the CLI.
## P384 Observability Documentation
P384 adds `docs/observability.md`. The doc is the single entry
point for the 3 observability commands:
1. `cargo run --offline --example claim_status_report`
(P366, claim flags + preconditions).
2. `cargo run --offline --example submission_readiness`
(P373, paper-submission verdict).
3. `cargo run --offline --example proof_replay_witnesses_section`
(P357, proof-replay witness summary, accessed via the
`verify::proof_replay_witnesses_section` function).
None of the 8 `*_claim_allowed` flags change. P384 is documentation;
no new observability paths are added.
## P385 Post-P353 Stress Coverage
P385 extends `tests/proptest_stress.rs` with 3 new proptest blocks:
`stress_shape_reshape` (Reshape preserves element order across
random inputs), `stress_nn_relu` (ReLU clamps negatives across
random inputs), and `stress_index_gather` (Gather at index i
returns data[i] across random inputs). The existing 3 proptest
blocks (arithmetic Add+Mul+Relu) remain unchanged. All 6 proptest
blocks honor the `PROPTEST_CASES` env (default 100, bumped to
500 in CI via env). None of the 8 `*_claim_allowed` flags change.
P385 is test coverage; no public API change.