LemmaStatement: Literature-sourcedProof: AI-generatedSession-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 rational-defining relation is an equivalence relation

Statement

The relation $(a,b) \sim (c,d) \iff ad = cb$ on pairs of integers with nonzero second component (The rationals as equivalence classes of pairs of integers) is an equivalence relation.

Facts & Assumptions

Given: Pairs $(a,b), (c,d), (e,f)$ of integers with $b, d, f \ne 0$ .

[L1]

$\mathbb{Z}$ is a commutative ring (The integers form a commutative ring).

[L2]

Multiplicative cancellation in $\mathbb{Z}$ : $ud = vd$ with $d \ne 0$ implies $u = v$ (The integers have no zero divisors; multiplicative cancellation).

Proof

technique · direct

1.1

Reflexivity: $ab = ba$ , so $(a,b) \sim (a,b)$ .

1.2

Symmetry: if $ad = cb$ then $cb = ad$ , 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. $ad = cb$ and $cf = ed$ .

given

2.1

Multiplying the first equation by $f$ and the second by $b$ : $adf = cbf$ and $cfb = edb$ .

step 1.3L1

3.1

Chaining: $(af)d = adf = cbf = cfb = edb = (eb)d$ .

step 2.1L1

4.1

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

step 3.1L2

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 rationals as equivalence classes of pairs of integers.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 25 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.2 (standard reference, not scraped)
L. S. Krapp, Constructions of the real numbers: a set theoretical approach (Oxford, 2014) (standard reference, not scraped)