A series whose terms do not vanish is +oo, not left as written

[Rafael-SOWNet]

Closes the question you raised on #1218 — "can you really assume that integral(floor(x)^floor(x), x, 1, +oo) cannot be solved, or is it just missing a solver?" It was missing a solver. It is +oo.

What it answers

sum(2^k, k, 0, +oo) and sum(k, k, 1, +oo) were left as written. They have no finite value, and saying nothing was the only thing missing — the nth-term test settles them. Terms that do not tend to zero mean the series diverges; the sign of the limit says which infinity, because where the terms tend to a positive L they are eventually all above L / 2, so the partial sums pass every bound. A negative limit gives -oo the same way, and the finitely many terms before that point are finite and cannot change it.

What it refuses, which is most of the design

• A limit of zero. This is the case the test says nothing about, not a gap in the implementation: sum(1/k) diverges and sum(1/k^2) converges and the terms of both tend to 0. Answering either from here would be a guess.
• A limit that does not exist. sum((-1)^k, k, 0, +oo) has no value rather than an infinite one. I am deliberately not inferring "the limit does not exist" from "the limit did not compute" — those arrive identically and only one of them licenses an answer.
• A pole in the index, which is the trap worth naming. One undefined term makes the sum undefined, not infinite: sum(k / (k - 5), k, 0, +oo) has terms tending to 1, so a reader that consulted only the limit would answer +oo and be wrong about k = 5. Rather than hunt for poles, the index is allowed to occur only where none can arise — under +, -, *, and three power shapes (k^3, 2^k, n^n). Division by anything containing the index, a factorial of it, a logarithm of it are refused outright.

That structural check runs before the limit, which is also what keeps it cheap: a summand this cannot speak about never reaches the limit engine, and it is only consulted at all after every closed form has declined.

One wrinkle worth recording: the step split hands over n ^ n provided not n = 0 or n > 0, because 0 ^ 0 is the one power that must say what it assumes. A condition true for every index in range is dropped; one that is not leaves the Providedf in place, where the pole check declines it. ExponentialSeries has a sibling of this specialised to factorial clauses — the vocabularies do not overlap, and a third caller would be the moment to merge them rather than now.

Measured

Both columns on builds, 102911be against this branch:

	was	is
sum(2^k, k, 0, +oo), sum(k, k, 1, +oo), sum(k^2 + 1, k, 0, +oo), sum(n^n, n, 1, +oo)	left as written	+oo
sum(-k, k, 1, +oo), sum(-2^k, k, 0, +oo)	left as written	-oo
integral(floor(x)^floor(x), x, 1, +oo)	left as written	+oo
sum(1/k, k, 1, +oo), sum(1/k^2, …), sum((-1)^k, …), sum(k / (k - 5), …)	left as written	the same
sum(2^(-k), k, 0, +oo), sum(x^k / k!, k, 0, +oo), sum(2^k, k, 0, 5)	2, e^x, 63	the same

Pins that moved, and why

Four pinned examples used an infinite range as their illustration of a summation that stays unevaluated, and three are no longer that:

• BreakpointIntegrationTest asserted integral(floor(x)^floor(x), x, 1, +oo) stayed an Integralf, with a comment I wrote on A geometric series is summed in closed form #1218 saying it would move to the value the day a divergence test existed. It has.
• GeometricSeriesTest listed sum(2^k, k, 0, +oo) under "not a geometric series". That reader still declines it — a ratio at or beyond 1 has no sum — but the chain now answers it, so the example moved rather than the claim.
• ClosedFormSummationTest and SyntaxDocumentedTest each used sum(k, k, 1, +oo) to illustrate a bound the polynomial closed form declines. Their other examples still make that point; the infinite one no longer does.

Docs/Usage/Syntax.md gains a paragraph, since what a sum to +oo does is now a documented behaviour rather than an absence.

Checks

DivergentSeriesTest, 27 cases: seven diverging to +oo, three to -oo, three vanishing limits, two non-existent limits, three poles, the two condition cases, what still converges, finite ranges, a symbolic lower bound, and the sheet's integral. Full suite in two chunks: 8471 and 1485 pass.

One unrelated failure appeared once in the first chunk and not on re-run of the same binary: FractionFreeDeterminantTest, which is the concurrency defect filed as #1219. I have added the sighting there — the notable part is that the test is seeded, so the 300 matrices are identical between runs, and a different matrix failed this time than the first, which rules out anything data-dependent and points at a race.

🤖 Generated with Claude Code

https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura