Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28
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.

Integer multiples in a ring: (m+n)a=ma+na(m + n)a = ma + na, m(a+b)=ma+mbm(a + b) = ma + mb, (ma)b=m(ab)=a(mb)(ma)b = m(ab) = a(mb) and (ma)(nb)=(mn)(ab)(ma)(nb) = (mn)(ab) for all m,nZm, n \in \mathbb{Z} and a,bRa, b \in R

Statement

Let RR be a ring (Ring: an abelian group under addition and a monoid under multiplication, with multiplication distributing over addition on both sides). For mZm \in \mathbb{Z} and aRa \in R write mama for the integer power of aa in the additive group (R,+,0)(R,+,0), read in additive notation as in Powers gng^{n}: natural exponents in a monoid and integer exponents in a group, with g0=eg^{0} = e: thus 0a=00a = 0, σ(n)a=na+a\sigma(n)a = na + a for nNn \in \mathbb{N}, and ma=(ka)ma = -(ka) when m<0m < 0 and m-m is the image of kNk \in \mathbb{N} under the embedding of The naturals embed in the integers. Throughout, a natural number written where an integer is expected means its image under that embedding.

Then for all m,nZm, n \in \mathbb{Z} and all a,bRa, b \in R:

  1. (m+n)a=ma+na(m + n)a = ma + na;
  2. m(a+b)=ma+mbm(a + b) = ma + mb;
  3. (ma)b=m(ab)=a(mb)(ma)b = m(ab) = a(mb);
  4. (ma)(nb)=(mn)(ab)(ma)(nb) = (mn)(ab);
  5. ma=(m1)a=a(m1)ma = (m\,1)a = a(m\,1), where 11 is the identity of RR.

No commutativity of RR is assumed. The symbol mama is not a product in RR: an integer is not an element of RR, and claim 5 is the precise statement that the multiple mama is nevertheless a product in RR, namely the product of aa with the ring element m1m\,1.

Facts & Assumptions

Given: A ring RR with zero 00 and identity 11, elements a,bRa, b \in R, integers m,nZm, n \in \mathbb{Z}, and multiples mama as described in the Statement (Ring: an abelian group under addition and a monoid under multiplication, with multiplication distributing over addition on both sides, Powers gng^{n}: natural exponents in a monoid and integer exponents in a group, with g0=eg^{0} = e).

[L1]

(R,+,0)(R,+,0) is an abelian group, (R,,1)(R,\cdot,1) is a monoid, and both distributive laws hold (Ring: an abelian group under addition and a monoid under multiplication, with multiplication distributing over addition on both sides, Group and abelian group).

[L2]

The defining recursion for multiples: 0a=00a = 0 and σ(n)a=na+a\sigma(n)a = na + a for nNn \in \mathbb{N}; and ma=(ka)ma = -(ka) when m<0m < 0 and m=ι(k)-m = \iota(k) (Powers gng^{n}: natural exponents in a monoid and integer exponents in a group, with g0=eg^{0} = e).

[L3]

Exponent laws in a group, read additively in (R,+,0)(R,+,0): (x+y)a=xa+ya(x+y)a = xa + ya; (x)a=(xa)(-x)a = -(xa); y(xa)=(xy)ay(xa) = (xy)a; and x(u+v)=xu+xvx(u+v) = xu + xv whenever uu and vv commute, all for x,yZx, y \in \mathbb{Z} (Exponent laws in a group: gm+n=gmgng^{m+n} = g^{m}g^{n} and (gm)n=gmn(g^{m})^{n} = g^{mn} for all m,nZm, n \in \mathbb{Z}, and (gh)n=gnhn(gh)^{n} = g^{n}h^{n} when gg and hh commute).

[L5]

Induction on N\mathbb{N} (The principle of mathematical induction), and N\mathbb{N} contains 00 (The natural numbers N\mathbb{N} (von Neumann)).

[L6]

ι:NZ\iota : \mathbb{N} \to \mathbb{Z} is injective, preserves addition, multiplication and order, and its image is exactly the nonnegative integers (The naturals embed in the integers, The integers as equivalence classes of pairs of naturals).

[L7]

Z\mathbb{Z} is a totally ordered commutative ring: multiplication on Z\mathbb{Z} is commutative, exactly one of 0x0 \le x and x<0x < 0 holds, and x<0x < 0 implies 0<x0 < -x (The integers form a commutative ring, The integers form a totally ordered ring, Order on the integers, Arithmetic on the integers).

Proof

technique · induction
1.1

Claim 1 is the first exponent law of [L3] read additively in the group (R,+,0)(R,+,0): (m+n)a=ma+na(m+n)a = ma + na.

L1L3
1.2

Claim 2: addition in RR is commutative, so any two elements of (R,+,0)(R,+,0) commute, and the last law of [L3] applies with u=au = a, v=bv = b to give m(a+b)=ma+mbm(a+b) = ma + mb.

L1L3
1.3

Base of claim 3 at the exponent 00: (0a)b=0b=0(0a)b = 0 \cdot b = 0, 0(ab)=00(ab) = 0 and a(0b)=a0=0a(0b) = a \cdot 0 = 0, so all three agree.

baseL2L4
1.4

Inductive hypothesis for claim 3: fix nNn \in \mathbb{N} and assume (na)b=n(ab)(na)b = n(ab) and a(nb)=n(ab)a(nb) = n(ab) for all a,bRa, b \in R.

ih
2.1

Successor step: (σ(n)a)b=(na+a)b=(na)b+ab=n(ab)+ab=σ(n)(ab)(\sigma(n)a)b = (na + a)b = (na)b + ab = n(ab) + ab = \sigma(n)(ab), by the recursion, the right distributive law and the hypothesis; and a(σ(n)b)=a(nb+b)=a(nb)+ab=n(ab)+ab=σ(n)(ab)a(\sigma(n)b) = a(nb + b) = a(nb) + ab = n(ab) + ab = \sigma(n)(ab), by the recursion, the left distributive law and the hypothesis.

step 1.4L1L2
3.1

By induction, (ka)b=k(ab)=a(kb)(ka)b = k(ab) = a(kb) for every kNk \in \mathbb{N} and all a,bRa, b \in R.

step 1.3step 2.1L5
4.1

Negative exponents. Let m<0m < 0, so 0<m0 < -m and m=ι(k)-m = \iota(k) for a unique kNk \in \mathbb{N}. Then (ma)b=((ka))b=((ka)b)=(k(ab))=((k)(ab))=m(ab)(ma)b = (-(ka))b = -((ka)b) = -(k(ab)) = ((-k)(ab)) = m(ab), and likewise a(mb)=a((kb))=(a(kb))=(k(ab))=m(ab)a(mb) = a(-(kb)) = -(a(kb)) = -(k(ab)) = m(ab), using the second clause of the recursion, the sign rules of [L4], step 3.1, and (x)c=(xc)(-x)c = -(xc) from [L3].

step 3.1L2L3L4L6L7
5.1

Claim 3 in full: for mZm \in \mathbb{Z} either 0m0 \le m, in which case m=ι(k)m = \iota(k) for some kNk \in \mathbb{N} and step 3.1 applies, or m<0m < 0, in which case step 4.1 applies; exactly one of the two holds.

step 3.1step 4.1L6L7
6.1

Claim 4: applying claim 3 first with the pair (a,nb)(a, nb) and then with the pair (a,b)(a,b), (ma)(nb)=m(a(nb))=m(n(ab))=(nm)(ab)=(mn)(ab)(ma)(nb) = m\bigl(a(nb)\bigr) = m\bigl(n(ab)\bigr) = (nm)(ab) = (mn)(ab), the third equality being y(xc)=(xy)cy(xc) = (xy)c from [L3] with x=nx = n, y=my = m, and the fourth commutativity of multiplication in Z\mathbb{Z}.

step 5.1L3L7
6.2

Claim 5: applying claim 3 with the pair (1,a)(1,a) gives (m1)a=m(1a)=ma(m\,1)a = m(1 \cdot a) = ma, and applying it with the pair (a,1)(a,1) gives a(m1)=m(a1)=maa(m\,1) = m(a \cdot 1) = ma, using the identity law of the multiplicative monoid.

step 5.1L1
7.1

Claims 1 to 5 are established: claim 1 in step 1.1, claim 2 in step 1.2, claim 3 in step 5.1, claim 4 in step 6.1 and claim 5 in step 6.2.

step 1.1step 1.2step 5.1step 6.1step 6.2discharge-induction

Remarks

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 59 results over 19 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