ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17

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.

$Z$ is Noetherian but not Artinian as a module over itself

Example

The regular $Z$ -module $Z$ is Noetherian but not Artinian. See Noetherian modules: every submodule is finitely generated.

Facts & Assumptions

Given: The hypotheses and objects in the Example.

[L1]

A left $R$ -module $M$ is Noetherian when every submodule of $M$ is finitely generated (def-generated-cyclic-finitely-generated-and-free-modules). This finite-generation definition is the convention; its equivalence with ACC and the maximal condition is proved in thm-equivalent-characterizations-of-noetherian-modules. (Noetherian modules: every submodule is finitely generated).

[L2]

A left $R$ -module $M$ is Artinian when every descending chain $M_{0} \supseteq M_{1} \supseteq \dots$ of submodules stabilizes: there is $N$ such that $M_{n} = M_{N}$ for all $n \geq N$ . This is the descending chain condition. (Artinian modules by the descending chain condition).

[L3]

Every subgroup $H \leq (Z, +)$ equals $n Z = ⟨ n ⟩$ for exactly one $n \in N$ ; in particular every subgroup is cyclic. (Every subgroup of $(Z, +)$ is $⟨ n ⟩ = n Z$ for exactly one natural number $n$ ).

Verification

technique · direct

1.1L1L2L3givenalgebra

Every subgroup of $Z$ is principal, so every submodule is finitely generated.

2.1step 1.1givenalgebra

The descending chain $2^{n} Z$ is strict from $n = 0$ onward, showing failure of DCC.

3.1step 2.1givenalgebra∎

The chain of step 2.1 begins at $2^{0} Z = Z$ , the whole module, and each inclusion $2^{n} Z \supseteq 2^{n + 1} Z$ is strict because $2^{n} \notin 2^{n + 1} Z$ ; so the chain never stabilizes and DCC fails from the first term onward. This proves the stated claim.

Depends on

Used by

False statement: every module has a composition series False statement

Dependency tree · two levels

23 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Arvind Nair, Algebra I, Lecture 5 (standard reference, not scraped)

ZZ is Noetherian but not Artinian as a module over itself