Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17
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 algebraic integers are exactly the integers

Statement

A rational number is an algebraic integer if and only if it is an integer. See Integral elements over a commutative ring and algebraic integers.

Facts & Assumptions

Given: The hypotheses and objects in the Statement.

[L1]

Let AB be a homomorphism of commutative rings. An element bB is integral over A when it is a root of a monic polynomial in A[X]. The extension is integral when every element is integral. An algebraic integer is a complex number integral over Z. (Integral elements over a commutative ring and algebraic integers).

[L2]

Let f=anxn++a1x+a0Z[x] with an0. If a reduced rational number r/s, where r,sZ, s>0, and gcd(r,s)=1, is a root of f, then ra0andsan.. (Rational root theorem).

[L3]

(Q,+,,0,1) with the operations of def-rat-operations is a field: a commutative ring with 10 in which every nonzero element has a multiplicative inverse. (The rationals form a field).

[L4]

The map j(k)=[(k,1)] is injective and preserves addition, multiplication, and order. Composing with lem-nat-embeds-int embeds N in Q; we write k for j(k) throughout. (The integers embed in the rationals).

Proof

technique · direct
1.1

We write a rational algebraic integer in lowest terms r/s with s>0.

L1L2L3L4givenalgebra
2.1

It is a root of a monic integer polynomial, so the rational-root theorem makes s1, hence s=1.

step 1.1givenalgebra
3.1

Conversely every integer satisfies the monic polynomial Xn.

step 2.1givenalgebra
4.1

Both are admitted and neither is exceptional. The polynomial Xn of step 3.1 is monic with integer coefficients for every integer n, giving X at n=0 and X+n for n<0; and in step 2.1 the lowest-terms representation covers 0 as 0/1, where the denominator is already 1. This proves the stated claim.

step 2.1step 3.1givenalgebra

Depends on

Used by

Dependency tree · next 3 levels

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