Corpus Graph

Conceptual graph

What the graph should answer

The graph exists to answer practical review questions:

• Which definitions does this theorem depend on?
• Which later results use this object?
• Which public result is anchored by this registry item?
• Which publication states the argument narratively?
• Which Lean module, if any, formalizes the relevant layer?
• Which version or release manifest fixes the current public state?

Current data-backed projection

The current page remains a conceptual surface, but Wave 3 now publishes the underlying graph projection data from Corpus.

• Object inventory: data/graph/objects.json
• Dependency adjacency: data/graph/adjacency.json
• Reverse dependency adjacency: data/graph/reverse-adjacency.json
• Dependency nodes: 4139
• Reverse dependency nodes: 4139

This sprint does not turn the graph into a full interactive UI. It makes the data contract explicit so later visual or query surfaces have a stable Corpus-owned source.

Corpus v3 — live graph stats

The next-generation Corpus v3 graph projects every Corpus Item to a permanent /id/cid######/ URL with relation panels, identifier box, and JSON-LD metadata. This is a parallel surface to the v2 Registry above — both remain live during the v3 cutover phase.

Type distribution

• axiom  8
• bridge claim  1
• chapter  1
• claim  1
• construction step  100
• corollary  6
• definition  313
• erratum  1
• falsifier  1
• formal axiom  3
• formal module  267
• formal theorem  838
• lemma  23
• monograph  7
• open problem  1
• prediction  1
• proof  6
• proposition  114
• readout claim  1
• release packet  2
• research dossier  1
• research note  1
• research paper  1
• result  1
• theorem  223

Sample item pages

A handful of representative Corpus v3 surfaces to explore:

• Master Constant Calibration (THM0001) — the running-example theorem with its full prose proof at PRF0001 and its Lean formalization at FTH0001
• Construction Spine (DOS0001) — the 121-step construction dossier
• Book II — The τ-Kernel (BOK0001) — monograph artifact item
• Categorical AI (PAP0001) — research paper artifact
• No Independent Dark-Sector Particle (RSL0001) — Result item with inspection route
• Lean-Formalized Proof of FTA on τ-Idx (PRF0005) — lean_formalized proof item

Every public typed alias also short-routes — e.g., /thm0001/, /def0001/, /pap0001/, /dos0001/ — for citation continuity. v2 legacy IDs (II.T25, S024, RN-001, WP-RC-CS-E0-E3, etc.) are preserved as aliases[] on each item and discoverable via search.

Discipline

Per the Corpus v3 Charter:

• CIDs are permanent (never reused after public release)
• Typed aliases are typed-short-ID aliases of the canonical CID
• Atoms contain. Artifacts point. Projections render.
• prrp:// makes prose proofs corpus-addressed (Wave 6)
• Public-closure CI keeps the public graph closed (Wave 8 activates strict enforcement)

The v3 graph is bidirectionally formalization-aware (prose ↔ Lean), machine-readable as JSON-LD on every item page, and exposes its full dependency closure for downstream audit tools.