Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24
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.

Uniqueness of invariant factors and elementary divisors over a PID

Statement

A finitely generated PID module is classified by its free rank and invariant factors, equivalently its elementary divisors. More precisely, the free rank is unique; invariant factors are unique up to associates in their divisibility order; elementary divisors are unique up to associates and permutation; and two finitely generated modules are isomorphic exactly when these data agree.

Facts & Assumptions

[L1]

The dimensions of pk1M[pk] recover every elementary-divisor exponent multiplicity (p-power torsion dimensions recover the elementary divisors of a PID module).

Proof

technique · constructive
1.1

An isomorphism carries torsion elements to torsion elements, so it induces an isomorphism of torsion submodules and of the quotients by torsion. The latter quotients are finite free, and invariant basis number recovers their common free rank.

given
2.1

For every associate class of irreducible p and every k1, an isomorphism preserves M[pk], multiplication by pk1, and the resulting R/(p)-dimension. By [L1], it therefore preserves every elementary-divisor multiplicity.

L1step 1.1
3.1

Aligning the unique prime-power columns as in the primary-decomposition theorem recovers one divisibility chain of invariant factors up to associates. Hence invariant factors are unique as well. Empty torsion data, pure torsion, pure free, and the zero module are included.

step 2.1algebra
4.1

Conversely, equal free ranks and equal invariant-factor or elementary-divisor data give termwise isomorphisms between the corresponding direct-sum decompositions; their direct sum constructs a module isomorphism. This proves both directions of the classification.

step 3.1constructdischarge-construct

Depends on

Used by

Dependency tree · two levels

18 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