Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (openai/gpt-5.4)audited 2026-07-25
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 reciprocal on the rationals is well-defined

Statement

On Q∖{0}\mathbb{Q} \setminus \{0\} the reciprocal [(a,b)]−1:=[(b,a)][(a,b)]^{-1} := [(b,a)] (Arithmetic on the rationals) is independent of the chosen representative: if (a,b)∼(a′,b′)(a,b) \sim (a',b') with a,a′,b,b′≠0a, a', b, b' \ne 0, then (b,a)∼(b′,a′)(b,a) \sim (b',a'). Hence the reciprocal is a well-defined function on Q∖{0}\mathbb{Q} \setminus \{0\}.

Facts & Assumptions

Given: Nonzero rationals represented by integer pairs (a,b)(a,b) and (a′,b′)(a',b') with a,a′,b,b′≠0a, a', b, b' \ne 0, where (x,y)∼(z,w)  ⟺  xw=zy(x,y) \sim (z,w) \iff x w = z y in Z\mathbb{Z} (The rationals as equivalence classes of pairs of integers).

[L1]

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

Proof

technique · direct
1.1

By hypothesis (a,b)∼(a′,b′)(a,b) \sim (a',b'), that is ab′=a′ba b' = a' b in Z\mathbb{Z}.

given
2.1

Commuting each product by [L1], b′a=ba′b' a = b a', hence ba′=b′ab a' = b' a.

step 1.1L1
3.1

The equation ba′=b′ab a' = b' a is exactly the defining relation (b,a)∼(b′,a′)(b,a) \sim (b',a'), and since a,a′≠0a, a' \ne 0 the pairs (b,a),(b′,a′)(b,a), (b',a') are legal rational representatives; therefore [(a,b)]−1=[(b,a)]=[(b′,a′)]=[(a′,b′)]−1[(a,b)]^{-1} = [(b,a)] = [(b',a')] = [(a',b')]^{-1}, so the reciprocal is well-defined on Q∖{0}\mathbb{Q} \setminus \{0\}.

step 2.1given∎

Depends on

Used by

Nothing in the library uses this result yet.

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

Dependency tree · next 3 levels

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