From 69407da59ab114b4e181cc092970fc81dd7163e0 Mon Sep 17 00:00:00 2001 From: Rafael Vuijk Date: Fri, 30 Oct 2026 16:41:51 +0000 Subject: [PATCH] The factorial and the gamma function are defined off the real line The factorial's condition was x in RR and (x >= 0 or not x in ZZ), which asked for a real argument as well, though i! is 0.498 - 0.155i and the only poles are the negative integers. x!/x! simplified to 1 provided x in RR and (...), which has no value at x = i, where it is 1. The condition is now x in ZZ implies x >= 0: off the integers x in ZZ is false and the implication is true. It is written as Simplify writes it, so that a quotient's not x! = 0, which Simplify reads as True under this condition, folds into it. As not (x in ZZ and x < 0) the answer carried both. ExponentialSeries.HoldsOverTheRange read the old shape to drop a factorial's condition over a summation range, and integral(floor(x) / (floor(x) + 1)!, x, 0, +oo) stopped being 1. An implication now holds over the range wherever its conclusion does. FactorialOffTheRealLineTest takes the condition at eleven points, off the real line, at poles and between them, and two simplified quotients at complex points; six fail on master. SimplifyTest's three x!/x!-shaped tests pinned the old condition, and now have the new one. Found by work/domaincheck. Part of #2256. Co-Authored-By: Claude Opus 5.5 (1M context) --- BREAKING-CHANGES.md | 13 +++++ Sources/.editorconfig | 3 ++ .../Algebra/Polynomials/ExponentialSeries.cs | 4 ++ ...aluation.Continuous.Arithmetics.Classes.cs | 12 +++-- .../Patterns/Patterns.EqualityInequality.cs | 2 +- .../FactorialOffTheRealLineTest.cs | 48 +++++++++++++++++++ .../UnitTests/PatternsTest/SimplifyTest.cs | 9 ++-- 7 files changed, 84 insertions(+), 7 deletions(-) create mode 100644 Sources/Tests/UnitTests/Convenience/FactorialOffTheRealLineTest.cs diff --git a/BREAKING-CHANGES.md b/BREAKING-CHANGES.md index 59064adbc..23461c32b 100644 --- a/BREAKING-CHANGES.md +++ b/BREAKING-CHANGES.md @@ -616,6 +616,19 @@ Both are real, `im(3 + 4i)` being `4`, real-linear, and turned by the conjugate | `"im(3 + 4i)".ToEntity().Simplify()` | `(3 + 4i) * im` | `4` | | `"re * x".ToEntity()` | `re * x` | `re * x` | +### The factorial and the gamma function are defined off the real line + +**Silent: the condition a simplified factorial carries is `x in ZZ implies x >= 0`, where it was `x in RR and (x >= 0 +or not x in ZZ)`.** A factorial, and the gamma function with it, has poles at the negative integers and nowhere else. +Its condition also asked for a real argument, though `i!` is `0.498 - 0.155i`. So `x!/x!` simplified to an answer with +no value at `i`, where it is 1 ([#2256](https://github.com/asc-community/AngouriMath/issues/2256)). + +| Input | Was (2.6.0) | Now | +|---|---|---| +| `"x!/x!".ToEntity().Simplify()` | `1 provided x in RR and (x >= 0 or not x in ZZ)` | `1 provided x in ZZ implies x >= 0` | +| `"x! = 0".ToEntity().Simplify()` | `False provided x in RR and (x >= 0 or not x in ZZ)` | `False provided x in ZZ implies x >= 0` | +| `"x!".ToEntity().DomainCondition` | `x in RR and (x >= 0 or not x in ZZ)` | `x in ZZ implies x >= 0` | + ### A number's conjugate is made under the setting in force **Silent: `Complex.Conjugate` is made under the downcasting setting of the caller, where the first caller's setting was diff --git a/Sources/.editorconfig b/Sources/.editorconfig index b677d246c..8b9e25e3d 100644 --- a/Sources/.editorconfig +++ b/Sources/.editorconfig @@ -240,6 +240,9 @@ file_header_template=\nCopyright (c) 2019-2026 Angouri.\nAngouriMath is licensed [Tests/UnitTests/Convenience/ConjugateAndArgumentTest.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/Convenience/FactorialOffTheRealLineTest.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/Algebra/SolveTest/FractionalPowerRangeTest.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 diff --git a/Sources/AngouriMath/Functions/Algebra/Polynomials/ExponentialSeries.cs b/Sources/AngouriMath/Functions/Algebra/Polynomials/ExponentialSeries.cs index 287da1421..bb36745d5 100644 --- a/Sources/AngouriMath/Functions/Algebra/Polynomials/ExponentialSeries.cs +++ b/Sources/AngouriMath/Functions/Algebra/Polynomials/ExponentialSeries.cs @@ -202,6 +202,10 @@ private static bool HoldsOverTheRange(Entity condition, Variable index, int star => HoldsOverTheRange(left, index, start) && HoldsOverTheRange(right, index, start), Orf(var left, var right) => HoldsOverTheRange(left, index, start) || HoldsOverTheRange(right, index, start), + // A factorial's own condition, index + a in ZZ implies index + a >= 0: true wherever + // its conclusion is. https://github.com/asc-community/AngouriMath/issues/2256 + Impliesf(_, var conclusion) + => HoldsOverTheRange(conclusion, index, start), _ => false, }; diff --git a/Sources/AngouriMath/Functions/Evaluation/Evaluation.Continuous/Evaluation.Continuous.Arithmetics.Classes.cs b/Sources/AngouriMath/Functions/Evaluation/Evaluation.Continuous/Evaluation.Continuous.Arithmetics.Classes.cs index f8a8bc6fd..2ee76bce1 100644 --- a/Sources/AngouriMath/Functions/Evaluation/Evaluation.Continuous/Evaluation.Continuous.Arithmetics.Classes.cs +++ b/Sources/AngouriMath/Functions/Evaluation/Evaluation.Continuous/Evaluation.Continuous.Arithmetics.Classes.cs @@ -524,9 +524,15 @@ public partial record Factorialf { // Factorial is defined for non-negative integers in the traditional sense, // but extends to complex numbers via the gamma function: n! = Γ(n+1) - // The gamma function has poles at negative integers, so factorial is undefined there - private protected override Entity IntrinsicCondition => - Argument.In(MathS.Sets.R) & (Argument >= 0 | !Argument.In(MathS.Sets.Z)); + // The gamma function has poles at negative integers, so factorial is undefined there, + // and only there. The condition asked for a real argument as well, though i! is + // 0.498 - 0.155i, so x!/x! simplified to 1 provided x in RR, which has no value at i. + // Off the integers x >= 0 may have no truth value and x in ZZ is false, so the implication + // is true. It is written as Simplify writes it, so that a quotient's x! = 0, which Simplify + // reads as False under this same condition, folds into it. + // https://github.com/asc-community/AngouriMath/issues/2256 + private protected override Entity IntrinsicCondition => + new Impliesf(Argument.In(MathS.Sets.Z), Argument >= 0); /// protected override Entity InnerSimplify(bool isExact) => diff --git a/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.EqualityInequality.cs b/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.EqualityInequality.cs index 98dcae852..79fd0c2ee 100644 --- a/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.EqualityInequality.cs +++ b/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.EqualityInequality.cs @@ -280,7 +280,7 @@ internal static Entity PushNotInside(IEnumerable operands, bool disjoin) // a! = 0 // A factorial is never zero *where it is defined*, and at a negative integer it is // not: `(-1)!` is a pole, so `(-1)! = 0` is NaN rather than False. The condition owed - // is therefore the factorial's own -- `x in RR and (x >= 0 or not x in ZZ)`. + // is therefore the factorial's own -- `x in ZZ implies x >= 0`. // // What was written was `Factorialf({ DomainCondition: var condition })`, a property // pattern on the factorial's *argument*. For a bare variable that condition is True, diff --git a/Sources/Tests/UnitTests/Convenience/FactorialOffTheRealLineTest.cs b/Sources/Tests/UnitTests/Convenience/FactorialOffTheRealLineTest.cs new file mode 100644 index 000000000..fa7533431 --- /dev/null +++ b/Sources/Tests/UnitTests/Convenience/FactorialOffTheRealLineTest.cs @@ -0,0 +1,48 @@ +// +// 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; + +namespace AngouriMath.Tests.Convenience +{ + /// + /// The factorial, and the gamma function with it, is defined everywhere but at the negative integers, its poles, where + /// its condition asked for a real argument as well: i! is 0.498 - 0.155i, and x!/x! simplified to + /// 1 provided x in RR, which has no value at i. + /// #2256 + /// + [Trait("Area", "Convenience")] + public sealed class FactorialOffTheRealLineTest + { + [Theory] + [InlineData("x!", "i", true)] + [InlineData("x!", "1/2 + 6/5 * i", true)] + [InlineData("x!", "-2 * i", true)] + [InlineData("x!", "-1/2", true)] + [InlineData("x!", "0", true)] + [InlineData("x!", "3", true)] + [InlineData("x!", "-1", false)] + [InlineData("x!", "-2", false)] + [InlineData("gamma(x)", "i", true)] + [InlineData("gamma(x)", "0", false)] + [InlineData("gamma(x)", "-3", false)] + public void ItIsDefinedOffThePoles(string expression, string at, bool defined) + { + var condition = expression.ToEntity().DomainCondition.Substitute("x", at.ToEntity()).Evaled; + Assert.Equal(defined ? Entity.Boolean.True : Entity.Boolean.False, condition); + Assert.Equal(!defined, expression.ToEntity().Substitute("x", at.ToEntity()).Evaled.IsNaN); + } + + [Theory] + [InlineData("x! / x!", "i")] + [InlineData("gamma(x) / gamma(x)", "1/2 + 6/5 * i")] + public void ASimplificationKeepsItsValueThere(string expression, string at) + => Assert.Equal(Entity.Number.Integer.One, expression.ToEntity().Simplify().Substitute("x", at.ToEntity()).Evaled); + } +} diff --git a/Sources/Tests/UnitTests/PatternsTest/SimplifyTest.cs b/Sources/Tests/UnitTests/PatternsTest/SimplifyTest.cs index 355c54979..ae0ce22c2 100644 --- a/Sources/Tests/UnitTests/PatternsTest/SimplifyTest.cs +++ b/Sources/Tests/UnitTests/PatternsTest/SimplifyTest.cs @@ -89,13 +89,16 @@ [Fact] public void Patt8Negative() => // with the unsimplified quotient at every one -- NaN at the three poles and 1 elsewhere. // The old form was adequate here by accident, since `(1 + x)!` is NaN at a pole and a // comparison against NaN is not True; the new one says so rather than relying on it. - [Fact] public void FactorialXP1OverFactorialXP1() => AssertSimplify(MathS.Factorial(x + 1) / MathS.Factorial(x + 1), "1 provided 1 + x in RR and (1 + x >= 0 or not 1 + x in ZZ)"); + // A factorial is defined off its poles, the negative integers, and off the real line too: the + // condition asked for 1 + x in RR, so this had no value at x = i, where it is 1. + // https://github.com/asc-community/AngouriMath/issues/2256 + [Fact] public void FactorialXP1OverFactorialXP1() => AssertSimplify(MathS.Factorial(x + 1) / MathS.Factorial(x + 1), "1 provided 1 + x in ZZ implies 1 + x >= 0"); [Fact] public void FactorialXP1OverFactorialX() => AssertSimplify(MathS.Factorial(1 + x) / MathS.Factorial(x), 1 + x); [Fact] public void FactorialXP1OverFactorialXM2() => AssertSimplify(MathS.Factorial(1 + x) / MathS.Factorial(-2 + x), "x3 - x"); [Fact] public void FactorialXP1OverFactorialXM1() => AssertSimplify(MathS.Factorial(1 + x) / MathS.Factorial(-1 + x), x * (1 + x)); [Fact] public void FactorialXP1OverFactorialXM3() => AssertSimplifyIdentical(MathS.Factorial(x + 1) / MathS.Factorial(x - 3)); [Fact] public void FactorialXOverFactorialXP1() => AssertSimplify(MathS.Factorial(x) / MathS.Factorial(x + 1), 1 / (1 + x)); - [Fact] public void FactorialXOverFactorialX() => AssertSimplify(MathS.Factorial(x) / MathS.Factorial(x), "1 provided x in RR and (x >= 0 or not x in ZZ)"); + [Fact] public void FactorialXOverFactorialX() => AssertSimplify(MathS.Factorial(x) / MathS.Factorial(x), "1 provided x in ZZ implies x >= 0"); [Fact] public void FactorialXOverFactorialXM1() => AssertSimplify(MathS.Factorial(0 + x) / MathS.Factorial(x - 1), x); [Fact] public void FactorialXOverFactorialXM2() => AssertSimplify(MathS.Factorial(x + 0) / MathS.Factorial(x - 2), x.Pow(2) - x); [Fact] public void FactorialXOverFactorialXM3() => AssertSimplifyIdentical(MathS.Factorial(x) / MathS.Factorial(x - 3)); @@ -105,7 +108,7 @@ [Fact] public void Patt8Negative() => // commit, because a bare `x!` reached this through the candidate polynomial long division // produces rather than through a cancellation rule. That division carries its divisor's // domain now as well, so all three of these agree again. - [Fact] public void FactorialXM1OverFactorialXM1() => AssertSimplify(MathS.Factorial(x - 1) / MathS.Factorial(x - 1), "1 provided x - 1 in RR and (x - 1 >= 0 or not x - 1 in ZZ)"); + [Fact] public void FactorialXM1OverFactorialXM1() => AssertSimplify(MathS.Factorial(x - 1) / MathS.Factorial(x - 1), "1 provided x - 1 in ZZ implies x - 1 >= 0"); [Fact] public void FactorialXM1OverFactorialXM2() => AssertSimplify(MathS.Factorial(-1 + x) / MathS.Factorial(-2 + x), x - 1); // Same two factors, now in ascending order: the polynomial factorer offers // (x - 1) * (x - 2) and the complexity metric cannot tell the two orders apart.