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

Identities and inverses in a field are unique

Statement

In a field F (Field) the additive identity, the multiplicative identity, each additive inverse, and each multiplicative inverse are unique. Hence the notations 0, 1, −x, and x−1 denote well-defined elements, as the field definition and its consequences assume.

Facts & Assumptions

Given: A field F satisfying the axioms (A), (M), (D) (Field).

[L1]

(F,+) is an abelian group with identity 0: addition is associative and commutative and x+0=x for all x; and (F∖{0},⋅) is an abelian group with identity 1: multiplication is associative and commutative and x⋅1=x for all x≠0 (Field).

Proof

technique · direct
1.1

The additive identity is unique: if 0 and 0′ both satisfy x+0=x and x+0′=x for all x, then 0′=0′+0=0+0′=0, using that 0 is an identity, commutativity, and that 0′ is an identity.

L1
1.2

Additive inverses are unique: if a and b both satisfy x+a=0 and x+b=0, then a=a+0=a+(x+b)=(a+x)+b=0+b=b, using associativity and commutativity.

L1
1.3

The same two arguments in the abelian group (F∖{0},⋅) give uniqueness of the multiplicative identity, 1′=1′⋅1=1⋅1′=1, and of multiplicative inverses: if xa=1 and xb=1 with x≠0, then a=a⋅1=a(xb)=(ax)b=1⋅b=b (using ax=xa=1).

L1
2.1

Therefore 0, 1 and, for each x, its additive inverse −x and (for x≠0) its multiplicative inverse x−1 are the unique elements with their defining properties, so all four notations are well-defined.

step 1.1step 1.2step 1.3∎

Depends on

Used by

Cited to discharge well-definedness by Field.

Dependency tree · one level

1 result within one dependency step of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources