Gather logarithms only where that is exact, and tell the limit machinery where it is going

[Rafael-SOWNet]

Closes boundcheck's last disagreement. 1 → 0.

ln(a) + ln(b) = ln(a*b) is false off the positive reals, and both it and its Minusf sibling were applied unconditionally:

"ln(x) + ln(x+1)" at x = -3     1.7918 + 6.2832i
gathered to ln(x*(1+x))         1.7918              — what was returned

The two differ by 2*pi*i, the turn of the argument the principal branch discards.

Why it could not simply be guarded

Guarding it is not a coverage trade. The limit machinery expands logarithms and relies on the simplifier to gather them back, so withdrawing the rule makes the suite stop finishing — a hang, not a lost answer. Measured before this PR: three failures and a run that passed three and a half hours against a normal five minutes.

That is what makes this #802's case. The identity has to move to where it is checkable, not be deleted — the same repair a^n / b^n -> (a/b)^n already had.

Where it is checkable is a stated approach

A limit knows where the expression is going, which is the one thing a simplification rule cannot work out for itself. On the way to a destination the sign of each operand is decidable, so the limit machinery states the approach and the rule consults it:

• a sum needs both operands positive;
• a difference needs only that their signs agree — ln of a negative is ln|.| + pi*i, and that cancels in a difference while it would double in a sum.

The negative case is not an edge. A destination at -oo is normalised by substituting -x, so lim x->-oo (x-5)^x / x^x arrives as ln(-x) - ln(-(x+5)) with both operands negative.

Four things that had to be measured, each wrong first

This is the part worth reading, because none of it was reachable by argument:

1. A limit solver never fires — the machinery never asks a sub-limit for that node.
2. A rewrite in the limit pipeline is reached zero times.
3. The gathering happens inside the simplifier's own candidate search. With the approach stated around only the first Simplify, the rule was reached 192 times for that limit, with the right operands, and found no approach to check against every time. It has to be stated for the whole computation.
4. Stating it only at the two +oo-normalised entries left it correct but 6× slower — 37.8s against 6.4s on Unexpected behavior of limits #596's limit — because a rule that declines leaves the search to explore what it would have collapsed. The memo that looked like the fix for that made no difference at all, which is how the real cause was found.

Both of the placements that failed were deleted rather than left in, once removing them and re-measuring showed nothing depended on them.

Guards

The sign memo is keyed by destination as well as expression and shared by every approach inside the outermost one; it is dropped when that one exits. Re-entry is bounded. The approach is withdrawn while its own check runs, so the limits it asks cannot come back through the same door. A plain Simplify after a limit still refuses to gather — there is a test for it.

Measured

Rebased onto a3c7554f, the polynomial layer (#918), and re-measured against it — every figure below is on that base, not the one this branch was cut from.

	master a3c7554f	here
boundcheck disagreements	1	0
simpsweep (62778 point comparisons)	0	0
C# tests	6948	6948, 0 failed
F# tests	130	130
suite wall clock	~4m57s	4m57s, no hang

Timings for the two limits this touches, taken on the previous base where the comparison was made directly: lim x->0- 1/ln(x+sqrt(x^2+1)) - 1/ln(x+1) 6.4s → 6.9s, and lim x->-oo (x-5)^x / x^x 1.2s → 1.3s.

Numbers still gather: ln(2) + ln(3) is ln(6), ln(6) - ln(2) is ln(3). What no longer happens is the same rewrite on a symbol, which may be anything.

The changed answers are in BREAKING-CHANGES.md under Unreleased — since 2.1.0, alongside #918's.

Not in scope

This is not per-symbol assumptions (#721's second half). It is the narrower thing that consumer actually needed, and the measurement above is the argument for why: no assumption on a and b discharges a termination dependency, because the limit machinery's own expansion is what creates the operands.