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

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

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

[A1]

Addition on $N$ is commutative and associative.

[A2]

Cancellation in $N$ : if $x + z = y + z$ then $x = y$ .

technique · direct

1.1A1

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

1.2A1

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.3given

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

2.1step 1.3algebra

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

3.1step 2.1A1

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

4.1step 3.1A2

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

5.1step 1.1step 1.2step 4.1∎

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

Depends on