Alphabeta MathHow 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.
Assuming Choice, cardinality of a small category and κ-small diagrams
Definition
Assume the Axiom of Choice (The Axiom of Choice), so every set has a cardinality (A set equinumerous with some ordinal has a least such ordinal, that ordinal is a cardinal, and equinumerous sets get the same one; no choice principle is used, Cardinal sum , product and exponentiation , and why they are written apart from the ordinal operations). For a small category (Small, locally small, and large categories), define
Every object contributes an identity morphism, so this convention also bounds the number of objects. The cardinality of a small diagram (Diagram as a functor from an indexing category) is . For a cardinal , the diagram is -small when .
Depends on
Small, locally small, and large categories
A set equinumerous with some ordinal has a least such ordinal, that ordinal is a cardinal, and equinumerous sets get the same one; no choice principle is used
Cardinal sum , product and exponentiation , and why they are written apart from the ordinal operations
The Axiom of Choice
Diagram as a functor from an indexing category