Floor/Ceil composition contract: exact substitution and usable jump analysis

[Happypig375]

What you ran: An application uses Floor/Ceil as both symbolic operations and plotted functions. The smallest correctness reproducer on AngouriMath 2.5.0 is:

open AngouriMath

let x : Entity.Variable = "x"
let two = MathS.FromString("2")
let four = MathS.FromString("4")
let child = MathS.Sin(MathS.pi * x / two)
let rounded = MathS.Floor(child)

printfn "%O" (rounded.Substitute(x, four).InnerSimplified)
// -1

let childAtFour = child.Substitute(x, four).InnerSimplified
printfn "%O" childAtFour
printfn "%O" (MathS.Floor(childAtFour).InnerSimplified)
// 0
// 0

The first result should also be 0: the substituted argument is exactly sin(2*pi) = 0. The construction order changes the result.

The application also constructs these ordinary compositions:

floor(x^2)
floor(x^2/2)
floor(sin(pi*x*(4-x)/2))
ceil(sin(pi*x*(4-x)/2))

It needs to evaluate them exactly at authored rational checkpoints, compile them for plotting, and, where provable on a bounded real interval, obtain their constant pieces and exact jump/endpoint ownership for later integration or differentiation.

What it did:

There are three separate parts to the integration contract.

1. Exact substitution can give the wrong integer. The reproducer above returns -1 because the already-wrapped expression reaches Floor from the negative side of a numerically evaluated trigonometric zero. Simplifying the child first produces exact zero and the correct Floor. Current master at 2d3dc6a still routes an exact Rational through EDecimal.Floor/Ceiling (Floor source, Ceil source). The broader finite-precision number-design problem is already tracked in Will we have a powerful and quick enough simplifier to avoid equating small numbers to 0? #1376; this issue is not presenting the known 100+ digit near-integer case as a new discovery.

2. Compilation was an application blocker in 2.5.0. rounded.Compile([| x |]) throws UncompilableNodeException, so the same expression that is displayed symbolically cannot use AngouriMath's fast evaluator for a plot. Solve throws UncompilableNodeException when its Newton fallback meets floor, max or another node the compiler has no form for #1603 covered Floor/Ceil as part of a solver-fallback failure. Current master has since added both fast-expression instructions (Floor/Ceil compiler) and LINQ forms (LINQ compiler). That appears to resolve the compiler part for the next release; it is recorded here so this integration requirement is not mistaken for a duplicate request.

3. A caller cannot yet obtain a complete, checkable partition for nonlinear compositions. Current master has careful breakpoint integration, but its Floor/Ceil recognition is deliberately limited to the direct argument x (break recognition, unit-step recognition). floor(x^2) and the sine composition therefore remain unevaluated under anchored integration. Differentiation returns the mathematically useful almost-everywhere condition 0 provided not argument in ZZ (source); that is not a claim that the full composition is or is not differentiable at every preimage of an integer, and it does not expose the one-sided information a renderer needs.

I searched open and closed issues for Floor/Ceil compilation and sine evaluation. #1603 is the related compilation report, and #1376 is the related v3 exact-versus-approximate number-design discussion. I did not find an existing issue for the substitution-order error or for a public, completeness-reporting jump analysis of composed Floor/Ceil.

What it should have done:

For exact symbolic evaluation:

• substituting x = 4 into floor(sin(pi*x/2)) and then simplifying should return exact 0, independent of whether the child was simplified before it was wrapped;
• exact Rational Floor/Ceil should be decided from numerator and denominator, without first rounding through EDecimal;
• exact and approximate evaluation should have an explicit contract. If the side of an integer cannot be proved in exact mode, retaining the Floor/Ceil node is safer than returning a guessed integer. The wider redesign can remain with Will we have a powerful and quick enough simplifier to avoid equating small numbers to 0? #1376.

For numerical plotting, the compiled Floor/Ceil support now on master should remain covered for both compiler paths and for nonlinear children such as x^2 and sin(pi*x/2).

For downstream symbolic consumers, a useful result would be either:

• a public piecewise/jump analysis over a caller-supplied bounded real domain, returning proven constant pieces with exact boundary expressions and open/closed ownership; or
• an explicit incomplete/unresolved result when those boundaries cannot be proved.

This need not promise a general closed-form integral or distributional derivative. Leaving Integralf unevaluated is valid, and the current conditional derivative is useful as an almost-everywhere statement. The required distinction is that an unresolved integral, an almost-everywhere derivative, or an incomplete jump search must remain visibly unresolved rather than being usable as proof that a composed rounded curve is numerically valid everywhere. Such an API would let applications render and validate the cases AngouriMath can prove while declining the rest honestly, instead of each application building its own partial piecewise solver.

[Rafael-SOWNet]

Measured on 2.5.0 and on master 2d3dc6a8:

• Substitution order. floor(sin(pi*x/2)) at x = 4 is -1 on 2.5.0 and 0 on master, by InnerSimplified, Simplify and Evaled alike: sin(2 pi) evaluates to an exact zero there, where 2.5.0 gave -6.48e-50.
• Exact Rational Floor/Ceil. Still wrong on master for a rational with more digits than the precision: floor(10^120 - 1/3) is 10^120. The floor and the ceiling of a rational are exact whatever its size #1810 takes it from the numerator and denominator. In exact mode a Real whose side of an integer is unknown already stays written.
• Compilation. On master, as you say.
• Jump analysis over a bounded domain for composed Floor/Ceil is a feature; I've left it open here rather than in The floor and the ceiling of a rational are exact whatever its size #1810.