Repository navigation
Limits should read the codomain, so that agreeing one-sided limits can be promoted #719
Description
Split out of #596, where @Happypig375 proposed the design: "setting the codomain to real should just make the limit two sided".
The problem
A two-sided limit is the two one-sided ones when they agree. That promotion cannot be applied today, because 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; each is the complex continuation approached from the left. So promoting agreement would also turn lim x->0 (x*ln x) into 0 and lim x->0 x^x into 1, and both are deliberately NaN -- the second is pinned by LimitTest.TestNoLimit, because x^x is not real for x < 0.
The guard has to reject the whole promotion because it cannot tell that case apart from the honest one. The codomain is exactly the missing information.
The plan
ComputeLimitreadsMathS.Settings.Codomain. UnderDomain.Real, a one-sided limit whose value comes from the complex continuation has no value rather than the continued one -- solim x->0- ln(x)stops answering-oo.- With (1) in place, promote agreeing one-sided limits to a two-sided answer under a real codomain.
1/ln(x + sqrt(x^2+1)) - 1/ln(x+1)at 0 then answers-1/2two-sided, which is what Unexpected behavior of limits #596 reported, withoutx*ln(x)orx^xgaining a value they should not have. - Under
Domain.Complexthe current answers stand unchanged.
What has to be re-measured, not assumed
Step 1 changes what every existing one-sided limit answers under a real codomain. LimitTest.TestNoLimit, the one-sided limit tests, and work/casbench all have to be re-run and read rather than expected to pass. This is the subsystem where a plausible-looking change has broken things more than once, so the order matters: land step 1 with its measurements first, step 2 separately.
Tests pinning both one-sided values of the #596 expression already exist (added in #714), so step 2 has somewhere to land.
Activity
Let limits be told whether they are being read over the reals (#719, …
Promote two agreeing one-sided limits over the reals (#719, step 2; #596
Rafael-SOWNet commentedon Aug 6, 2026
Both steps are done.
Step 1 — PR #755.
MathS.Settings.Codomain, defaulting toDomain.Complexso nothing changes for anyone who does not ask. UnderDomain.Reala limit approached through values the function does not take is withdrawn rather than answered from the continuation:One correction to the plan in this issue: it says "
ComputeLimitreadsMathS.Settings.Codomain" as though the setting existed. It did not —Codomainwas a per-nodeEntityproperty only, and adding the setting was part of the work.Two things step 1 cost, both now comments in the code:
ApplyFirstRemarkableit overflows the stack.(1 + x)^(1/x)at1e-9is1.000000001raised to a billion at a hundred digits, six times 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, so the guard withdraws on evidence and never on its absence.Step 2 — PR #756. Agreeing one-sided limits are promoted, under
Domain.Realonly — which is what makes it sound, since there the offending side has no value to agree with. The expression this issue was split out of (#596) now answers:and the two cases the guard existed to protect are untouched:
x*ln(x)andx^xat 0 are real on one side only, so there is nothing to agree with, and1/x,abs(x)/x,e^(1/x),arctan(1/x)have sides that disagree and are stillNaN.Step 2 also exposed something step 1 had half-done: a two-sided limit was being withdrawn on one direction of approach only, so
lim x->0 sqrt(x)answered 0 while its own left-hand limit had been withdrawn. Fixed in #756, since promoting from the sides is what made the two halves visibly disagree about the same reading.Measured across both: suite 5107 → 5147 passed / 0 failed, F# 130/130, corpus 112/117 with every verdict and answer byte-identical,
rootcheck596/596,propcheck0 failures.LimitTest.TestNoLimitstill means what it meant, and that is pinned by tests rather than assumed.What this does not do, and why it is worth leaving open elsewhere rather than here: the setting is read by the limit machinery only. #752 (
sqrt(x^2) -> x,sqrt(-x) -> i*sqrt(x)) and #536 (collapsing a piecewise) want the same information read by the simplifier, and #721 wants it unified withprovided ... in RR. Those are each their own change; the thing they were all waiting on now exists.