Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)verified 2026-07-26 (claude-opus-5)
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.

Factorisation of bn−anb^n - a^n, and the resulting Lipschitz estimate

Statement

Let a,b∈Ra, b \in \mathbb{R} and let n∈Nn \in \mathbb{N} with n≥1n \ge 1, with powers as in Integer powers ama^m and finite sums as in Finite sums and finite products, by recursion. Then

bn−an=(b−a)∑k=0n−1akb n−1−k.b^n - a^n = (b - a)\sum_{k=0}^{n-1} a^k b^{\,n-1-k}.

Lipschitz estimate. If 0≤a≤b≤M0 \le a \le b \le M then

0≤bn−an≤nM n−1(b−a),0 \le b^n - a^n \le n M^{\,n-1} (b - a),

where nn denotes the canonical natural ι(n)∈R\iota(n) \in \mathbb{R} (Canonical naturals are positive and strictly increasing, The unique embedding of ℚ into an ordered field). This estimate is the form in which the factorisation is used, later on this page, to prove that nn-th roots exist.

Facts & Assumptions

Given: Elements a,b,Ma, b, M of R\mathbb{R} and a natural n≥1n \ge 1. Define c:N→Rc : \mathbb{N} \to \mathbb{R} by ck=akb n−kc_k = a^k b^{\,n-k} for k≤nk \le n and ck=anc_k = a^n for k>nk > n; only the values c0,…,cnc_0, \dots, c_n occur below.

[L1]

Definition of powers (Integer powers ama^m): a0=1a^0 = 1 and aj+1=ajaa^{j+1} = a^j a.

[L2]

Laws of finite sums (Laws of finite sums and finite products, themselves proved by induction, The principle of mathematical induction): telescoping ∑k<n(ck+1−ck)=cn−c0\sum_{k<n}(c_{k+1} - c_k) = c_n - c_0; scaling ∑k<nλdk=λ∑k<ndk\sum_{k<n}\lambda d_k = \lambda \sum_{k<n} d_k and the constant sum ∑k<nλ=nλ\sum_{k<n}\lambda = n\lambda; and monotonicity, dk≤ekd_k \le e_k for all k<nk < n implies ∑k<ndk≤∑k<nek\sum_{k<n} d_k \le \sum_{k<n} e_k.

[L3]

Laws of integer exponents (Laws of integer exponents): MkM n−1−k=M n−1M^{k} M^{\,n-1-k} = M^{\,n-1} for k≤n−1k \le n-1.

[L4]

Monotonicity of powers (Monotonicity of x↦xnx \mapsto x^n and of n↦ann \mapsto a^n): 0≤x≤y0 \le x \le y implies 0≤xj≤yj0 \le x^j \le y^j.

[L5]

Multiplying inequalities of nonnegatives: 0≤x≤y0 \le x \le y and 0≤u≤v0 \le u \le v imply xu≤yvxu \le yv. Multiplying inequalities of positives states exactly this nonstrict form, alongside the strict one, and it is the only product-of-inequalities move used below. Two instances occur: in step 1.3 with the four nonnegatives ak≤Mka^k \le M^k and b n−1−k≤M n−1−kb^{\,n-1-k} \le M^{\,n-1-k}, and in step 4.1 with 0≤∑k<nakb n−1−k≤nM n−10 \le \sum_{k<n} a^k b^{\,n-1-k} \le nM^{\,n-1} and 0≤b−a≤b−a0 \le b - a \le b - a, which yields (∑k<nakb n−1−k)(b−a)≤nM n−1(b−a)\big(\sum_{k<n} a^k b^{\,n-1-k}\big)(b-a) \le nM^{\,n-1}(b-a). No instance with a possibly negative factor and no strict instance is needed, so the multiplicative order claims of Sign rules for products and monotonicity of multiplication, which are strict and require a nonzero multiplier, are not what carries either move.

Proof

technique · direct
1.1

The consecutive differences of cc factor: for k<nk < n, ck+1−ck=ak+1b n−k−1−akb n−k=akb n−1−k a−akb n−1−k b=akb n−1−k(a−b)c_{k+1} - c_k = a^{k+1} b^{\,n-k-1} - a^k b^{\,n-k} = a^k b^{\,n-1-k}\,a - a^k b^{\,n-1-k}\,b = a^k b^{\,n-1-k}(a - b), using ak+1=akaa^{k+1} = a^k a and b n−k=b n−1−kbb^{\,n-k} = b^{\,n-1-k} b.

L1algebra
1.2

The endpoints of cc are c0=a0b n=bnc_0 = a^0 b^{\,n} = b^n and cn=anb 0=anc_n = a^n b^{\,0} = a^n.

L1algebra
1.3

Now assume 0≤a≤b≤M0 \le a \le b \le M; then for every k<nk < n, 0≤ak≤Mk0 \le a^k \le M^k and 0≤b n−1−k≤M n−1−k0 \le b^{\,n-1-k} \le M^{\,n-1-k}, so 0≤akb n−1−k≤MkM n−1−k=M n−10 \le a^k b^{\,n-1-k} \le M^k M^{\,n-1-k} = M^{\,n-1}.

L3L4L5
1.4

Also b−a≥0b - a \ge 0 and M n−1≥0M^{\,n-1} \ge 0, and bn−an≥0b^n - a^n \ge 0 because 0≤a≤b0 \le a \le b gives an≤bna^n \le b^n.

L4L5
2.1

Telescoping the differences: ∑k<n(ck+1−ck)=cn−c0=an−bn\sum_{k<n}(c_{k+1} - c_k) = c_n - c_0 = a^n - b^n.

step 1.2L2
2.2

Pulling the constant factor out of the same sum: ∑k<n(ck+1−ck)=∑k<nakb n−1−k(a−b)=(a−b)∑k<nakb n−1−k\sum_{k<n}(c_{k+1} - c_k) = \sum_{k<n} a^k b^{\,n-1-k}(a-b) = (a-b)\sum_{k<n} a^k b^{\,n-1-k}.

step 1.1L2
2.3

Summing the bound of step 1.3 over k<nk < n and using monotonicity and the constant sum: ∑k<nakb n−1−k≤∑k<nM n−1=nM n−1\sum_{k<n} a^k b^{\,n-1-k} \le \sum_{k<n} M^{\,n-1} = n M^{\,n-1}.

step 1.3L2
3.1

Comparing the two evaluations gives an−bn=(a−b)∑k<nakb n−1−ka^n - b^n = (a - b)\sum_{k<n} a^k b^{\,n-1-k}, and multiplying both sides by −1-1 gives the stated factorisation bn−an=(b−a)∑k=0n−1akb n−1−kb^n - a^n = (b-a)\sum_{k=0}^{n-1} a^k b^{\,n-1-k}.

step 2.1step 2.2algebra
4.1

Multiplying the inequality of step 2.3 by the nonnegative factor b−ab - a and substituting into the factorisation gives bn−an=(b−a)∑k<nakb n−1−k≤nM n−1(b−a)b^n - a^n = (b-a)\sum_{k<n} a^k b^{\,n-1-k} \le n M^{\,n-1}(b-a); the multiplication is the instance of [L5] with 0≤∑k<nakb n−1−k≤nM n−10 \le \sum_{k<n} a^k b^{\,n-1-k} \le nM^{\,n-1} and 0≤b−a≤b−a0 \le b-a \le b-a, the left-hand nonnegativity holding because every term is nonnegative by step 1.3 and finite sums are monotone. Together with bn−an≥0b^n - a^n \ge 0 this is the Lipschitz estimate.

step 3.1step 1.3step 1.4step 2.3L2L5∎

Depends on

Used by

Dependency tree · next 3 levels

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