DefinitionDefinition: Literature-sourcedProof: Not applicablePipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-08-27

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Preadditive category

A category $C$ (Category, object, morphism, domain, codomain, identity, composition, and hom-collection) is preadditive when every hom-set $C (A, B)$ is an abelian group and composition is bilinear in the sense that for all composable morphisms $k : A^{'} \to A$ , $f, g : A \to B$ , and $h : B \to B^{'}$ ,

$h \circ (f + g) = h \circ f + h \circ g, (f + g) \circ k = f \circ k + g \circ k .$

The additive identity in $C (A, B)$ is written $0_{A, B}$ and is called the zero element of that hom-group.

Depends on