LemmaStatement: Literature-sourcedProof: 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.

The integer-defining relation is an equivalence relation

Statement

The relation $(a,b) \sim (c,d) \iff a + d = b + c$ on $\mathbb{N} \times \mathbb{N}$ (The integers as equivalence classes of pairs of naturals) is an equivalence relation.

Facts & Assumptions

Given: The relation $(a,b) \sim (c,d) \iff a + d = b + c$ on $\mathbb{N} \times \mathbb{N}$ .

[A1]

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

[A2]

Cancellation in $\mathbb{N}$ : if $x + z = y + z$ then $x = y$ .

Proof

technique · direct

1.1

Reflexivity: for any $(a,b)$ we have $a + b = b + a$ , so $(a,b) \sim (a,b)$ .

1.2

Symmetry: suppose $(a,b) \sim (c,d)$ , i.e. $a + d = b + c$ . Then $c + b = d + a$ , which is the defining equation for $(c,d) \sim (a,b)$ .

1.3

Suppose $(a,b) \sim (c,d)$ and $(c,d) \sim (e,f)$ , i.e. $a + d = b + c$ and $c + f = d + e$ .

given

2.1

Adding the two equations: $(a + d) + (c + f) = (b + c) + (d + e)$ .

step 1.3algebra

3.1

Regrouping both sides: $(a + f) + (c + d) = (b + e) + (c + d)$ .

step 2.1A1

4.1

Cancelling $(c + d)$ : $a + f = b + e$ , so $(a,b) \sim (e,f)$ ; the relation is transitive.

step 3.1A2

5.1

The relation is reflexive, symmetric, and transitive, hence an equivalence relation.

step 1.1step 1.2step 4.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Cited to discharge well-definedness by The integers as equivalence classes of pairs of naturals.

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

T. Tao, Analysis I, 3rd ed., §4.1 (standard reference, not scraped)
L. S. Krapp, Constructions of the real numbers: a set theoretical approach (Oxford, 2014) (standard reference, not scraped)