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.
Class-sized category theory in ZFC: definable-class schemas, small and locally small categories, and why is not formed
The word class in this development is an abbreviation for a formula in the language of set theory, as described by The first-order language of set theory: , , formulas with parameters, and class abbreviations. It is not an additional set. A category may therefore have a definable class of objects and a definable class of morphisms. Quantification over such a category is a schema: each use expands to an ordinary formula of ZFC.
A category is small when its objects and morphisms form sets, and locally small when each hom-collection is a set. The category used below has small categories as objects; its hom-categories are sets or locally small categories as asserted in the relevant result. We do not form a category of all large categories. Doing so as though all classes were members of a larger set would conflict with the same size obstruction exhibited for the ordinals by Burali-Forti: there is no set of all ordinals. Class recursion, when used, is only the definable schema licensed by Transfinite recursion.