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.
and are fields, hence commutative rings, integral domains and ordered rings, all of characteristic
Example
Let be either (The rationals form a field) or (The reals form a field), with its published order (The rationals form a totally ordered field, The reals form a totally ordered field). Then:
- is a commutative ring with and an integral domain (Every field is a commutative ring with ; it is an integral domain, and it is a commutative division ring, Zero divisor, and integral domain: a commutative ring with and no zero divisors);
- with its order is an ordered ring (Ordered ring: a ring with a total order compatible with addition and with positives closed under multiplication), and the set is a positive cone making an ordered field in the sense of Ordered field, whose induced order is the published one;
- (The characteristic of a ring: the least with when one exists, and otherwise).
Facts & Assumptions
Given: is or , with its published operations and order.
and are fields (The rationals form a field, The reals form a field, Field).
The published order on each makes it a totally ordered field: the order is total, implies , and and imply (The rationals form a totally ordered field, The reals form a totally ordered field).
Every field is a commutative ring with , and is an integral domain (Every field is a commutative ring with ; it is an integral domain, and it is a commutative division ring, Ring: an abelian group under addition and a monoid under multiplication, with multiplication distributing over addition on both sides, Commutative ring, Zero divisor, and integral domain: a commutative ring with and no zero divisors).
An ordered ring is a ring with a total order satisfying the two compatibilities of [L2]; for such a ring, satisfies trichotomy and closure and induces the original order (Ordered ring: a ring with a total order compatible with addition and with positives closed under multiplication, The order presentation and the positive-cone presentation of an ordered ring determine each other: satisfies trichotomy and closure, and recovers the order).
An ordered field is a field with a subset satisfying trichotomy (O1) and closure (O2), the order being ; and every ordered field is an ordered ring whose positive cone is (Ordered field, Every ordered field is an ordered ring, and its order is the one its positive cone induces).
In a field, the additive multiple equals the canonical natural of The canonical natural of a field (In a field, the additive multiple is the canonical natural : the additive power of the group-power definition and the canonical natural are the same function, both being the unique one given by the recursion , ).
In an ordered field, for every , the multiples being given by and (Canonical naturals are positive and strictly increasing).
is the least with , or if there is none (The characteristic of a ring: the least with when one exists, and otherwise).
Verification
Claim 1: is a field by [L1], hence a commutative ring with and an integral domain by [L3].
By [L2] the published order on is a total order satisfying (OR1) and (OR2) of Ordered ring: a ring with a total order compatible with addition and with positives closed under multiplication verbatim; with step 1.1 this makes an ordered ring.
By [L4] applied to that ordered ring, satisfies trichotomy and closure, and the relation is the published order. Together with the field structure from step 1.1, trichotomy and closure are exactly axioms (O1) and (O2) of Ordered field, so is an ordered field whose order is the published one. This is claim 2.
By step 3.1 the ordered-field structure of is available, so [L7] applies. Its multiples and the multiples of [L8] are the same elements: both agree with the canonical natural of The canonical natural of a field by [L6], since and both recursions add at each successor. Hence for every natural , and because is not positive by trichotomy.
Claim 3: by step 4.1 there is no natural with , so by [L8].
Claims 1, 2 and 3 are established in steps 1.1, 3.1 and 5.1.
Remarks
-
Two presentations of one order, reconciled here rather than assumed. The published The rationals form a totally ordered field and The reals form a totally ordered field state the order form; the published Ordered field states the positive-cone form. The step establishing claim 2 above passes between them using The order presentation and the positive-cone presentation of an ordered ring determine each other: satisfies trichotomy and closure, and recovers the order, and that is the only reason Canonical naturals are positive and strictly increasing, which is stated for an ordered field, may be applied to and here.
-
The multiples agree with the canonical naturals. By [L6] the element appearing in The characteristic of a ring: the least with when one exists, and otherwise is the of The canonical natural of a field, so claim 3 is also the statement that never takes the value on in these two fields. More is true and is quoted rather than proved here: Canonical naturals are positive and strictly increasing shows is strictly increasing on , hence injective.
-
and are domains for a reason stronger than necessary. They have no zero divisors because every nonzero element is invertible, not because of any cancellation argument; the same reasoning gives nothing about , whose domain property is recorded separately in is an integral domain of characteristic whose group of units is , so it is not a field: is nonzero and not invertible.
Depends on
- Field
- Every field is a commutative ring with $1 \ne 0$; it is an integral domain, and it is a commutative division ring
- Zero divisor, and integral domain: a commutative ring with $1 \ne 0$ and no zero divisors
- Ordered ring: a ring with a total order compatible with addition and with positives closed under multiplication
- The order presentation and the positive-cone presentation of an ordered ring determine each other: $P = \{\, x : 0 < x \,\}$ satisfies trichotomy and closure, and $a < b :\iff b - a \in P$ recovers the order
- Every ordered field is an ordered ring, and its order is the one its positive cone induces
- Ordered field
- The characteristic of a ring: the least $n \ge 1$ with $n \cdot 1_R = 0$ when one exists, and $0$ otherwise
- In a field, the additive multiple $n \cdot 1_F$ is the canonical natural $\iota(n)$: the additive power of the group-power definition and the canonical natural are the same function, both being the unique one given by the recursion $\iota(0) = 0_F$, $\iota(\sigma(n)) = \iota(n) + 1_F$
- The canonical natural $\iota(n) = n \cdot 1_F$ of a field
- Canonical naturals are positive and strictly increasing
- The rationals form a field
- The reals form a field
- The rationals form a totally ordered field
- The reals form a totally ordered field
- Ring: an abelian group under addition and a monoid under multiplication, with multiplication distributing over addition on both sides
- Commutative ring
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 98 results over 29 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
- Field (mathematics) (Wikipedia) (standard reference, not scraped)
- Characteristic (algebra) (Wikipedia) (standard reference, not scraped)
- Thomas W. Judson, Abstract Algebra: Theory and Applications, §16.4: Integral Domains and Fields (standard reference, not scraped)