Read an exponent out of a logarithm where a limit says the base holds its sign (#902)

BREAKING-CHANGES.md

@@ -26,6 +26,7 @@ read first.
 | **silent** | `ln(x).DomainCondition` | `x > 0` | `not x = 0` |
 | **silent** | `"x ^ n".Differentiate("x").Simplify()` | `x ^ n * n / x provided x > 0` — `NaN` at every negative `x` | `x ^ n * n / x provided not x = 0` |
 | **silent** | `ln(a) + ln(b)` and `ln(a) - ln(b)` for symbolic `a`, `b` | `ln(a * b)`, `ln(a / b)` — wrong by `2*pi*i` off the positive reals | left as written |
+| **silent** | `lim x->+oo (x^2)^x / e^(2*x*ln(x))` and `lim x->+oo x^x / e^(x*ln(x) - ln(x))` | unevaluated, the deliberate loss 2.1.0 recorded | `1` and `+oo`, the answers from before 2.1.0 |
 | **silent** | `"x^5 + 2x^3 - 2x^2 - 4".SolveEquation("x")` | three of the five roots, one of them a float | all five, exact |
 | | `"x^4 + x^2 + 1".SolveEquation("x")` | `sqrt((-1 - sqrt(-3)) / 2)` and its three companions | `(-1 - sqrt(-3)) / 2` and its three, with no nested radical |
 | | `"x^4 + 3x^2 + 2".SolveEquation("x")` | `{ sqrt(-2), -sqrt(-2), i, -i }` | the same four, in the order the factors are found |
@@ -110,6 +111,47 @@ creates the pairs that only this puts back together.
 
 From [#721](https://github.com/asc-community/AngouriMath/issues/721).
 
+### An exponent under a logarithm is read again, where a limit says the base holds its sign
+
+2.1.0 withdrew `log_b(a^c) = c * log_b(a)` from an undecided argument, because it is false off
+`ln`'s principal strip, and recorded two limits as the price:
+
+| | 2.1.0 | now |
+|---|---|---|
+| `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` |
+
+Both are answered again, and by the same route the logarithm gathering above takes: a stated
+approach. The identity needs `Im(c * ln a)` inside `(-pi, pi]`; a base that holds a positive sign on
+the way to the destination makes `ln a` real, and an exponent that is real along the approach leaves
+the product real, so there is nothing for the principal branch to discard. Both halves are
+answerable while a limit is being read and neither is answerable to a simplifier reading an
+expression on its own account — so **outside a limit the rule still declines**, and `ln(e^x)` is
+still left as written. That half now has a test of its own, because widening the guard until an
+ordinary `Simplify` applies the identity would restore the wrong answer
+[#902](https://github.com/asc-community/AngouriMath/issues/902) reported while every limit above
+kept passing.
+
+The exponent's realness is decided structurally and conservatively rather than read off a limit: a
+positive *limit* does not make a base real on the way to it, since `x + i*sin(x)` tends to `+oo` off
+the real line. A power is admitted only with a whole exponent or a decidably positive base, because
+`(-2)^(1/2)` is imaginary; a second variable carries no approach and is refused. Anything unlisted
+is refused too, which costs coverage and never correctness.
+
+**What this corrects is a recorded prediction, not only a lost answer.** 2.1.0's entry said these two
+wanted "an assumption travelling with the expression — `#746`'s tier 1 and the subject of
+[#721](https://github.com/asc-community/AngouriMath/issues/721) — and not another pass", on the
+strength of three insertion points that were each tried and each failed. That measurement was
+sound and the conclusion drawn from it was not: all three were *pre-passes*, which rewrite the
+expression before `Simplify` is called and cannot reach the candidate search that rebuilds it. An
+ambient scope is not a pass. The rule itself asks whether an approach is being read, so it is
+answered wherever the rule is asked — including 117 times inside one l'Hopital descent. No
+assumption mechanism arrived, and none was needed.
+
+`boundcheck` stays at **0** disagreements, and the suite finishes in its usual time — the failure
+mode to watch for here is a hang rather than a wrong answer, since the limit machinery's own
+expansion creates the shapes these rules put back.
+
 ### The logarithm's domain follows the reading, as every other node's already did
 
 `Arcsinf`, `Arccosf`, `Arcsecantf` and `Arccosecantf` each state one condition over the reals and

Sources/AngouriMath/Docs/Contributing/SimplificationContract.md

@@ -406,3 +406,43 @@ Recorded because each was ruled out by measurement and none was reachable by arg
 
 The last of those is the one worth generalising: **withdrawing a rewrite has a cost in search, not
 only in coverage**, and that cost is invisible until something is timed.
+
+## 12. The same move takes the second rule, and retires a prediction
+
+`log_b(a^c) = c * log_b(a)` was withdrawn from an undecided argument by
+[#902](https://github.com/asc-community/AngouriMath/issues/902) for the same reason as the gathering
+above — it is false off `ln`'s principal strip — and it cost two limits over `(x^2)^x` and `x^x`.
+Those were recorded as needing *an assumption travelling with the expression*, on the strength of
+three insertion points that were each implemented, instrumented and measured to fail.
+
+**The measurement was sound; the conclusion was not.** All three were pre-passes. A pre-pass rewrites
+the expression and hands it on, so it cannot reach the candidate search that rebuilds the logarithm
+behind it — which is precisely what the 192-times and 117-times counts above were showing. The
+ambient approach of §11 is a different mechanism: the *rule* asks it, so it is answered wherever the
+rule is asked, candidate search included. Applying it to this second rule answers both limits, on the
+default complex reading, with no assumption mechanism anywhere.
+
+**The distinction to carry to the next unsound rule.** 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 | §11's gathering, and this |
+
+Prefer the second whenever the rule is one the simplifier's own alternation depends on. Ask which
+kind is needed before promising a limit-side guard, and do not conclude from a failed pre-pass that
+an assumption channel is required.
+
+**What the condition has to be, and why it is not read off a limit.** A positive limit does not make
+a base real on the way to it: `x + i*sin(x)` tends to `+oo` off the real line. So the base and the
+exponent are both required to be real *along* the approach, decided structurally — closed
+subexpressions that evaluate to a finite real, the approach variable itself, and sums, products,
+quotients and absolute values of those. A power joins only with a whole exponent or a decidably
+positive base, since `(-2)^(1/2)` is imaginary. A second variable carries no approach and is refused,
+as is anything unlisted: the list costs coverage and never correctness, which is the right way round.
+
+**Outside a limit the rule still declines, and that half needs its own test.** Widening the guard
+until an ordinary `Simplify` applies the identity restores #902's wrong answer — `ln(e^x)` as `x`,
+which at `x = 3*pi*i` is `9.4247i` where the expression is `pi*i` — while every limit that motivated
+the change keeps passing. A rewrite earned under a stated approach must be shown to be *unavailable*
+without one.

Sources/AngouriMath/Functions/Continuous/Limits/Transformations.cs

@@ -380,6 +380,85 @@ internal static bool MayGatherLogarithmsHere(Entity left, Entity right, bool isD
             finally { SwapApproach(previous); gatherLogarithmsDepth--; }
         }
 
+        /// <summary>
+        /// Whether <c>log_b(a^c) = c * log_b(a)</c> may be applied here, which it may only while
+        /// an approach is being read, and only where <paramref name="base"/> holds a positive
+        /// sign on it and <paramref name="exponent"/> is real along it.
+        /// </summary>
+        /// <remarks>
+        /// The identity needs <c>Im(c * ln a)</c> inside the strip <c>(-pi, pi]</c>. A base that
+        /// is positive on the approach makes <c>ln a</c> real, and a real <c>c</c> then leaves the
+        /// product real, so there is nothing for the principal branch to discard. Both halves are
+        /// answerable here and neither is answerable to a simplifier reading the expression on its
+        /// own account, which is why the rule declines there.
+        /// <para/>
+        /// The approach is withdrawn for the duration of the sign check, as in
+        /// <see cref="MayGatherLogarithmsHere"/>, so the limits it asks for cannot come back
+        /// through this same door.
+        /// https://github.com/asc-community/AngouriMath/issues/902
+        /// </remarks>
+        internal static bool MayTakeLogOfPowerHere(Entity @base, Entity exponent)
+        {
+            if (currentApproach is not { } approach || logOfPowerDepth >= MaxLogOfPowerDepth)
+                return false;
+            // A destination off the real line is not an approach along it, and then nothing below
+            // can be said about the variable.
+            if (approach.Dest.Evaled is not Real)
+                return false;
+            // The sign check below reads the base's limit, and a limit being positive does not
+            // make the base real on the way to it -- x + i*sin(x) tends to +oo off the real line.
+            if (!IsRealAlong(@base, approach.X) || !IsRealAlong(exponent, approach.X))
+                return false;
+            logOfPowerDepth++;
+            var previous = SwapApproach(null);
+            try
+            {
+                return MemoisedSign(@base, approach) == 1;
+            }
+            finally { SwapApproach(previous); logOfPowerDepth--; }
+        }
+
+        /// <summary>
+        /// How deep <see cref="MayTakeLogOfPowerHere"/> may re-enter itself, for the reason
+        /// <see cref="MaxGatherLogarithmsDepth"/> gives: it asks for a limit, and that limit runs
+        /// the machinery the question was asked from.
+        /// </summary>
+        private const int MaxLogOfPowerDepth = 1;
+
+        [System.ThreadStatic] private static int logOfPowerDepth;
+
+        /// <summary>
+        /// Whether <paramref name="expr"/> is real wherever <paramref name="x"/> is, decided
+        /// structurally. On an approach to a real destination the variable runs along the real
+        /// line, which is the one thing that makes this answerable for a symbol at all.
+        /// </summary>
+        /// <remarks>
+        /// A power is admitted only with a whole exponent or a decidably positive base, because a
+        /// real raised to a real leaves the real line as soon as the base goes negative:
+        /// <c>(-2)^(1/2)</c> is imaginary. Any other symbol answers <see langword="false"/>, since
+        /// a second variable carries no approach and may be complex. Anything unlisted answers
+        /// <see langword="false"/> as well, which costs coverage and never correctness.
+        /// </remarks>
+        private static bool IsRealAlong(Entity expr, Variable x)
+        {
+            // Anything closed that evaluates to a finite real is one, which is how pi and e get
+            // in: both are Variable here, and neither is the approach variable.
+            if (expr.Evaled is Real { EDecimal.IsFinite: true })
+                return true;
+            return expr switch
+            {
+                Variable v => v == x,
+                Sumf(var a, var b) => IsRealAlong(a, x) && IsRealAlong(b, x),
+                Minusf(var a, var b) => IsRealAlong(a, x) && IsRealAlong(b, x),
+                Mulf(var a, var b) => IsRealAlong(a, x) && IsRealAlong(b, x),
+                Divf(var a, var b) => IsRealAlong(a, x) && IsRealAlong(b, x),
+                Absf => true,
+                Powf(var b, Integer) => IsRealAlong(b, x),
+                Powf(var b, var e) => IsRealAlong(e, x) && b.Evaled is Real { IsPositive: true },
+                _ => false
+            };
+        }
+
         /// <summary>
         /// How many times over <see cref="ApplySecondRemarkable"/> may be re-read into an
         /// expression that <see cref="SimplifyAndComputeLimitToInfinity"/>'s simplification

Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Power.cs

@@ -180,8 +180,11 @@ expr is Powf(var @base, Integer { IsNegative: true } pow)
             // written -- including a symbolic exponent under the default complex reading, where
             // the question is not decidable.
             // https://github.com/asc-community/AngouriMath/issues/902
+            // Or the limit machinery is reading the expression towards a destination and has
+            // established the base holds a positive sign on the way to it, which is the same
+            // second way in that the logarithm gathering below takes.
             Logf(var any1, Powf(var any2, var any3))
-                when IsPositiveReal(any2) && MayBeTakenAsReal(any3) => any3 * MathS.Log(any1, any2),
+                when MayTakeLogOfPower(any2, any3) => any3 * MathS.Log(any1, any2),
             // log_b(b) is 1 wherever it is defined at all, so the condition to carry is the
             // node's own and not one written out here. Asserting `any1 > 0` stated the real
             // reading inside the rule and was wrong in both directions at once: undefined at
@@ -323,6 +326,16 @@ internal static Entity GatherPowersOfOneBase(Entity x)
         private static bool IsPositiveReal(Entity entity)
             => entity.Evaled is Real { EDecimal.IsFinite: true } value && value.IsPositive;
 
+        /// <summary>
+        /// Whether the exponent may be pulled out of a logarithm: because the base is a decidably
+        /// positive number and the exponent may be taken as real, or because a limit is being read
+        /// and the base holds a positive sign on the approach to its destination while the exponent
+        /// is real along it.
+        /// </summary>
+        private static bool MayTakeLogOfPower(Entity @base, Entity exponent)
+            => (IsPositiveReal(@base) && MayBeTakenAsReal(exponent))
+               || Algebra.LimitFunctional.MayTakeLogOfPowerHere(@base, exponent);
+
         /// <summary>
         /// Whether two antilogarithms may be gathered into one: because both are decidably
         /// positive numbers, or because a limit is being read and they hold their sign on the

Sources/Tests/UnitTests/Calculus/GruntzMovingExponentTest.cs

@@ -42,6 +42,7 @@ private static void AssertLimit(string expression, string expected) =>
         [InlineData("x ^ x / e ^ (x * ln(x))", "1")]
         [InlineData("e ^ (x * ln(x)) / x ^ x", "1")]
         [InlineData("x ^ (2 * x) / e ^ (2 * x * ln(x))", "1")]
+        [InlineData("(x ^ 2) ^ x / e ^ (2 * x * ln(x))", "1")]
         public void APowerAndItsExponentialAreOneFunction(string expression, string expected) =>
             AssertLimit(expression, expected);
 
@@ -53,40 +54,33 @@ public void APowerAndItsExponentialAreOneFunction(string expression, string expe
         [Theory]
         [InlineData("x ^ x / e ^ (x * ln(x) - x)", "+oo")]
         [InlineData("x ^ x / e ^ (x * ln(x) + x)", "0")]
+        [InlineData("x ^ x / e ^ (x * ln(x) - ln(x))", "+oo")]
         public void WhatIsLeftOverDecidesIt(string expression, string expected) =>
             AssertLimit(expression, expected);
 
         /// <summary>
-        /// Two of the cases above are no longer answered, and they are lost honestly: each comes
-        /// back as an unevaluated <c>limit</c> node rather than as a value, so the caller is told
-        /// that nothing was settled instead of being told something false.
+        /// The two rows above that need <c>ln(a^c) = c * ln(a)</c> are answered only because a
+        /// limit is being read. The identity is false off <c>ln</c>'s principal strip
+        /// (https://github.com/asc-community/AngouriMath/issues/902), so a bare <c>Simplify</c>
+        /// must still decline it: there is no destination there, and nothing says the base keeps
+        /// its sign.
         /// </summary>
         /// <remarks>
-        /// Both need <c>ln(a^c) = c * ln(a)</c> — <c>d/dx (x^2)^x</c> carries <c>ln(x^2)</c>, and
-        /// l'Hopital's rule reached it through <c>Simplify</c>. That identity is false off
-        /// <c>ln</c>'s principal strip, so the simplifier no longer applies it
-        /// (https://github.com/asc-community/AngouriMath/issues/902), and as x -> +oo the base
-        /// really is positive, so what is missing here is a way to say so.
-        /// <para/>
-        /// Supplying it from the limit side does not reach: rewriting the expression before
-        /// <c>Simplify</c> is called does pull the exponent out, and <c>Simplify</c>'s own
-        /// candidate search then writes <c>(x^2)^x</c> back into a logarithm and needs the
-        /// identity again. It is load-bearing *inside* the search, so restoring these two wants
-        /// an assumption travelling with the expression rather than another pre-pass.
-        /// <para/>
-        /// An unevaluated node is asserted rather than <c>NaN</c> deliberately: <c>NaN</c> would
-        /// claim the limit does not exist, and it does. If a value comes back here, the
-        /// assumption mechanism has arrived and these two rows belong back in the theories above.
+        /// This is the half of the pair that can regress silently. Widening the guard until an
+        /// ordinary <c>Simplify</c> applies the identity would restore the wrong answer #902
+        /// reported -- <c>ln(e^x)</c> as <c>x</c>, which at <c>x = 3*pi*i</c> is <c>9.4247i</c>
+        /// where the expression is <c>pi*i</c> -- and every limit above would keep passing.
         /// </remarks>
         [Theory]
-        [InlineData("(x ^ 2) ^ x / e ^ (2 * x * ln(x))")]
-        [InlineData("x ^ x / e ^ (x * ln(x) - ln(x))")]
-        public void AnExponentUnderALogarithmIsNotReadForNow(string expression)
+        [InlineData("ln(e ^ x)")]
+        [InlineData("log(2, 2 ^ x)")]
+        public void OutsideALimitTheExponentStaysUnderTheLogarithm(string expression)
         {
-            var limit = expression.ToEntity().Limit("x", "+oo".ToEntity());
-            Assert.True(limit is Entity.Limitf,
-                $"{expression} came back as {limit.Stringize()}, which is a value rather than an "
-                + "unevaluated limit -- see this test's remarks before changing it");
+            var simplified = expression.ToEntity().Simplify();
+            Assert.True(simplified is Entity.Logf,
+                $"{expression} simplified to {simplified.Stringize()}, pulling the exponent out "
+                + "of a logarithm with nothing to say the base holds its sign -- see this test's "
+                + "remarks before changing it");
         }
 
         /// <summary>