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 rationals form a field
Statement
with the operations of Arithmetic on the rationals is a field: a commutative ring with in which every nonzero element has a multiplicative inverse.
Facts & Assumptions
Given: Rationals with representatives , second components nonzero.
The operations are independent of representatives (Rational arithmetic is well defined).
is a commutative ring in which (The integers form a commutative ring; because in ).
has no zero divisors and admits cancellation (The integers have no zero divisors; multiplicative cancellation).
Proof
By [L1], each axiom may be verified on fixed representatives.
Associativity of : both and have representative .
Commutativity of : and are equal pairs.
Additive identity: .
Additive inverses: since , [L3] gives . Thus .
Associativity and commutativity of : and .
Multiplicative identity: ; and since .
Distributivity: has representative , while has representative ; cancelling the common nonzero factor these are equivalent.
Inverses: iff iff ; for , .
All field axioms hold: is a field.