Promote two agreeing one-sided limits over the reals (#719, step 2; #596)

[Rafael-SOWNet]

Step 2 of #719, on top of #755. Closes #596's reported expression.

What was wrong

A two-sided limit is the two one-sided ones agreeing, and AngouriMath could not say so. The branch that compares them compares two ComputeLimitDivideEtImpera results — the bare descent — where a caller who names a side gets that descent and everything behind it: SolveAsIndeterminatePower, l'Hôpital's rule, and the substitution that moves a finite destination out to infinity.

The promotion could not be made before, and #719 says exactly why: the sides did not stay inside the reals. Over the complex plane lim x->0- x^x answers 1 from the continuation, so promoting agreement would give lim x->0 x^x the value 1 — and x^x is not real to the left of 0 at all. LimitTest.TestNoLimit pins it as non-existent.

#755 gave limits a codomain to read. This uses it.

What it does

Only under Domain.Real, and that is exactly what makes it sound: there the offending side has no value to agree with, so the case this could get wrong is the case that no longer arises.

The expression #596 reported, at 0, over the reals:

1 / ln(x + sqrt(x^2 + 1)) - 1 / ln(x + 1)

  left    -1/2          already
  right   -1/2          already
  both    unevaluated  ->  -1/2

What must not be promoted, and is not:

	why
x * ln(x), x ^ x, sqrt(x), ln(x)	real on one side only — nothing to agree with
1/x, abs(x)/x, e^(1/x), arctan(1/x)	both sides real and they disagree — still NaN

A second change, which this exposed

A two-sided limit is now withdrawn if either approach leaves the reals, where the check added in #755 asked about one direction only. lim x->0 sqrt(x) answered 0 while its own left-hand limit had been withdrawn — the two halves disagreeing about the same reading. It belongs in this PR rather than #755 because promoting from the sides is what made the inconsistency visible.

Cost

Asked only where the answer would otherwise be NaN or nothing, so no limit that already answers pays for it. Bounded at a depth of two: each side may itself reach a two-sided limit of a subexpression, and without a bound the two questions branch into four and so on down the tree.

Measured

• Suite 5135 → 5147 passed / 0 failed, F# 130/130.
• Corpus 112/117, 0 wrong / 0 error / 0 timeout, every verdict and answer byte-identical.
• work/rootcheck 596/596 clean, work/propcheck 0 failures.

Nothing changes by default. The complex reading answers as it always has — pinned by tests, including that x^x and x*ln(x) at 0 are still the definite NaN they were.

🤖 Generated with Claude Code