[Rafael-SOWNet]

Part 3 of #1807: a caller can now ask for the proven pieces of a composed floor or ceiling over a bounded range, and definite integrals use them.

MathS.ExperimentalFeatures.PiecewiseOver(expr, x, from, to) gives expr over [from, to] as the piecewise it is there. Each floor and ceiling of x is replaced by its value on each piece. The pieces partition the range and their ends are exact. An end belongs to the piece whose value it has, which the closedness of each interval says. It returns null wherever the partition cannot be proved complete. It is experimental because the issue asked for the contract to be designed, and no design has been agreed yet.

expr over the range	pieces
floor(x^2) over [0, 2]	0 on [0; 1), 1 on [1; sqrt(2)), 2 on [sqrt(2); sqrt(3)), 3 on [sqrt(3); 2), 4 at x = 2
floor(sin(pi*x*(4 - x)/2)) over [0, 4]	0 on [0; 2 - sqrt(3)), 1 at x = 2 - sqrt(3), 0 on (2 - sqrt(3); 2 - sqrt(2)], -1 on (2 - sqrt(2); 2), 0 at x = 2, -1 on (2; 2 + sqrt(2)), 0 on [2 + sqrt(2); 2 + sqrt(3)), 1 at x = 2 + sqrt(3), 0 on (2 + sqrt(3); 4]
floor(x^2) + ceil(x) over [-1, 2]	0 on [-1; 0], 1 on (0; 1), 2 at x = 1, 3 on (1; sqrt(2)), …
floor(1/x) over [-1, 1]	null: a pole inside the range

How the pieces are proved complete. The ends are the roots of g(x) = k for each whole k in a step argument g's range, taken from the solver and each checked to be exact. Then, between two consecutive ends, g must be shown to reach no whole number. That is done by bisection with intervals that hold every value there (the interval evaluator, now with a variable bound to a range). Each part is settled by one of three tests:

• g lies inside one (k, k + 1);
• g is strictly monotone, with no whole number between its values at the part's ends;
• the part sits beside an end where g = k, and the first derivative that does not vanish there has one sign throughout the part. Then g - k has one sign beside the end, by Taylor's theorem.

The third test is what the sine above needs: its argument touches 1, −1 and 0 at turning points, where g' = 0. A root the solver misses leaves a part that none of the three settles, so the whole answer is declined.

What it declines. A step inside a step's argument, another jump in x, a pole of an argument in the range, and an end where the slope is infinite: floor(sqrt(x)) from 0 declines, while from 1 it gives its pieces.

Definite integrals of a floor or ceiling of something in x, between numeric bounds, are now the sum over the pieces, with an entry in BREAKING-CHANGES.md measured on the 2.6.0 package:

	2.6.0	now
integral(floor(x^2), x, 0, 2)	as written	5 - sqrt(2) - sqrt(3)
integral(floor(2*x), x, 0, 3)	as written	15/2
integral(floor(sin(pi*x*(4-x)/2)), x, 0, 4)	as written	(-2) * sqrt(2)
integral(floor(1/x), x, 1/4, 1)	as written	13/12

BreakpointIntegrationTest.WhatCannotBeSplitIsLeftAsWritten pinned floor(x^2) from 0 to 2 as unsplittable, and that row is removed. The new tests are PiecewiseOverTest (15) and two theories in BreakpointIntegrationTest. The full suite and the MCP tests pass. Indefinite integration is untouched, so the Rubi corpus was not re-run.

🤖 Generated with Claude Code

https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura