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.

Divisibility is reflexive and transitive on Z\mathbb{Z}, and is linear: if dad \mid a and dbd \mid b then dax+byd \mid ax + by for all integers x,yx, y; also dad \mid a implies dacd \mid ac, da-d \mid a and dad \mid -a

Statement

Let a,b,c,d,x,yZa, b, c, d, x, y \in \mathbb{Z} and let \mid be divisibility (Divisibility in Z\mathbb{Z}: dad \mid a when a=dqa = dq for some integer qq). Then

  1. reflexivity: aaa \mid a;
  2. transitivity: dad \mid a and aba \mid b imply dbd \mid b;
  3. linearity: dad \mid a and dbd \mid b imply dax+byd \mid ax + by; in particular da+bd \mid a + b and dabd \mid a - b;
  4. dad \mid a implies dacd \mid ac;
  5. dad \mid a implies da-d \mid a and dad \mid -a.

Consequently the four statements dad \mid a, da-d \mid a, dad \mid -a and da-d \mid -a are equivalent.

Facts & Assumptions

Given: Integers a,b,c,d,x,ya, b, c, d, x, y.

[L1]

dad \mid a means a=dqa = dq for some qZq \in \mathbb{Z}; a=a1a = a \cdot 1 exhibits aaa \mid a (Divisibility in Z\mathbb{Z}: dad \mid a when a=dqa = dq for some integer qq).

[L2]

Z\mathbb{Z} is a commutative ring: addition and multiplication are associative and commutative, x+0=xx + 0 = x, x1=xx \cdot 1 = x, multiplication distributes over addition, and every xx has an additive inverse x-x, with (x)=x-(-x) = x, (x)y=(xy)(-x)y = -(xy) and (x)(y)=xy(-x)(-y) = xy; we write uvu - v for u+(v)u + (-v) (The integers form a commutative ring, Arithmetic on the integers).

Proof

technique · direct
1.1

Reflexivity: a=a1a = a \cdot 1, so aaa \mid a.

L1L2
1.2

Transitivity: suppose a=dma = dm and b=anb = an. Then b=(dm)n=d(mn)b = (dm)n = d(mn) by associativity, so dbd \mid b.

L1L2
1.3

Linearity: suppose a=dma = dm and b=dnb = dn. Then ax+by=(dm)x+(dn)y=d(mx+ny)ax + by = (dm)x + (dn)y = d(mx + ny) by associativity, commutativity and distributivity, so dax+byd \mid ax + by.

L1L2
1.4

Clause 4: suppose a=dma = dm. Then ac=(dm)c=d(mc)ac = (dm)c = d(mc), so dacd \mid ac.

L1L2
1.5

Clause 5: suppose a=dma = dm. Then a=(d)(m)a = (-d)(-m), so da-d \mid a; and a=(dm)=d(m)-a = -(dm) = d(-m), so dad \mid -a.

L1L2
2.1

The two special cases in clause 3: taking x=y=1x = y = 1 gives da+bd \mid a + b, and taking x=1x = 1, y=1y = -1 gives da1+b(1)=abd \mid a \cdot 1 + b \cdot (-1) = a - b.

step 1.3L2
2.2

The four equivalent forms: clause 5 gives dadad \mid a \Rightarrow -d \mid a and dadad \mid a \Rightarrow d \mid -a; applying each to d-d in place of dd, or to a-a in place of aa, and using (x)=x-(-x) = x, gives the reverse implications, so all four statements are equivalent.

step 1.5L2
3.1

Clauses 1 to 5 and the two consequences are established.

step 1.1step 1.2step 1.3step 1.4step 1.5step 2.1step 2.2

Remarks

Depends on

Used by

…and 5 more results.

Dependency tree · next 3 levels

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