Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27
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.

For rational p>0p > 0, ∑1/kp\sum 1/k^p converges iff p>1p > 1

Statement

Let p∈Qp \in \mathbb{Q} with p>0p > 0. For a natural number k≥1k \ge 1 write ι(k)=k⋅1R\iota(k) = k \cdot 1_{\mathbb{R}} for the canonical natural, which is positive (Canonical naturals are positive and strictly increasing), and write kp:=ι(k)pk^{p} := \iota(k)^{p} for its rational power (Rational powers ara^r of a positive base). Then

∑k≥11kp converges⟺p>1.\sum_{k \ge 1} \frac{1}{k^{p}} \ \text{converges} \qquad \Longleftrightarrow \qquad p > 1 .

In particular the harmonic series ∑k≥11/k\sum_{k \ge 1} 1/k diverges, at p=1p = 1, and ∑k≥11/k2\sum_{k \ge 1} 1/k^{2} converges, at p=2p = 2.

The index range is not cosmetic. The series starts at k=1k = 1 because 1/0p1/0^{p} is undefined: Rational powers ara^r of a positive base gives 0p=00^{p} = 0 for rational p>0p > 0, and 00 has no inverse. Sequences here are functions on N\mathbb{N} and N\mathbb{N} contains 00 (Series, partial sums, convergence and the sum, divergence, and the tail series), so the object named above is a series from the starting index 11 in the sense of Series, partial sums, convergence and the sum, divergence, and the tail series, not a series of a sequence on N\mathbb{N}.

The exponent is rational, and that is a limitation of this page. Rational powers of a positive base are what Rational powers ara^r of a positive base supplies; real exponents require the exponential and the logarithm, which this library develops later. The statement above is therefore the full pp-series theorem for every exponent this page can name.

Facts & Assumptions

Given: A rational p>0p > 0 and the family ak:=1/kp=ι(k)−pa_k := 1/k^{p} = \iota(k)^{-p}, defined for naturals k≥1k \ge 1 (Rational powers ara^r of a positive base, Series, partial sums, convergence and the sum, divergence, and the tail series).

[L1]

Rational powers of a positive base are positive, and ar+s=arasa^{r+s} = a^{r}a^{s}, (ar)s=ars(a^{r})^{s} = a^{rs}, a−r=1/ara^{-r} = 1/a^{r} for a>0a > 0 and rationals r,sr, s (Laws of rational exponents).

[L2]

Monotonicity of rational powers: for rational t>0t > 0 and 0<a<b0 < a < b one has at<bta^{t} < b^{t}; and for a>1a > 1 and rationals r<sr < s one has ar<asa^{r} < a^{s} (Monotonicity of r↦arr \mapsto a^{r} and of a↦ara \mapsto a^{r}).

[L3]

The integer power and the rational power agree at an integer exponent: for a>0a > 0 and n∈Zn \in \mathbb{Z}, ana^{n} read as in Integer powers ama^m equals ana^{n} read as in Rational powers ara^r of a positive base, since n=n/1n = n/1 and a1/1=aa^{1/1} = a (Existence and uniqueness of nn-th roots: a unique a1/n≥0a^{1/n} \ge 0 with (a1/n)n=a(a^{1/n})^n = a, Rational powers ara^r of a positive base). In particular a0=1a^{0} = 1.

[L4]

Reciprocation reverses the order on the positives: 0<a<b0 < a < b implies 0<1/b<1/a0 < 1/b < 1/a (Inverses of positives are positive, and reciprocation reverses order).

[L5]

Condensation: for a family (xk)k≥1(x_k)_{k \ge 1} that is nonnegative and nonincreasing, ∑k≥1xk\sum_{k \ge 1} x_k converges if and only if ∑j≥02jx2j\sum_{j \ge 0} 2^{j} x_{2^{j}} converges (For a nonincreasing nonnegative sequence, ∑ak\sum a_k converges iff ∑2ka2k\sum 2^k a_{2^k} converges, Nondecreasing, increasing, nonincreasing, decreasing, monotone, and eventually monotone sequences).

[L6]

The geometric series: ∑j≥0rj\sum_{j \ge 0} r^{j} converges if and only if ∣r∣<1|r| < 1 (For ∣r∣<1|r| < 1, ∑k≥0rk=1/(1−r)\sum_{k \ge 0} r^k = 1/(1-r), and for ∣r∣≥1|r| \ge 1 the series diverges, Basic properties of the absolute value).

[L7]

The canonical naturals are positive and order preserving: 0<ι(1)≤ι(j)<ι(k)0 < \iota(1) \le \iota(j) < \iota(k) for naturals 1≤j<k1 \le j < k, and ι(2)=2>1\iota(2) = 2 > 1 (Canonical naturals are positive and strictly increasing).

Proof

technique · direct
1.1

For every natural k≥1k \ge 1 the base ι(k)\iota(k) is positive, so ak=ι(k)−pa_k = \iota(k)^{-p} is defined and positive; in particular the family is nonnegative.

givenL7L1
1.2

For naturals 1≤j<k1 \le j < k we have 0<ι(j)<ι(k)0 < \iota(j) < \iota(k), hence ι(j)p<ι(k)p\iota(j)^{p} < \iota(k)^{p} since p>0p > 0, hence aj=1/ι(j)p>1/ι(k)p=aka_j = 1/\iota(j)^{p} > 1/\iota(k)^{p} = a_k; and for j=kj = k the two are equal. So aj≥aka_j \ge a_k whenever 1≤j≤k1 \le j \le k.

givenL7L2L4L1
1.3

For every j∈Nj \in \mathbb{N} the base 2j2^{j} is positive and, reading the exponent jj as a rational, 2ja2j=2j(2j)−p=2j⋅2−jp=2 j−jp=2 (1−p)j=(2 1−p)j2^{j} a_{2^{j}} = 2^{j} \big(2^{j}\big)^{-p} = 2^{j} \cdot 2^{-jp} = 2^{\,j - jp} = 2^{\,(1-p)j} = \big(2^{\,1-p}\big)^{j}.

L1L3L7algebra
1.4

Since 2>12 > 1, the map t↦2tt \mapsto 2^{t} is strictly increasing on Q\mathbb{Q} and 20=12^{0} = 1; hence r=2 1−p<1=20r = 2^{\,1-p} < 1 = 2^{0} holds exactly when 1−p<01 - p < 0, that is exactly when p>1p > 1.

L2L3L7
2.1

Condensation applies to (ak)k≥1(a_k)_{k \ge 1}: ∑k≥1ak\sum_{k \ge 1} a_k converges if and only if ∑j≥02ja2j\sum_{j \ge 0} 2^{j} a_{2^{j}} converges.

step 1.1step 1.2L5
2.2

So the condensed series is the geometric series ∑j≥0rj\sum_{j \ge 0} r^{j} with r:=2 1−pr := 2^{\,1-p}, and r>0r > 0, so ∣r∣=r|r| = r.

step 1.3L1L3
3.1

By the geometric series theorem, ∑j≥0rj\sum_{j \ge 0} r^{j} converges if and only if r<1r < 1.

step 2.2L6
4.1

Chaining the three equivalences: ∑k≥11/kp\sum_{k \ge 1} 1/k^{p} converges   ⟺  \iff the condensed series converges   ⟺  \iff r<1r < 1   ⟺  \iff p>1p > 1.

step 2.1step 2.2step 3.1step 1.4∎

Remarks

  • Where the threshold comes from. Condensation turns the pp-series into a geometric series of ratio 21−p2^{1-p}, and the geometric threshold r=1r = 1 pulls back to p=1p = 1. Nothing about the number 11 is special to the pp-series; it is the exponent at which the condensed terms stop shrinking.

  • At p=1p = 1 the condensed series is ∑j≥01\sum_{j \ge 0} 1. Its terms do not tend to 00, so it diverges, and with it the harmonic series. That instance is worked out on the companion page, together with the older block argument that does not use condensation at all.

  • Only rational exponents are covered, and the gap is real. For irrational pp the expression kpk^{p} has no meaning in this library yet, so the statement is not merely unproved there, it is unstatable. The same limitation is what keeps the Bertrand-type series ∑1/(k(log⁡k)p)\sum 1/(k (\log k)^{p}) off this page entirely, the logarithm not being available.

Depends on

Used by

Dependency tree · next 3 levels

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