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.
Depth is bounded by support dimension
Statement
Assume the Axiom of Choice (The Axiom of Choice). For every nonzero finite module over a Noetherian local ring , The nonzero hypothesis is essential for this formulation: under the adopted convention , whereas the empty support has no nonnegative Krull dimension.
Facts & Assumptions
Given: The Axiom of Choice; is nonzero and finite over the Noetherian local ring .
Depth is the supremum of lengths of regular sequences in the maximal ideal, including the empty sequence (Depth with respect to an ideal).
Under the assumed AC, the depth of a nonzero finite local module is at most its support dimension (A finite local module has depth at most its dimension).
Proof
By [L1], depth is a supremum of a set containing zero, so it is nonnegative. The AC-qualified supplier [L2] gives the upper bound.
These give the displayed double inequality. The last sentence follows directly from the separately declared zero-module depth convention.