Let limits be told whether they are being read over the reals (#719, step 1)

[Rafael-SOWNet]

Step 1 of #719. Step 2 — promoting agreeing one-sided limits — is deliberately not here; see the bottom.

What was wrong

AngouriMath's one-sided limits do not stay inside the reals:

lim x->0- ln(x)        -oo
lim x->0- x * ln(x)    0
lim x->0- x ^ x        1

None of those is a real limit. The logarithm of a negative real is ln|x| + i*pi, and what comes back is the magnitude of something that is not a real number at any point of the approach.

#719 names why this matters beyond the three lines: a two-sided limit is the two one-sided ones agreeing, and that promotion cannot be made while the sides answer from the complex continuation — it would give lim x->0 x^x the value 1, which the suite pins as non-existent because x^x is not real for negative x. The guard has to refuse the whole promotion because it cannot tell that case from the honest one. The codomain is exactly the missing information.

What this adds

MathS.Settings.Codomain — a statement about the reading, where an Entity's own Codomain is a statement about a node.

Domain.Complex by default, so nothing changes for anyone who does not ask. The default is pinned by tests against the values themselves, not against the setting's value.

Under Domain.Real:

	default	Domain.Real
lim x->0- ln(x)	-oo	unevaluated
lim x->0+ ln(x)	-oo	-oo
lim x->0- x * ln(x)	0	unevaluated
lim x->0+ x * ln(x)	0	0
lim x->0- x ^ x	1	unevaluated
lim x->0- sqrt(x)	0	unevaluated
lim x->-oo ln(x)	answers	unevaluated
lim x->0 sin(x)/x	1	1
lim x->0 (1 + x)^(1/x)	e	e

It is the approach that is judged, not the expression — which is why the same expression is withdrawn on one side and untouched on the other.

How it decides, and which way it errs

Whether a function takes non-real values near a point is not a property of the tree, so the approach is sampled. The direction of error is chosen deliberately: a sample that will not evaluate, or comes back non-finite, is passed over rather than counted, and an expression carrying a second variable is not judged at all. The answer is only ever "yes, demonstrably" or "not shown" — a limit is withdrawn on evidence, never on the absence of it.

Two things this cost, both in the code as comments

• The check must run before the rewrites, not after. Each rewrite asks for limits of its own; under this reading those come back unevaluated, and evaluating an unevaluated limit asks for it again through the same rewrite, without end. Placed after ApplyFirstRemarkable it overflows the stack — which is how it was found.
• The samples stop at a thousandth, for cost rather than principle. The sample point goes into the expression, and an expression may put it in an exponent: (1 + x)^(1/x) at 1e-9 is 1.000000001 raised to a billion, at a hundred digits, six times over on every limit the machinery takes. A 20 ms limit became a timeout. Sampling less far in only ever misses, and a miss answers exactly as before.

Under a real codomain limits are slower — (1 + x)^(1/x) at 0+ is 273 ms against 20 — because the sampling sits on the recursive path. Opt-in and measured rather than hidden.

Measured

• Suite 5107 → 5135 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.

What is not here

Step 2, the promotion of agreeing one-sided limits to a two-sided one, which is the point of the setting. #719 asks for step 1 to land with its own measurements first, because it changes what every one-sided limit answers under a real codomain, and this is the subsystem where a plausible-looking change has broken things more than once. A test pins the unpromoted state so the next step has somewhere to land.

One correction to #719 for whoever picks up step 2: it says "ComputeLimit reads MathS.Settings.Codomain" as though the setting existed. It did not — adding it was part of the work, and it is what this PR is.

🤖 Generated with Claude Code