Answer a family under the condition it carries

BREAKING-CHANGES.md

@@ -403,7 +403,8 @@ system is now eliminated one unknown at a time, and an unknown that nothing is l
 zero. Where one does not, or where a branch cannot be decided, the system is declined as `null`, which `Solve`
 documents as no solution found ([#212](https://github.com/asc-community/AngouriMath/issues/212)). A family with an
 `n_1` from a periodic root, which stands for every whole number, is kept where it is zero for each, as
-`forall n_1 in ZZ` decides it. Code that caught the exception around `Solve` to detect a non-square system no longer
+`forall n_1 in ZZ` decides it, and a family that says where it holds, as a root's inverse does, is kept where it is
+zero wherever that holds. Code that caught the exception around `Solve` to detect a non-square system no longer
 sees it.
 
 | Input | Was (2.6.0) | Now |
@@ -413,7 +414,7 @@ sees it.
 | `MathS.Equations("sin(x)", "x").Solve("x")` | `WrongNumberOfArgumentsException` | `[0]` |
 | `MathS.Equations("sin(x) - 1/2").Solve("x", "y")` | `WrongNumberOfArgumentsException` | `[[pi / 6 + 2 * pi * n_1, t_1], [pi - pi / 6 + 2 * pi * n_1, t_1]]` |
 | `MathS.Equations("sin(x) - y", "cos(x) - y", "x - pi/4").Solve("x", "y")` | `WrongNumberOfArgumentsException` | `[[pi / 4, 1/2 * sqrt(2)]]` |
-| `MathS.Equations("sqrt(y) - x").Solve("x", "y")` | `WrongNumberOfArgumentsException` | `null`: `y = x^2` is no solution where `x` is negative |
+| `MathS.Equations("sqrt(y) - x").Solve("x", "y")` | `WrongNumberOfArgumentsException` | `[[t_1, t_1 ^ 2 provided t_1 = 0 or -1/2 * pi < arg(t_1) and arg(t_1) <= 1/2 * pi]]`: `y = x^2` is a solution only where `sqrt` takes `x` as a value |
 | `MathS.Equations("x + y - a", "x - y - b", "x - c").Solve("x", "y")` | `WrongNumberOfArgumentsException` | `null`: there are solutions only where `a + b = 2c` |
 
 ### A whole number of periods comes out of a trigonometric function under a quantifier
@@ -429,6 +430,18 @@ or of `pi` for a tangent or a cotangent, the term is taken out, as `Complex.sin_
 | `"forall n in ZZ : sin(x + 2 pi n) = sin(x)".ToEntity().Simplify()` | `forall n in ZZ : sin(2 * n * pi + x) = sin(x)` | `True` |
 | `"forall n in ZZ : tan(pi/4 + pi n) = 1".ToEntity().Simplify()` | `forall n in ZZ : tan(pi * (1/4 + n)) = 1` | `True` |
 
+### A principal root of a power is read with what the quantifiers establish
+
+**Silent: a quantified statement about `(t^n)^(1/n)` is decided where it was left as written.** Where the quantifiers
+around a principal `n`-th root of an `n`-th power, for a whole `n >= 2`, establish that `t` is `0` or in the sector
+`-pi/n < arg(t) <= pi/n` where that root takes its values, or that `t >= 0`, the root is `t`, as
+`Complex.pow_cpow_nat_inv` has it. Nothing changes outside a quantifier, and `sqrt(t^2)` is not `t`
+([#212](https://github.com/asc-community/AngouriMath/issues/212)).
+
+| Input | Was (2.6.0) | Now |
+|---|---|---|
+| `"forall t in RR : t >= 0 implies sqrt(t^2) = t".ToEntity().Simplify()` | `forall t in RR : t >= 0 implies sqrt(t ^ 2) = t` | `True` |
+
 ### A system is not answered with a copy of one of its rows
 
 **Silent: a repeated row goes.** Two branches of an elimination can reach one solution, and each was answered: two

Sources/.editorconfig

@@ -405,6 +405,9 @@ file_header_template=\nCopyright (c) 2019-2026 Angouri.\nAngouriMath is licensed
 [Tests/UnitTests/Core/PeriodByFactsTest.cs]
 file_header_template=\nCopyright (c) 2019-2026 Angouri.\nAngouriMath is licensed under MIT.\nDetails: https://github.com/asc-community/AngouriMath/blob/master/LICENSE.md.\nWebsite: https://am.angouri.org.\n
 
+[Tests/UnitTests/Core/RootByFactsTest.cs]
+file_header_template=\nCopyright (c) 2019-2026 Angouri.\nAngouriMath is licensed under MIT.\nDetails: https://github.com/asc-community/AngouriMath/blob/master/LICENSE.md.\nWebsite: https://am.angouri.org.\n
+
 [AngouriMath/Core/Entity/Continuous/Number/ErrorFunctions.cs]
 file_header_template=\nCopyright (c) 2019-2026 Angouri.\nAngouriMath is licensed under MIT.\nDetails: https://github.com/asc-community/AngouriMath/blob/master/LICENSE.md.\nWebsite: https://am.angouri.org.\n
 

Sources/AngouriMath/Functions/Boolean/QuantifierFacts.cs

@@ -242,6 +242,8 @@ internal static Entity Renamed(Entity expression, Variable from, Variable to)
             Dividesf(not Number, _) or Congruentf(_, _, not Number) => true,
             Equalsf(Modf(_, var modulus), Modf(_, var other)) => modulus is not Number && modulus == other,
             Floorf(not Number) or Ceilf(not Number) => true,
+            // A principal root of a whole power, which PrincipalPowerOfAPower reads.
+            Powf(Powf(not Number, Integer), Rational) => true,
             _ => false
         };
 
@@ -487,6 +489,61 @@ internal static bool PrimeDividesByTheBinomialTheorem(Entity p, Entity d)
             return Recorded(function(argument), function(rest), $"{periods} is a whole number of periods", lemma);
         }
 
+        /// <summary>
+        /// <c>z</c> for the principal root <c>(z^n)^(1/n)</c> of a whole <c>n &gt;= 2</c>, where the facts in
+        /// scope put <c>z</c> where that root takes its values, or <see langword="null"/>: at <c>0</c> or in
+        /// the sector <c>-pi/n &lt; arg(z) &lt;= pi/n</c>, which is how the power's inversion states it, or on
+        /// the half-line <c>z &gt;= 0</c>, as <c>Complex.pow_cpow_nat_inv</c> has it. So <c>sqrt(t^2)</c> is
+        /// <c>t</c> where <c>t = 0 or -pi/2 &lt; arg(t) &lt;= pi/2</c>.
+        /// https://github.com/asc-community/AngouriMath/issues/212
+        /// </summary>
+        internal static Entity? PrincipalPowerOfAPower(Entity z, Entity inner, Entity exponent)
+        {
+            if (top is null || !MentionsARenamedName(z)
+                || inner is not Integer { EInteger: var n } || n.CompareTo(2) < 0
+                || exponent is not Rational { ERational: var p } || p.CompareTo(ERational.Create(EInteger.One, n)) != 0)
+                return null;
+            foreach (var fact in InScope())
+                if (IsOnTheHalfLine(fact, z) || IsInTheSector(fact, z, exponent))
+                    return Recorded(MathS.Pow(MathS.Pow(z, inner), exponent), z,
+                        $"{z} is where the principal {inner}-th root takes its values", "Complex.pow_cpow_nat_inv");
+            return null;
+
+            static bool IsOnTheHalfLine(Entity fact, Entity z)
+                => fact switch
+                {
+                    GreaterOrEqualf(var left, Integer { IsZero: true }) => left == z,
+                    Greaterf(var left, Integer { IsZero: true }) => left == z,
+                    LessOrEqualf(Integer { IsZero: true }, var right) => right == z,
+                    Lessf(Integer { IsZero: true }, var right) => right == z,
+                    _ => false
+                };
+
+            // z = 0 or (-p pi < arg(z) and arg(z) <= p pi), the two sides of each in either order.
+            static bool IsInTheSector(Entity fact, Entity z, Entity p)
+            {
+                if (fact is not Orf(var either, var other))
+                    return false;
+                var (zero, sector) = IsZero(either, z) ? (either, other) : (other, either);
+                if (!IsZero(zero, z) || sector is not Andf(var first, var second))
+                    return false;
+                var bound = p * MathS.pi;
+                return Below(first, -bound) && Above(second, bound) || Below(second, -bound) && Above(first, bound);
+
+                bool Below(Entity side, Entity lower)
+                    => side is Lessf(var low, Argf(var of)) && of == z && Same(low, lower)
+                       || side is Greaterf(Argf(var on), var low2) && on == z && Same(low2, lower);
+                bool Above(Entity side, Entity upper)
+                    => side is LessOrEqualf(Argf(var of), var high) && of == z && Same(high, upper)
+                       || side is GreaterOrEqualf(var high2, Argf(var on)) && on == z && Same(high2, upper);
+            }
+            static bool IsZero(Entity statement, Entity z)
+                => statement is Equalsf(var left, var right) && (left == z && right == 0 || right == z && left == 0);
+            // The bounds are multiples of pi, so they are compared by value.
+            static bool Same(Entity a, Entity b)
+                => !a.Vars.Any() && (a - b).Evaled is Complex difference && ((Real)difference.Abs()).EDecimal.ToDouble() < 1e-12;
+        }
+
         /// <summary>A function <see cref="WithoutWholePeriods"/> takes whole periods out of, of anything but a number.</summary>
         private static bool IsPeriodic(Entity node)
             => node is Sinf(not Number) or Cosf(not Number) or Tanf(not Number) or Cotanf(not Number) or Secantf(not Number) or Cosecantf(not Number);

Sources/AngouriMath/Functions/Continuous/Solvers/EquationSolver/NonSquareSystemSolver.cs

@@ -25,10 +25,11 @@ namespace AngouriMath.Functions.Algebra.AnalyticalSolving
     /// <remarks>
     /// <para>
     /// <b>An answer is given only where it is shown to hold.</b> The elimination trusts each solve
-    /// it makes, and a solve can answer for a case its equation does not cover: <c>sqrt(y) = x</c>
-    /// is solved for <c>y</c> as <c>x^2</c>, which is no solution where <c>x</c> is negative. So
-    /// each family is kept only where every equation, with the family substituted, simplifies to
-    /// <c>0</c>. <c>sqrt(t^2) - t</c> does not, and that system is declined.
+    /// it makes, and a solve can answer for a case its equation does not cover. So each family is
+    /// kept only where every equation, with the family substituted, simplifies to <c>0</c>. A family
+    /// that says where it holds is checked there: <c>sqrt(y) = x</c> is solved for <c>y</c> as
+    /// <c>x^2</c> provided <c>x</c> is where <c>sqrt</c> takes its values, and <c>sqrt(t^2) - t</c>
+    /// is zero wherever that holds.
     /// </para>
     /// <para>
     /// <b>A decline declines the whole system.</b> An equation left with no unknown in it is zero,
@@ -68,16 +69,22 @@ Variable ParameterFor(int index)
                 return null;
             var own = new HashSet<Variable>(equations.SelectMany(equation => equation.Vars));
             foreach (var family in families)
+            {
+                // A family that says where it holds, as y = t^2 provided t is where sqrt takes its
+                // values, is checked there and nowhere else.
+                var condition = family.OfType<Providedf>().Select(entry => entry.Predicate).Aggregate((Entity?)null, (all, one) => all is null ? one : all & one);
+                var bare = family.Select(entry => entry is Providedf(var value, _) ? value : entry).ToList();
                 foreach (var equation in equations)
                 {
                     var substituted = equation;
                     for (var index = 0; index < variables.Length; index++)
-                        substituted = substituted.Substitute(variables[index], family[index]);
+                        substituted = substituted.Substitute(variables[index], (condition is null ? family : bare)[index]);
                     // An n_1 a family brings from a periodic root stands for every whole number.
                     var whole = substituted.Vars.Where(name => !own.Contains(name) && name.Name.StartsWith("n_")).Distinct().ToList();
-                    if (!Vanishes(substituted, whole))
+                    if (!Vanishes(substituted, whole) && (condition is null || !VanishesWhere(substituted, condition, whole)))
                         return null;
                 }
+            }
             return families;
         }
 
@@ -235,6 +242,22 @@ private static bool Vanishes(Entity expression, IReadOnlyList<Variable> whole)
             };
         }
 
+        /// <summary>
+        /// Whether <paramref name="expression"/> is zero wherever <paramref name="condition"/> holds,
+        /// decided as a statement for every value of its symbols, a whole one for a symbol in
+        /// <paramref name="whole"/>: <c>sqrt(t^2) - t</c> is zero where
+        /// <c>t = 0 or -pi/2 &lt; arg(t) &lt;= pi/2</c>, which is
+        /// <c>forall t in CC : (t = 0 or -pi/2 &lt; arg(t) &lt;= pi/2) implies sqrt(t^2) - t = 0</c>.
+        /// https://github.com/asc-community/AngouriMath/issues/212
+        /// </summary>
+        private static bool VanishesWhere(Entity expression, Entity condition, IReadOnlyList<Variable> whole)
+        {
+            Entity statement = new Impliesf(condition, expression.EqualTo(Integer.Zero));
+            foreach (var name in statement.Vars.Distinct().ToList())
+                statement = MathS.ForAll(name, whole.Contains(name) ? MathS.Sets.Z : MathS.Sets.C, statement);
+            return statement.Simplify() == Entity.Boolean.True;
+        }
+
         /// <summary>
         /// <paramref name="expression"/> with each of its symbols at a fixed value, a whole one for
         /// a symbol in <paramref name="whole"/>.

Sources/AngouriMath/Functions/Evaluation/Evaluation.Continuous/Evaluation.Continuous.Arithmetics.Classes.cs

@@ -407,6 +407,7 @@ x.Evaled is Complex c
                     // https://github.com/asc-community/AngouriMath/issues/281
                     (Rational radicand, Rational exponent) when
                         RootExtraction.PullOutOfRadical(radicand, exponent) is { } pulled => pulled.InnerSimplified(isExact),
+                    (Powf(var z, var inner), var exponent) when Functions.Boolean.QuantifierFacts.PrincipalPowerOfAPower(z, inner, exponent) is { } root => root,
                     _ => null
                 },
                 (@this, a, b) => ((Powf)@this).New(a, b), isExact);

Sources/Tests/UnitTests/Algebra/SolveTest/NonSquareSystemTest.cs

@@ -116,14 +116,36 @@ public void AnOverdeterminedSystemIsSolved(string[] equations, string[] variable
         }
 
         /// <summary>
-        /// What the elimination finds and cannot show to hold. <c>sqrt(y) = x</c> is solved for
-        /// <c>y</c> as <c>x^2</c>, no solution where <c>x</c> is negative. The coefficient of
-        /// <c>y</c> in the second is zero without being written so, and dividing by it gives a
-        /// family that <c>Simplify</c> calls zero provided it is not zero. The third has solutions
-        /// only where <c>a + b = 2c</c>.
+        /// A family that says where it holds is checked there. <c>sqrt(y) = x</c> is solved for
+        /// <c>y</c> as <c>x^2</c> where <c>x</c> is <c>0</c> or in the half-plane <c>sqrt</c> takes
+        /// its values in, so the family is <c>(t_1, t_1^2)</c> under that condition. It holds at
+        /// each <c>t_1</c> in the sector, <c>i/2</c> on its edge among them, and is not claimed
+        /// at a negative one, where <c>sqrt(t_1^2)</c> is <c>-t_1</c>.
+        /// </summary>
+        [Fact]
+        public void AFamilyThatSaysWhereItHoldsIsCheckedThere()
+        {
+            var solutions = Solve(new[] { "sqrt(y) - x" }, new[] { "x", "y" });
+            Assert.NotNull(solutions);
+            Assert.Equal(1, solutions!.RowCount);
+            var y = Assert.IsType<Entity.Providedf>(solutions[0, 1]);
+            var t = Assert.IsType<Entity.Variable>(solutions[0, 0]);
+            foreach (var at in new Entity[] { 2, "1.3 + 0.7i", "i/2", 0 })
+            {
+                Assert.Equal(Entity.Boolean.True, y.Predicate.Substitute(t, at).Evaled);
+                var residual = ("sqrt(y) - x".ToEntity().Substitute("y", y.Expression).Substitute("x", t)).Substitute(t, at);
+                Assert.True(((Entity.Number.Real)((Entity.Number.Complex)residual.Evaled).Abs()).EDecimal.ToDouble() < 1e-12, $"{residual}");
+            }
+            Assert.Equal(Entity.Boolean.False, y.Predicate.Substitute(t, -2).Evaled);
+        }
+
+        /// <summary>
+        /// What the elimination finds and cannot show to hold. The coefficient of <c>y</c> in the
+        /// first is zero without being written so, and dividing by it gives a family that
+        /// <c>Simplify</c> calls zero provided it is not zero. The second has solutions only where
+        /// <c>a + b = 2c</c>.
         /// </summary>
         [Theory]
-        [InlineData(new[] { "sqrt(y) - x" }, new[] { "x", "y" })]
         [InlineData(new[] { "x^2 - ((a + 1)^2 - a^2 - 2*a - 1)*y" }, new[] { "x", "y" })]
         [InlineData(new[] { "x + y - a", "x - y - b", "x - c" }, new[] { "x", "y" })]
         public void WhatCannotBeShownToHoldIsDeclined(string[] equations, string[] variables)

Sources/Tests/UnitTests/Core/RootByFactsTest.cs

@@ -0,0 +1,46 @@
+//
+// Copyright (c) 2019-2026 Angouri.
+// AngouriMath is licensed under MIT.
+// Details: https://github.com/asc-community/AngouriMath/blob/master/LICENSE.md.
+// Website: https://am.angouri.org.
+//
+
+using AngouriMath;
+using AngouriMath.Extensions;
+using Xunit;
+using static AngouriMath.Entity;
+
+namespace AngouriMath.Tests.Core
+{
+    /// <summary>
+    /// The principal n-th root of an n-th power, read with what the quantifiers establish: <c>(z^n)^(1/n)</c>
+    /// is <c>z</c> where <c>z</c> is <c>0</c> or in the sector <c>-pi/n &lt; arg(z) &lt;= pi/n</c>, which is how
+    /// the power's inversion states where its solution holds, or where <c>z &gt;= 0</c>.
+    /// <see href="https://github.com/asc-community/AngouriMath/issues/212"/>
+    /// </summary>
+    [Trait("Area", "Core")]
+    public sealed class RootByFactsTest
+    {
+        [Theory]
+        [InlineData("forall t in CC : (t = 0 or -1/2 * pi < arg(t) and arg(t) <= 1/2 * pi) implies sqrt(t^2) = t")]
+        [InlineData("forall t in CC : (arg(t) <= pi/2 and -pi/2 < arg(t) or t = 0) implies sqrt(t^2) = t")]
+        [InlineData("forall t in CC : (t = 0 or -1/3 * pi < arg(t) and arg(t) <= 1/3 * pi) implies (t^3)^(1/3) = t")]
+        [InlineData("forall t in RR : t >= 0 implies sqrt(t^2) = t")]
+        public void DecidedByWhatTheQuantifiersEstablish(string statement)
+            => Assert.Equal(Boolean.True, statement.ToEntity().Simplify());
+
+        [Theory]
+        // False at t = -1.
+        [InlineData("forall t in RR : sqrt(t^2) = t")]
+        // The sector of the square root is half of this: false at t = -1.
+        [InlineData("forall t in CC : (-pi < arg(t) and arg(t) <= pi) implies sqrt(t^2) = t")]
+        // The square root's sector, not the cube root's: false at t = i, where (i^3)^(1/3) is e^(-i pi/6).
+        [InlineData("forall t in CC : (t = 0 or -1/2 * pi < arg(t) and arg(t) <= 1/2 * pi) implies (t^3)^(1/3) = t")]
+        public void NotClaimedWhereTheFactsDoNotHold(string statement)
+            => Assert.NotEqual(Boolean.True, statement.ToEntity().Simplify());
+
+        [Fact]
+        public void OutsideAQuantifierNothingIsAssumed()
+            => Assert.NotEqual(MathS.Var("t"), "sqrt(t^2)".ToEntity().Simplify());
+    }
+}