Corpus Types
A guide to the object types used in the research corpus.
Type grammar
The corpus distinguishes object types so readers do not confuse definitions, lemmas, theorems, constructions, conjectures, remarks, and bridge claims.
The registry already exposes object IDs and book locations. Wave 3 makes the type grammar Corpus-owned metadata so the public page is no longer hand-maintaining these labels independently.
A foundational commitment of the formal kernel.
An introduced object, relation, construction, or term.
A supporting result used by later statements.
A local result or structured claim with narrower scope.
A load-bearing result with stronger downstream use.
A result obtained from prior statements.
Explanatory or interpretive material attached to the formal spine.
An explicit built object or method.
Why type matters
Type labels help readers decide what kind of burden a page carries. A theorem, a conjectural bridge, a definition, and an explanatory remark do not make the same kind of claim.
Reading the common types
-
Axiom: A foundational commitment of the formal kernel.
-
Definition: An introduced object, relation, construction, or term.
-
Lemma: A supporting result used by later statements.
-
Proposition: A local result or structured claim with narrower scope.
-
Theorem: A load-bearing result with stronger downstream use.
-
Corollary: A result obtained from prior statements.
-
Remark: Explanatory or interpretive material attached to the formal spine.
-
Construction: An explicit built object or method.
Save or share this page for inspection
Download a portable dossier, copy a reviewer note, or send this page to someone who can inspect it.