Stop pulling an exponent out of a logarithm over an undecided argument (#902)

BREAKING-CHANGES.md

@@ -68,6 +68,8 @@ read first.
 | loud | a known gap, e.g. a cubic inequality | `AngouriBugException`, asking to be reported | `NotSufficientlySupportedException` |
 | **silent** | `arcsin(sin(x))` and three siblings | `x`, wrong wherever `x` leaves the principal interval | left as written unless `x` is a real in that interval |
 | **silent** | `abs(sgn(x))` and `sgn(abs(x))` | `1`, wrong at `x = 0` where both are `0` | left as written unless the argument's value can be read |
+| **silent** | `ln(e^x)`, `log(2, 2^x)`, `ln(x^2)` | `x`, `x`, `2 * ln(x)` — wrong off the real line | left as written unless the argument is decidable |
+| **silent** | two limits over `(x^2)^x` and `x^x` | answered correctly | unevaluated — a deliberate loss |
 | **silent** | `arctan(x) + arccotan(x)` | `pi/2`, wrong for every negative `x` | `pi/2` or `-pi/2` where the sign is known, else left as written |
 | **silent** | `log(1, 1)` | `0` | `NaN`, since it is `0/0` |
 | **silent** | `log(b, 1)` | `0` for any base | `0 provided not b = 1` |
@@ -350,6 +352,57 @@ Found by `boundcheck`, a harness that composes every unary function node with ev
 compares against the original at points where an assumption fails rather than at sampled points.
 Issue [#887](https://github.com/asc-community/AngouriMath/issues/887).
 
+### An exponent is no longer pulled out of a logarithm over an undecided argument
+
+`log_b(a^c) = c * log_b(a)` holds where `c * ln(a)` stays inside the strip `Im in (-pi, pi]` that `ln`
+maps onto. It was applied to any argument at all, and the rewritten form is shorter, so it is what an
+ordinary caller got:
+
+| | was | is |
+|---|---|---|
+| `ln(e^x)` | `x` | left as written |
+| `log(2, 2^x)` | `x` | left as written |
+| `ln(x^2)` | `2 * ln(x)` | left as written |
+| `ln(e^3)`, `log(2, 2^5)` | `3`, `5` | unchanged |
+| `ln(e^x)` under `Codomain.Set(Domain.Real)` | `x` | `x`, unchanged |
+
+`ln(e^x) -> x` is wrong wherever `Im x` leaves that strip. At `x = 3*pi*i` the expression is `pi*i`,
+because `e^(3*pi*i)` is `-1`, while `x` is `9.4247...i` — the two differ by exactly the full turn the
+principal branch discards. `MathS.Settings.Codomain` defaults to `Domain.Complex`, so this was unsound
+on the library's own default reading. It is also unsound for a negative real base: `log(2, 64)` is `6`
+where `2 * log(2, -8)` is `6 + 9.0647...i`.
+
+The rule now asks for a base that is decidably a positive real, and an exponent that may be taken as
+real — because the reading is real analysis, because the node's declared codomain says so, or because
+its value is a real. A symbolic exponent under the default complex reading is none of those, so the
+expression is left as written: decide, or decline, as with the four inverse-trigonometric rules above.
+
+**Two limits are lost, and that is the cost of this entry rather than an oversight.**
+
+| | was | is |
+|---|---|---|
+| `lim x->+oo (x^2)^x / e^(2*x*ln(x))` | `1` | unevaluated |
+| `lim x->+oo x^x / e^(x*ln(x) - ln(x))` | `+oo` | unevaluated |
+
+Both are right answers becoming no answer, which this file has recorded before for two integrals, and
+which the ordering in [AGENTS.md](AGENTS.md) prefers to a wrong answer reachable from `ln(e^x)`. They
+are unevaluated rather than `NaN`: the caller is told nothing was settled, not that the limit does not
+exist.
+
+They want the identity that was just removed. `d/dx (x^2)^x` carries `ln(x^2)`, and l'Hopital's rule
+reached it through `Simplify`. On the way to `+oo` the base genuinely is positive, so the identity is
+true there — the limit machinery simply has no way to say so to the simplifier. Supplying it from the
+limit side was tried and does not reach: rewriting the expression before `Simplify` is called does pull
+the exponent out, and `Simplify`'s own candidate search then writes `(x^2)^x` back into a logarithm and
+needs the identity again. It is load-bearing *inside* the search, so what would restore these two is 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. The two rows
+have their own test asserting the unevaluated node, so a future fix flips them back deliberately.
+
+`boundcheck` drops from four disagreements to two; the remaining two are `log(x, x)` and
+`ln(x) + ln(x+1)`, both recorded elsewhere as wanting a decision rather than a guard. Issue
+[#902](https://github.com/asc-community/AngouriMath/issues/902).
+
 ### `abs(sgn(x))` and `sgn(abs(x))` are not `1` at zero
 
 `|sgn(z)|` and `sgn(|z|)` are `1` for every `z` except `0`, where both are `0`, because `sgn(0)` is

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

@@ -155,7 +155,16 @@ expr is Sumf(var any1, Mulf(Real { IsNegative: true } const1, var any2))
             // x * {} ^ {} = {} ^ {} * x
             Mulf(Variable var1, Powf(var any1, var any2)) => new Powf(any1, any2) * var1,
 
-            Logf(var any1, Powf(var any2, var any3)) => any3 * MathS.Log(any1, any2),
+            // log_b(a^c) = c * log_b(a) holds where c * ln(a) stays inside the strip
+            // Im in (-pi, pi] that ln maps onto, and not in general: ln(e^(3*pi*i)) is pi*i
+            // while 3*pi*i is not, the two differing by exactly the 2*pi*i the principal branch
+            // discards. A base that is a positive real makes ln(a) real, and a real exponent then
+            // keeps the product real, so there is nothing to discard. Anything else is left as
+            // written -- including a symbolic exponent under the default complex reading, where
+            // the question is not decidable.
+            // https://github.com/asc-community/AngouriMath/issues/902
+            Logf(var any1, Powf(var any2, var any3))
+                when IsPositiveReal(any2) && MayBeTakenAsReal(any3) => any3 * MathS.Log(any1, any2),
             Logf(var any1, var any1a) when any1 == any1a => new Providedf(1, any1 > 0),
             Logf(Divf(Integer(1), var any1), Divf(Integer(1), var any2)) => MathS.Log(any1, any2),
             Logf(var any1, Divf(Integer(1), var any2)) => -MathS.Log(any1, any2),
@@ -263,6 +272,33 @@ internal static Entity GatherPowersOfOneBase(Entity x)
         /// <c>a</c> -- the same guard the <c>({}^{})^{}</c> rule above carries, and for the
         /// same reason. https://github.com/asc-community/AngouriMath/issues/752
         /// </remarks>
+        /// <summary>
+        /// Whether <paramref name="entity"/> is a real strictly above zero, decided rather than
+        /// assumed. <c>ln</c> of such a number is a real, so a real multiple of it stays on the
+        /// real line and inside <c>ln</c>'s principal strip.
+        /// </summary>
+        /// <remarks>
+        /// Finiteness is checked separately because <see cref="Real.IsPositive"/> is
+        /// <c>!IsNegative &amp;&amp; !IsZero</c>, which <c>NaN</c> and <c>+oo</c> both satisfy.
+        /// </remarks>
+        private static bool IsPositiveReal(Entity entity)
+            => entity.Evaled is Real { EDecimal.IsFinite: true } value && value.IsPositive;
+
+        /// <summary>
+        /// Whether this operand may be taken as real: because the expression is being read as a
+        /// real-valued one, because the node's own declared codomain says so, or because its value
+        /// is a real to begin with.
+        /// </summary>
+        /// <remarks>
+        /// The first two are the disjunction <c>Patterns.EqualityInequality.cs</c> uses to ask the
+        /// same question. A bare <see cref="Variable"/> is <c>Domain.Any</c>, so a symbol under the
+        /// default complex reading answers <see langword="false"/> here -- which is the point.
+        /// </remarks>
+        private static bool MayBeTakenAsReal(Entity entity)
+            => MathS.Settings.Codomain.Value is AngouriMath.Core.Domain.Real
+               || IsKnownReal(entity)
+               || entity.Evaled is Real { EDecimal.IsFinite: true };
+
         private static (Entity Base, Entity Exponent) Decompose(Entity factor)
         {
             if (factor is not Powf(var @base, var exponent))

Sources/Tests/UnitTests/Calculus/GruntzMovingExponentTest.cs

@@ -42,7 +42,6 @@ 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,11 +52,43 @@ public void APowerAndItsExponentialAreOneFunction(string expression, string expe
         /// </summary>
         [Theory]
         [InlineData("x ^ x / e ^ (x * ln(x) - x)", "+oo")]
-        [InlineData("x ^ x / e ^ (x * ln(x) - ln(x))", "+oo")]
         [InlineData("x ^ x / e ^ (x * ln(x) + x)", "0")]
         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.
+        /// </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.
+        /// </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)
+        {
+            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");
+        }
+
         /// <summary>
         /// The claim the expected values above rest on, checked at a point rather than argued:
         /// the ratio is not merely close to 1, it is 1.

Sources/Tests/UnitTests/Common/SimplificationRegressionTest.cs

@@ -585,6 +585,46 @@ public void ComposingAFunctionOverItsOwnInverseIsStillTheIdentity(string input)
         static double Magnitude(Entity difference) =>
             ((System.Numerics.Complex)difference.EvalNumerical()).Magnitude;
 
+        // https://github.com/asc-community/AngouriMath/issues/902
+        // log_b(a^c) = c * log_b(a) needs c * ln(a) to stay inside the strip Im in (-pi, pi] that
+        // ln maps onto, and it was applied to anything at all. ln(e^x) came back as x, which at
+        // x = 3*pi*i is 9.42i where the expression is pi*i -- e^(3*pi*i) being -1. The rewrite
+        // wins on complexity, so it is what an ordinary caller gets.
+        [Theory]
+        [InlineData("ln(e^x)")]
+        [InlineData("log(2, 2^x)")]
+        [InlineData("ln(x^2)")]
+        [InlineData("log(2, x^2)")]
+        public void AnExponentIsNotPulledOutOfALogarithmOverAnUndecidedArgument(string expression) =>
+            Assert.Equal(expression.ToEntity(), expression.ToEntity().Simplify());
+
+        // The value is the point, so it is the value that is checked: at 3*pi*i the two forms
+        // differ by the full turn the principal branch discards.
+        [Fact]
+        public void TheLogarithmOfAPowerKeepsItsValueOffTheRealLine()
+        {
+            var original = "ln(e^x)".ToEntity();
+            var at = "3 * pi * i".ToEntity();
+            Assert.Equal(original.Substitute("x", at).EvalNumerical(),
+                original.Simplify().Substitute("x", at).EvalNumerical());
+        }
+
+        // Where both sides are decidable it still fires, and a real reading is enough to decide
+        // it: under Domain.Real the exponent is real by the reading itself.
+        [Theory]
+        [InlineData("ln(e^3)", "3")]
+        [InlineData("log(2, 2^5)", "5")]
+        [InlineData("ln(e^(1/2))", "1/2")]
+        public void AnExponentIsPulledOutWhereTheArgumentIsDecidable(string expression, string expected) =>
+            Assert.Equal(expected.ToEntity().Simplify(), expression.ToEntity().Simplify());
+
+        [Fact]
+        public void ARealReadingDecidesTheExponent()
+        {
+            using var _ = MathS.Settings.Codomain.Set(AngouriMath.Core.Domain.Real);
+            Assert.Equal("x".ToEntity(), "ln(e^x)".ToEntity().Simplify());
+        }
+
         // https://github.com/asc-community/AngouriMath/issues/890
         // log_b(1) is ln(1)/ln(b), which is 0/ln(b) -- so 0 for every base except 1, where it
         // is 0/0. The rewrite answered 0 for any base at all, so log(1, 1) was 0 where every