Alphabeta Math
False statementConstruction: AI-adaptedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16
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.

False: Z/mZZ/n is nonzero for all positive m,n

Statement

False claim: for all positive integers m,n, the tensor product Z/mZZ/n is nonzero.

In fact, with the convention that Z/1 is the zero group,

Z/mZZ/nZ/gcd(m,n).

Thus m=2 and n=3 give a tensor product of two nonzero cyclic groups that is zero.

Facts & Assumptions

Given: Positive integers m,n, and d:=gcd(m,n).

[L1]

For a right module M and an ideal I of a commutative ring R, MRR/IM/IM (MRR/IM/IM naturally).

[L3]

Modular addition and multiplication give Z/q its usual quotient-ring operations (For every natural n, (Z/n,+) is an abelian group, multiplication is a commutative monoid operation, and both distributive laws hold). For positive q, its classes have the unique representatives 0,,q1, so Z/q=q; in particular, Z/1 is zero while Z/2 and Z/3 are nonzero (For n1, every class in Z/n has one representative r with 0r<n, so Z/n=n; while Z/0 is in bijection with Z).

Refutation

technique · direct
1.1

Apply [L1] to M=Z/m and I=nZ to obtain Z/mZZ/n(Z/m)/n(Z/m).

L1L3
1.2

Define ϕ:Z/d(Z/m)/n(Z/m) by ϕ([a]d)=[a]m+n(Z/m). If abdZ=mZ+nZ by [L2], then [ab]m lies in n(Z/m), so ϕ is well-defined.

L2L3
2.1

The map ϕ is surjective because every class in the target is represented by some [a]m. If ϕ([a]d)=0, then [a]m=n[b]m for some integer b, so anbmZ and hence amZ+nZ=dZ by [L2]; therefore [a]d=0, and ϕ is injective.

step 1.2L2L3
3.1

Steps 1.1 and 2.1 give the displayed isomorphism. For (m,n)=(2,3) one has d=1, so the tensor product is Z/1=0 although both Z/2 and Z/3 are nonzero. This refutes the claim.

step 1.1step 2.1L3

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 99 results over 20 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources