Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passverified 2026-08-10 (gpt-5.6-terra-codex-subscription)
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 number ee is irrational

Statement

The number ee is irrational.

Facts & Assumptions

Given: The series definition of ee (The real exponential function and the number ee by a power series).

[L1]

Factorials are nonzero naturals and obey their recurrence. If k≤nk\le n, then (nk)k!(n−k)!=n!\binom nk k!(n-k)!=n!, so k!k! divides n!n! (The factorial n!n! and the falling factorial nk‾n^{\underline{k}}, defined by recursion in N\mathbb{N}, (nk) k! (n−k)!=n!\binom{n}{k}\,k!\,(n-k)! = n! for k≤nk \le n; hence (nk) k!=nk‾\binom{n}{k}\,k! = n^{\underline{k}}, the quotient n!/(k!(n−k)!)n!/(k!(n-k)!) is a natural number, and (nk)=(nn−k)\binom{n}{k} = \binom{n}{n-k}). Every positive natural has a positive, hence nonzero, canonical real image, and the canonical map preserves products (The canonical natural ι(n)=n⋅1F\iota(n) = n \cdot 1_F of a field, Canonical naturals are positive and strictly increasing).

[L2]

The exponential factorial tail is bounded by A geometric bound for tails of the exponential series.

[L3]

Every rational has an integer representative p/qp/q with positive denominator; every positive integer is the image of a unique natural q≥1q\ge1. The embeddings N↪Z↪Q↪R\mathbb N\hookrightarrow\mathbb Z\hookrightarrow\mathbb Q\hookrightarrow\mathbb R are injective, preserve arithmetic and order, and the integers are closed under finite sums and differences (Every rational has a positive-denominator representative, The naturals embed in the integers, The integers embed in the rationals, The unique embedding of ℚ into an ordered field, The integers form a commutative ring).

Proof

technique · contradiction
1.1

Assume e∈Qe\in\mathbb Q. By [L3], write e=p/qe=p/q in R\mathbb R with p∈Zp\in\mathbb Z and q∈Nq\in\mathbb N, q≥1q\ge1, using the canonical embeddings. Choose a natural n≥max⁡{q,2}n\ge\max\{q,2\} (Every complete ordered field is Archimedean).

assume-contraL3choose
2.1

Put A:=ι(n!)(e−∑k=0n1/ι(k!))A:=\iota(n!)\left(e-\sum_{k=0}^{n}1/\iota(k!)\right). Every tail term is positive, so A>0A>0. Applying [L2] with x=1x=1 and N=nN=n, then using the factorial recurrence, gives A≤2ι(n!)ι((n+1)!)=2ι(n+1)≤23<1A\le \frac{2\iota(n!)}{\iota((n+1)!)} =\frac2{\iota(n+1)} \le\frac23<1 because n≥2n\ge2.

step 1.1L1L2algebra
3.1

The number AA from step 2.1 is an embedded integer. Indeed, for each 0≤k≤n0\le k\le n, [L1] gives a natural sks_k with n!=k!skn!=k!s_k. Also q!=m!qq!=m!q for the natural mm with q=m+1q=m+1, and [L1] at k=qk=q gives q!∣n!q!\mid n!; hence n!=qrn!=qr for some natural rr. By [L3] and multiplicativity of the embeddings, ι(n!)e=pr^,ι(n!)ι(k!)=ι(sk),\iota(n!)e=\widehat{pr},\qquad \frac{\iota(n!)}{\iota(k!)}=\iota(s_k), where pr^\widehat{pr} is the real image of the integer prpr. Therefore AA is a difference of embedded integers and is itself an embedded integer.

step 1.1L1L3algebra
4.1

Since the embedding preserves order, no embedded integer lies strictly between 00 and 11, contradicting steps 3.1 and 2.1. Therefore e∉Qe\notin\mathbb Q.

step 3.1step 2.1L3discharge-contradiction∎

Depends on

Used by

Dependency tree · next 3 levels

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