[Rafael-SOWNet]

Closes #749 (its remaining half — the first half was withdrawn in a comment there, being #719, which has since landed).

What was wrong

ApplyFirstRemarkable rewrites a vanishing sin(u), tan(u), arcsin(u) or arctan(u) as the u it is equivalent to, and it matches a product or quotient whose own child is one of those functions. It was called on the whole expression, where its sibling one line below is applied at every node.

So a constant factor written to the left pushes the sine one level down and out of reach: 2 * sin(1/x) * x parses as (2 * sin(1/x)) * x, whose children are a product and a variable, and neither is a sine. The descent then reads it as 0 * (+oo) and is definite about it:

lim x->+oo sin(1/x) * x * 2   ->  2      ✅
lim x->+oo 2 * sin(1/x) * x   ->  NaN    ❌   the same product, associated the other way
lim x->+oo sin(1/x) * x / 2   ->  NaN    ❌
lim x->0   sin(x) * 1/x / 2   ->  NaN    ❌

Which side of a product a caller writes a constant on is not a mathematical difference, and simplification produces either.

The fix, and why it is not a Replace

The rule is applied down the product-and-quotient spine, stopping at anything that is not a product or a quotient.

That stop is the whole of what keeps it sound. The equivalence licenses replacing a factor of the expression as a whole — if f/g -> 1 then f*h and g*h go to the same place — and says nothing about a term of a sum, where the difference between f and g is the entire answer. Rewriting the sine inside (sin(x)/x - 1)/x^2 would answer 0 where the limit is -1/6. Those cases are pinned in ASumIsNotRewritten and AConstantFactorOnASumDoesNotOpenItEither:

lim x->0 (sin(x)/x - 1)/x^2        -1/6
lim x->0 (sin(x) - x)/x^3          -1/6
lim x->0 (tan(x) - x)/x^3           1/3
lim x->0 (x - sin(x))/(x - tan(x)) -1/2
lim x->0 2 * (sin(x) - x)/x^3      -1/3

What it costs — a value becoming NaN

Stated plainly, because it is not purely an improvement:

lim x->0 sin(x) * ln(x) * 2      was  0    is  NaN
lim x->0 2 * arctan(x) * ln(x)   was  0    is  NaN
lim x->0 sin(x) * ln(x)          was  NaN  is  NaN   (unchanged — and the reason)

A vanishing factor against a logarithm was being shielded by its constant from a rewrite the library already applies to the same limit written without the constant. The rewrite is sound (sin(x) * ln(x) and x * ln(x) have the same limit); what it exposes is that lim x->0 x * ln(x) is NaN by design — ln(x) is not real to the left of 0, the same judgement that pins lim x->0 x^x in LimitTest.TestNoLimit. So master answered two spellings of one limit differently, and they now agree. Under MathS.Settings.Codomain.Set(Domain.Real) both come back unevaluated, which is the honest answer where there is no real left-hand neighbourhood.

Recorded in BREAKING-CHANGES.md rather than filed under "fixed".

Measured

Generated 811 products and quotients of a vanishing sin/tan/arcsin/arctan against x, 1/x, ln(x), x^2, e^x with constants in every position, at 0 and +oo, and diffed this branch against master:

	count
NaN → a value	196
a value → NaN	13 — all of the trig(u) * ln(x) shape above, each with a constant-free twin already NaN on master
a value → a different value	0

Suites and harnesses, all from a clean build of this branch:

• unit tests 5201 passed, 0 failed (5169 on master; 32 added here, 21 of which fail without the one-line call-site change)
• F# wrapper tests 130 passed
• casbench 112/117 solved, 0 wrong, 0 error, 0 timeout — unchanged
• propcheck 0 failures of 1337 checks
• rootcheck 596/596 clean
• simpsweep 0 disagreements of 10463