Unify Codomain with a "provided ... in RR" condition

[Rafael-SOWNet]

Split out of #596, where @Happypig375 asked: "how to make codomains unified with provided node with the in relation?"

The two look like the same test and are not quite.

• MathS.Settings.Codomain is a statement about where the function is being read -- real-valued or complex-valued.
• provided x in RR is a statement about the point.

lim x->0- (x^x) is a limit at a real point of a function that is not real-valued anywhere to the left of it. So the predicate x in RR holds and tells you nothing, while the codomain is what rules the limit out. Unifying them means reading the condition as a claim about the neighbourhood rather than the point -- which is probably what is meant, and is a real change rather than an alias.

Worth doing: a single notion would mean expr provided x in RR and Codomain = RR cannot drift apart, and it would let a domain be stated locally rather than as a global setting. But it is wider than reading MathS.Settings.Codomain in ComputeLimit, which is why the sibling issue does the narrow thing first.

Filed so the question is not lost inside #596.

[Rafael-SOWNet]

Asked what other systems do here, and measured rather than recalled. The answer is fairly uniform, and
it is not what this library does.

What SymPy does

Measured on SymPy 1.14:

log(-3, -3)                                  # 1
log(-3)                                      # log(3) + I*pi
continuous_domain(log(x), x, S.Reals)        # Interval.open(0, oo)
log(x).is_real                               # None
log(Symbol('xp', positive=True)).is_real     # True

Three things worth separating out of that:

1. Evaluation is complex and unconditional. log(-3, -3) is 1, exactly as this library evaluates
   it. Nothing anywhere says the expression is undefined.
2. The real domain is a separate query — continuous_domain(f, x, S.Reals) — computed on demand,
   with the reading passed as an argument. It is not a property the expression carries.
3. Facts about a point live on the symbol, as assumptions (Symbol('x', positive=True)), and are
   answered three-valued: True, False, or None for "not known".

What Mathematica does

FunctionDomain[f, x] — "finds the largest domain of definition of the real function f of the variable
x". Its documentation says the domain argument's "possible values for dom are Reals and Complexes.
The default is Reals", and the domain is computed per call rather than stored on the expression.

Same shape as SymPy: a query, with the reading as a parameter.

(I could not verify Maxima's domain flag from its manual — the single-page HTML is too large to fetch
the entry — so I am not claiming anything about it.)

Where this library differs

Neither system bakes a real-analysis domain into the node. This one does, and the contradiction #890
reports follows directly from it:

eval(log(-3, -3))     =>  1
domain(log(-3, -3))   =>  False
eval(log(-3, 9))      =>  0.2179... - 0.6231...i

Logf.IntrinsicCondition is b > 0 and not b = 1 and x > 0 — a real-domain answer, fixed at
construction — while evaluation runs over ℂ and returns complex values happily. So the library declares
an expression undefined everywhere and simultaneously gives it a value.

The change that matches both systems is to make the reading a parameter of the query rather than a
property of the node: DomainCondition(Domain) instead of DomainCondition, defaulting to the
ambient MathS.Settings.Codomain for compatibility. That is option two of the fork in #890, and it is
the ordinary design elsewhere.

Incidentally, domain(log(x, x)) is x > 0 and not x = 1 and x > 0 — the same conjunct twice, because
base and antilogarithm are the same expression. Worth a Simplify on the conjunction whatever is
decided.

What it wins back, concretely

This is the part I was asked to check, and the answer is that the win is concentrated in exactly the
places that have blocked work recently — not speculative.

1. boundcheck goes from 2 disagreements to 1, immediately. One of the two remaining is
log(x, x) -> 1 provided x > 0, and that condition is precisely the baked-in real domain. Over ℂ,
log_x(x) is ln x / ln x, which is 1 for every x outside {0, 1} — measured: log(-3, -3) is
1 here and in SymPy. So with the reading parameterised, the condition becomes
not x = 1 and not x = 0, the x = -3 disagreement disappears, and the rule gets stronger rather than
weaker.

2. #876's provided x in RR conditions stop being over-strong. Since #907 made the connectives
three-valued, x < 0 and x = 0 evaluates to False for every x — including x = i, because
i = 0 is decidably false and False and u is False. Simplify still answers
False provided x in RR, so it is now weaker than evaluation on that row. A local statement of the
reading is what makes the condition expressible at the strength the reduction actually needs.

3. #902's two lost limits come back. This is the one that already cost correct answers.
(x^2)^x / e^(2*x*ln(x)) and x^x / e^(x*ln(x) - ln(x)) are unevaluated since #903, because
ln(a^c) = c*ln(a) needs a > 0 and there is no way to tell the simplifier that it holds on the
approach. I implemented the limit-side reader at three insertion points and measured each: the rewrite
fires correctly and the limits stay unevaluated, because Simplify's own candidate search rebuilds the
logarithm and asks again. A pre-pass cannot fix that; an assumption traveling with the expression can.

4. The ln(a) + ln(b) -> ln(ab) guard stops being a trade. That is boundcheck's other remaining
disagreement, wrong at x = -3 by 2*pi*i. Guarding it costs the log-equation solver coverage, the
same trade #903 took. With an assumption channel the rule can fire under a condition instead of
declining, so the guard costs nothing.

So: one existing disagreement fixed by the cheap half, one wrong answer fixable without a coverage
trade, two correct answers restored, and a class of guard-versus-coverage decisions that stops needing
to be made one rule at a time.

The two halves are separable, and only one is expensive

• Parameterising the query by the reading is small, matches SymPy and Mathematica, and settles DomainCondition says log(-3, -3) is defined nowhere and it evaluates to 1; log(1, 1) is 0 and should be NaN #890's
  contradiction plus win 1. It needs no new mechanism.
• Assumptions attached to variables — SymPy's Symbol('x', positive=True), three-valued — is what
  buys wins 2, 3 and 4. That is Goal: Math OS — a ten-year vision for AngouriMath as an open mathematical reasoning platform #746's tier 1 ("assumptions travelling with nodes") and a much larger
  piece.

The first does not require the second, which is worth knowing before scoping it.

The cost, named

A unified notion would have to fix what Providedf already does badly, since it becomes the carrier:
a condition competes on complexity, so attaching one can make a better form lose; and it
travels, escaping a binder (#878 §3), with
a single NaN condition collapsing a whole Piecewise. Those are recorded in
Docs/Contributing/SimplificationContract.md §2 as costs of the mechanism as it stands, and they would
stop being avoidable.

[Rafael-SOWNet]

Correcting my own comment above, on the strength of a measurement.

I listed four things the second half — assumptions attached to variables — would buy. Win 4 was wrong, and it was the one I was most confident about.

4. The ln(a) + ln(b) -> ln(ab) guard stops being a trade. [...] With an assumption channel the rule can fire under a condition instead of declining, so the guard costs nothing.

I guarded both rules with Patterns.Power.cs's own IsPositiveReal idiom and ran the suite. The cost is not a trade and not coverage:

• Three failures — SimplifyTest.PowerRulesTest for ln(a) + ln(b) and ln(a) - ln(b), which are the rules' own tests, and OneSidedLimitTest.ADifferenceOfReciprocalLogarithms(Left).
• A hang. The run does not finish — three and a half hours against a normal five minutes. Under --blame-hang the offending test is among RemarkableLimitAfterSimplificationTest, RealCodomainLimitTest.AgreeingOneSidedLimitsArePromoted, StirlingFactorialLimitTest, PowerQuotientGatheringTest and SolveOneEquation.LinearTrigRoots. Four of the five are limit tests.

The limit machinery expands logarithms (LogarithmExpanded, Limits/Transformations.cs) and relies on the simplifier to gather them back. Remove the gathering and some limit paths stop reaching a fixed point. That is a termination dependency, and no assumption about a and b discharges it — the limit machinery's own expansion is what creates those operands in the first place.

So this rule is not an argument for per-symbol assumptions. The move it actually wants is #802's, and there is a worked precedent eight rules up in the same file: a^n / b^n -> (a/b)^n was guarded for exactly this reason, cost (x^2 + 1)^x / (x^2)^x its limit, and was repaired by teaching the limit reader to recognise the quotient itself, where IsEventuallyPositive can require the bases to be positive on the approach (ApplySecondRemarkable). Note that repair also needed a thread-static re-read bound, which the logarithm path has no equivalent of — the likeliest reason its symptom is a hang rather than a lost answer.

Wins 1, 2 and 3 are untouched by this. Win 1 shipped in #916.

Written up as §11 of SimplificationContract.md in #917, with the acceptance criteria for whoever takes it: guard in place, boundcheck at 0 disagreements, those three tests passing, the suite finishing in five minutes, and no limit answer lost.

The general lesson is the one this tracker keeps re-teaching in both directions: a predicted interaction is worth exactly what it has been measured at. work/TRIAGE.md had recorded this cost as "the log-equation solver loses coverage", which is a third thing again, and also not what happens.

[Rafael-SOWNet]

Correcting my own comment above a second time, and this one retires the second half's last named consumer.

I wrote that wins 2 and 3 needed assumptions attached to variables, and that the two limits #902 withdrew were the case a rule fix could not reach — the identity is load-bearing inside Simplify's candidate search, so supplying it from the limit side does not get there. That was measured, at three insertion points, with a stack trace showing the rule asked 117 times inside one l'Hopital descent.

The measurement was sound and the conclusion drawn from it was not. All three insertion points were pre-passes — a Replace before Simplify, the exponent SolveAsIndeterminatePower builds, the differentiated quotient in ApplylHopitalRuleImpl. A pre-pass rewrites the expression and hands it on, so it cannot reach a search that rebuilds the logarithm behind it. That is a fact about pre-passes, not about limit-side repairs.

An ambient scope is not a pass, and #922 built one after that comment was written. The thread-static Approach is consulted by the rule, so it is answered wherever the rule is asked — candidate search included. Applying the same move to Logf(b, Powf(a, c)) answers both limits, on the default complex reading:

	was	is
lim x->+oo (x^2)^x / e^(2*x*ln(x))	unevaluated	1
lim x->+oo x^x / e^(x*ln(x) - ln(x))	unevaluated	+oo

#925. No assumption mechanism arrived, and none was needed.

One of the two was never as lost as the record said. x^x / e^(x*ln(x) - ln(x)) comes back as +oo on stock master with nothing but Codomain.Set(Domain.Real), because #903's own guard takes the real reading as sufficient. "Lost" meant "lost under the default reading" throughout, and nothing said so.

What this leaves the second half

Nothing open is waiting on it. Win 4 was withdrawn on measurement (it wanted #802's move, and the cost was termination rather than coverage — #922). Wins 2 and 3 were the two limits above, and they wanted #922's move. Win 1 shipped in #916 and needed no new mechanism at all.

So all four of the wins I listed for per-symbol assumptions have now been taken by something else, and each time the something else was cheaper. That is not an argument that expression metadata is a bad idea — it is #746's tier 1 and it stays there — but it does mean it is a design goal with no consumer measured, and building it now would be building it speculatively. The next person here should find a consumer first.

The distinction worth keeping, since this tracker has now got it wrong in both directions

Two repairs look alike and are not:

	reaches	example
the machinery rewrites a shape it matches directly	what the machinery constructs	#802, ApplySecondRemarkable
the rule asks an ambient scope for a condition	that, and what Simplify constructs for itself	#922's gathering, and #925

Prefer the second whenever the rule is one the simplifier's own alternation depends on, and do not conclude from a failed pre-pass that an assumption channel is required. Written up as §12 of SimplificationContract.md.

The general lesson is the one I wrote in the comment above, pointed the other way: a predicted interaction is worth exactly what it has been measured at — and so is a predicted impossibility.