Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-01
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.

Picard iteration from 11 produces the exponential partial sums

Statement

Define u0(x)=1u_0(x)=1 and ur+1(x)=1+∫0xur(t) dtu_{r+1}(x)=1+\int_0^x u_r(t)\,dt. Then ur(x)=∑k=0rxkι(k!)u_r(x)=\sum_{k=0}^{r}\frac{x^k}{\iota(k!)} and ur→exp⁡u_r\to\exp uniformly on every bounded interval. Moreover, exp⁡(x)=1+∫0xexp⁡(t) dt,\exp(x)=1+\int_0^x\exp(t)\,dt, and differentiating this integral equation recovers exp⁡′=exp⁡\exp' = \exp and exp⁡(0)=1\exp(0)=1.

Facts & Assumptions

Given: The displayed recursion with the oriented integral of The integral with oriented limits: ∫aaf:=0\int_a^a f := 0 and ∫baf:=−∫abf\int_b^a f := -\int_a^b f.

[L1]

For k∈Nk\in\mathbb N, the derivative of tk+1/ι(k+1)t^{k+1}/\iota(k+1) is tkt^k (For a natural n≥1n \ge 1 the function x↦xnx \mapsto x^{n} is differentiable everywhere with derivative ι(n) x n−1\iota(n)\,x^{\,n-1}; for n=0n = 0 it is the constant 11, with derivative 00; for a natural n≥1n \ge 1 the function x↦x−nx \mapsto x^{-n} is differentiable at every x≠0x \ne 0 with derivative −ι(n) x−n−1-\iota(n)\,x^{-n-1}; consequently every polynomial function is differentiable at every real, with the derivative computed term by term), so the second fundamental theorem evaluates its oriented integral (The second fundamental theorem: if GG is differentiable on [a,b][a,b] with G′=fG' = f and ff is integrable, then ∫abf=G(b)−G(a)\int_a^b f = G(b)-G(a), The integral with oriented limits: ∫aaf:=0\int_a^a f := 0 and ∫baf:=−∫abf\int_b^a f := -\int_a^b f); the integral is linear over finite sums (Integrable functions on [a,b][a,b] form a set closed under sums and scalar multiples, and ∫ab(λf+μg)=λ∫abf+μ∫abg\int_a^b(\lambda f+\mu g) = \lambda\int_a^b f + \mu\int_a^b g), and the factorial recurrence is The factorial n!n! and the falling factorial nk‾n^{\underline{k}}, defined by recursion in N\mathbb{N}.

[L2]

The exponential series has infinite radius (The exponential series converges absolutely for every real argument, The real exponential function and the number ee by a power series), and a power series converges uniformly on compact subintervals of its interval of convergence (A power series converges absolutely and uniformly on every closed interval strictly inside its interval of convergence).

[L3]

Polynomial functions are continuous (Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function); uniform limits of continuous real functions are continuous (The uniform limit of continuous real-valued functions on a metric space is continuous); continuous functions on compact intervals are integrable (A continuous function on [a,b][a,b] is Riemann integrable, by Heine-Cantor and Riemann's criterion); uniform limits interchange with Riemann integration (A uniform limit of Riemann-integrable functions is Riemann integrable, and its integral is the limit of their integrals); and the first fundamental theorem differentiates an integral of a continuous function (The first fundamental theorem: if ff is integrable on [a,b][a,b] and continuous at cc, then F′(c)=f(c)F'(c) = f(c); in particular a continuous ff has FF as a primitive).

Proof

technique · induction
1.1

At r=0r=0, u0=1u_0=1, the stated finite sum.

basegiven
1.2

If the formula holds at rr, integrate its finite sum termwise from 00 to xx. By [L1], the integral of tk/ι(k!)t^k/\iota(k!) is xk+1/ι((k+1)!)x^{k+1}/\iota((k+1)!), giving the formula at r+1r+1.

ihL1given
2.1

Hence the iterates are precisely the partial sums of the exponential series. Its infinite radius and [L2] give uniform convergence on every bounded interval.

step 1.1step 1.2L2given
3.1

Fix xx and work on the compact interval with endpoints 00 and xx. The polynomial iterates are continuous and integrable there, and step 2.1 gives uniform convergence to exp⁡\exp. Thus [L3] lets the integrals in ur+1(x)=1+∫0xur(t) dtu_{r+1}(x)=1+\int_0^x u_r(t)\,dt pass to the limit, giving exp⁡(x)=1+∫0xexp⁡(t) dt\exp(x)=1+\int_0^x\exp(t)\,dt, with the orientation supplied by The integral with oriented limits: ∫aaf:=0\int_a^a f := 0 and ∫baf:=−∫abf\int_b^a f := -\int_a^b f when x<0x<0.

step 2.1L3given
4.1

Step 2.1 and [L3] make exp⁡\exp continuous. The first fundamental theorem applied to step 3.1 gives exp⁡′(x)=exp⁡(x)\exp'(x)=\exp(x), and setting x=0x=0 gives exp⁡(0)=1\exp(0)=1.

step 2.1step 3.1L3discharge-induction∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 175 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