Pith Number

pith:5RHIG7GS

pith:2026:5RHIG7GS2FKOFNCMTC4ZT3I3YG

not attested not anchored not stored refs pending

TensorRocq: Enabling diagrammatic reasoning in Rocq

Aleks Kissinger, Benjamin Caldwell, Robert Rand, William Spencer

Tools in Rocq convert symmetric monoidal category terms to hypergraphs with interfaces to support verified reasoning about string diagram deformations.

arxiv:2604.17592 v2 · 2026-04-19 · cs.LO · cs.PL

Open paper page JSON Open Graph Bundle Merged state Verified badge What is a Pith Number?

Add to your LaTeX paper

\usepackage{pith}
\pithnumber{5RHIG7GS2FKOFNCMTC4ZT3I3YG}

Prints a linked badge after your title and injects PDF metadata. Compiles on arXiv. Learn more · Embed verified badge

Record completeness

1 Bitcoin timestamp

2 Internet Archive

3 Author claim open · sign in to claim

4 Citations open

5 Replications open

✓ Portable graph bundle live · download bundle · merged state

The bundle contains the canonical record plus signed events. A mirror can host it anywhere and recompute the same current state with the deterministic merge algorithm.

Claims

C1strongest claim

We have developed verified tools for diagrammatic reasoning in Rocq, including inferring term equivalence and rewriting modulo the deformation of string diagrams. This is achieved by converting between syntactic representations of SMC terms and hypergraphs with interfaces, while preserving a common tensor semantics.

C2weakest assumption

The conversion between syntactic SMC terms and hypergraphs with interfaces correctly preserves tensor semantics and fully captures all allowed deformations of string diagrams.

C3one line summary

TensorRocq supplies verified Rocq tactics that convert symmetric monoidal category terms to hypergraphs with interfaces, enabling equivalence inference and rewriting based on string-diagram deformations while preserving tensor semantics.

Receipt and verification

First computed	2026-05-26T01:02:34.237004Z
Builder	pith-number-builder-2026-05-17-v1
Signature	Pith Ed25519 (`pith-v1-2026-05`) · public key
Schema	pith-number/v1.0

Canonical hash

ec4e837cd2d154e2b44c98b999ed1bc1bab2541fa0acf69016306c1a34a58617

Aliases

arxiv: 2604.17592 · arxiv_version: 2604.17592v2 · doi: 10.48550/arxiv.2604.17592 · pith_short_12: 5RHIG7GS2FKO · pith_short_16: 5RHIG7GS2FKOFNCM · pith_short_8: 5RHIG7GS

Agent API

Resolver JSON Graph JSON Events JSON Schema Signing key

Verify this Pith Number yourself

curl -sH 'Accept: application/ld+json' https://pith.science/pith/5RHIG7GS2FKOFNCMTC4ZT3I3YG \
  | jq -c '.canonical_record' \
  | python3 -c "import sys,json,hashlib; b=json.dumps(json.loads(sys.stdin.read()), sort_keys=True, separators=(',',':'), ensure_ascii=False).encode(); print(hashlib.sha256(b).hexdigest())"
# expect: ec4e837cd2d154e2b44c98b999ed1bc1bab2541fa0acf69016306c1a34a58617

Canonical record JSON

{
  "metadata": {
    "abstract_canon_sha256": "3f1b4b2a5b04fd2fe3973bf882c0d9b935d335226fc20fea3377aba9e9dc4c32",
    "cross_cats_sorted": [
      "cs.PL"
    ],
    "license": "http://creativecommons.org/licenses/by/4.0/",
    "primary_cat": "cs.LO",
    "submitted_at": "2026-04-19T19:52:46Z",
    "title_canon_sha256": "7169ccef07c4de794a70dec490bdf5e29e01924740cad5494fb3a5c61985e5aa"
  },
  "schema_version": "1.0",
  "source": {
    "id": "2604.17592",
    "kind": "arxiv",
    "version": 2
  }
}