Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (openai/gpt-5.4)audited 2026-07-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.

Integer addition and negation are well defined

Statement

The operations [(a,b)]+[(c,d)]=[(a+c,b+d)][(a,b)] + [(c,d)] = [(a+c, b+d)] and −[(a,b)]=[(b,a)]-[(a,b)] = [(b,a)] on Z\mathbb{Z} (Arithmetic on the integers) are independent of the chosen representatives.

Facts & Assumptions

Given: Pairs with (a,b)∼(a′,b′)(a,b) \sim (a',b') and (c,d)∼(c′,d′)(c,d) \sim (c',d') in the sense of The integers as equivalence classes of pairs of naturals.

[A1]

Addition on N\mathbb{N} is commutative and associative.

Proof

technique · direct
1.1

By hypothesis a+b′=b+a′a + b' = b + a'.

given
1.2

By hypothesis c+d′=d+c′c + d' = d + c'.

given
2.1

Adding the two equations: (a+b′)+(c+d′)=(b+a′)+(d+c′)(a + b') + (c + d') = (b + a') + (d + c').

step 1.1step 1.2algebra
2.2

Commuting the equation of step 1.1: b+a′=a+b′b + a' = a + b', which is the defining equation for (b,a)∼(b′,a′)(b,a) \sim (b',a'); negation is well defined.

step 1.1A1
3.1

Regrouping both sides: (a+c)+(b′+d′)=(b+d)+(a′+c′)(a+c) + (b'+d') = (b+d) + (a'+c'), which is the defining equation for (a+c, b+d)∼(a′+c′, b′+d′)(a+c,\, b+d) \sim (a'+c',\, b'+d'); addition is well defined.

step 2.1A1
4.1

Both operations are independent of representatives.

step 3.1step 2.2∎

Depends on

Used by

Cited to discharge well-definedness by Arithmetic on the integers.

Dependency tree · next 3 levels

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