The binomial coefficient's identities as rules, and its sums in closed form

BREAKING-CHANGES.md

@@ -725,6 +725,25 @@ names are keywords now, and were names.
 | `preimage(x^2, x in RR, {1})` | `UnhandledParseException` | `{ 1, -1 }` |
 | `{ x in ZZ : x^2 in {1, 4} }` | `{ x in ZZ : x ^ 2 in { 1, 4 } }` — left as written | `{ 1, -1, 2, -2 }` |
 
+### The binomial coefficient's identities, and its sums in closed form
+
+Pascal's rule, the chairperson identity and the symmetry are rewrite rules, each in the direction
+that collects (`binomial(n - 1, k) + binomial(n - 1, k - 1)` → `binomial(n, k)`,
+`n binomial(n - 1, k - 1)` → `k binomial(n, k)`, `binomial(n, n - k)` → `binomial(n, k)`), so the
+identities are `True` as statements of symbols; a sum written with `binomial(n, k)` is the binomial
+theorem read backwards, as the factorial spelling already was (`sum(binomial(n, k) x^k y^(n - k), k, 0, n)`
+is `(x + y)^n` for `n >= 0`). **Wrong answer fixed** in the alternating sum, in both spellings:
+`sum(binomial(n, k) (-1)^k, k, 0, n)` is `1` at `n = 0` and `0` above, and the closed form `0^n`
+carried a condition the piecewise read as no value, so the sum was `0` at `n = 0`
+([#1409](https://github.com/asc-community/AngouriMath/issues/1409), the reference's §8.4).
+
+| Input | Was (2.5.0) | Now |
+|---|---|---|
+| `"binomial(n, k) = binomial(n, n - k)".ToEntity().Simplify()` | `UnhandledParseException` — `binomial` is new since, and was left as written when it arrived | `True` |
+| `"binomial(n - 1, k) + binomial(n - 1, k - 1)".ToEntity().Simplify()` | `UnhandledParseException` | `binomial(n, k)` |
+| `"sum(binomial(n, k), k, 0, n)".ToEntity().Evaled` | `UnhandledParseException` | `piecewise((2 ^ n) provided (n >= 0), 0 provided True)` |
+| `"sum(n! / (k! (n - k)!) (-1)^k, k, 0, n)".ToEntity().Evaled` | `piecewise(0 provided True)` — wrong at `n = 0` | `piecewise(1 provided (n = 0), 0 provided True)` |
+
 ### `binomial(n, k)` is a function
 
 **Addition, not silent.** The binomial coefficient is a node, `Entity.Binomialf`, spelled

Sources/.editorconfig

@@ -291,6 +291,9 @@ file_header_template=\nCopyright (c) 2019-2026 Angouri.\nAngouriMath is licensed
 [AngouriMath/Functions/NumberTheory/ResidueClasses.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/BinomialIdentityTest.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/ConjunctionFilterTest.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/Core/Transformations/Matching/MatchedRules.cs

@@ -856,7 +856,43 @@ is var (divided, remainder)
                     node, bound["x"], bound["y"], (Number)bound["a"], Integer.Create(0)),
                 Soundness.SoundUnderAssumptions,
                 // Left Unknown: as above, the answer's size is the offset's.
-                description: "(x + a)! * y = (x + a + 1)!, where y is the next term"));
+                description: "(x + a)! * y = (x + a + 1)!, where y is the next term"),
+
+            // The binomial coefficient's three identities, each in the direction that collects:
+            // Pascal's rule, the chairperson identity and the symmetry. The reference's
+            // Props 8.4.1-8.4.3 (Sullivan and Mackey), which it proves by counting in two ways;
+            // here they are identities of the falling factorial for a whole lower index and of
+            // the gamma function elsewhere. https://github.com/asc-community/AngouriMath/issues/1409
+            new MatchedRule(
+                "two-binomial-coefficients-of-one-upper-index-and-adjacent-lower-indices-add-by-pascals-rule",
+                MatchPattern.Node<Sumf>(
+                    MatchPattern.Node<Binomialf>(MatchPattern.Any("n"), MatchPattern.Any("k")),
+                    MatchPattern.Node<Binomialf>(MatchPattern.Any("n"), MatchPattern.Any("j"))),
+                (node, bound) => Functions.Patterns.PascalsRule(node, bound["n"], bound["k"], bound["j"]),
+                Soundness.SoundUnderAssumptions,
+                // Left Unknown: which of the two lower indices is the larger is decided by the
+                // helper, and the answer is one coefficient where there were two.
+                description: "binomial(n, k) + binomial(n, k - 1) = binomial(n + 1, k)"),
+
+            new MatchedRule(
+                "a-number-times-a-binomial-coefficient-of-the-number-less-one-is-the-chairperson-identity",
+                MatchPattern.Commutative<Mulf>(
+                    MatchPattern.Any("n"),
+                    MatchPattern.Node<Binomialf>(MatchPattern.Any("m"), MatchPattern.Any("j"))),
+                (node, bound) => Functions.Patterns.ChairpersonsRule(node, bound["n"], bound["m"], bound["j"]),
+                Soundness.SoundUnderAssumptions,
+                // Left Unknown: fires only where the multiplier is one more than the upper
+                // index, and the answer is written with the lower index one more.
+                description: "n * binomial(n - 1, k - 1) = k * binomial(n, k)"),
+
+            new MatchedRule(
+                "a-binomial-coefficient-whose-lower-index-is-the-complement-is-the-symmetric-one",
+                MatchPattern.Node<Binomialf>(MatchPattern.Any("n"), MatchPattern.Any("d")),
+                (node, bound) => Functions.Patterns.SymmetricBinomial(node, bound["n"], bound["d"]),
+                Soundness.SoundUnderAssumptions,
+                // Left Unknown: fires only where the complement of the lower index is the
+                // smaller expression, and the answer is the coefficient with that.
+                description: "binomial(n, n - k) = binomial(n, k)"));
 
         /// <summary>
         /// <see cref="Functions.Patterns.PerfectSquareRules"/>, as data.

Sources/AngouriMath/Docs/Contributing/WritingARule.md

@@ -18,7 +18,7 @@ effect". This is how to supply those seven things.
 ## Where a rule goes
 
 `Core/Transformations/Matching/MatchedRules.cs`, as a value in a `MatchedRuleSet`. **33** sets and
-**332** rules live there today.
+**335** rules live there today.
 
 The `switch` statements in `Functions/Simplification/Patterns` are the older form. **All thirty
 registered sets now run as data and describe what they run**; none executes its `switch` any more.
@@ -64,7 +64,7 @@ in a name and putting the identity in brackets after it:
 2. Tangent is sine over cosine (tan(a) = sin(a) / cos(a)), so tan(x) becomes sin(x) / cos(x).
 ```
 
-So the name has to be a clause that survives being read that way. **All 303 distinct rule names are,
+So the name has to be a clause that survives being read that way. **All 306 distinct rule names are,
 and `StepAsASentenceTest` holds them to it** — a name with a capital, a bracket or an underscore
 fails that test rather than degrading the prose quietly.
 
@@ -91,7 +91,7 @@ debugged for an afternoon.
 | `Left.ToString()` | `Divf(var a, Divf(var b, var c))` — how the matcher spells it |
 
 Write the identity with `=`, not `->`: it is an equality, and the arrow belongs to the direction the
-rule happens to be applied in. **329** rules carry one today; a new rule should.
+rule happens to be applied in. **332** rules carry one today; a new rule should.
 
 ## The pattern language
 
@@ -137,7 +137,7 @@ A pattern replacement gets:
 - **an exact growth**, counted from the two patterns rather than declared.
 
 A code replacement gets neither, and its growth is `Unknown` unless you declare one. That is the
-honest default — **123** rules sit at `Unknown` — but declare it where you can justify it:
+honest default — **126** rules sit at `Unknown` — but declare it where you can justify it:
 
 ```csharp
 // The Chebyshev expansion of sin(n * a) is a sum of n terms where the pattern is one node,
@@ -226,7 +226,7 @@ limit, against nothing for handing the node over.
 | `SoundUnderAssumptions` | holds given something the rule does not check |
 | `Heuristic` | usually right |
 
-**186** of the 332 rules are `Sound` and **146** are conditional. Every one of the thirty registered
+**186** of the 335 rules are `Sound` and **149** are conditional. Every one of the thirty registered
 *sets* declares `SoundUnderAssumptions`, because a set's tier is the **minimum** over its rules — so
 the set grain says nothing and the rule grain says everything. A derivation reports the rule's tier
 (`RewriteStep.Soundness`), which is why getting it right matters beyond the label.

Sources/AngouriMath/Functions/Algebra/Polynomials/BinomialSum.cs

@@ -70,6 +70,12 @@ internal static class BinomialSum
                 }
                 switch (factor)
                 {
+                    // The coefficient written as the node it is, binomial(N, k) or binomial(N, N - k):
+                    // the three factorials at once. https://github.com/asc-community/AngouriMath/issues/1409
+                    case Binomialf(var top, var bottom) when top == upper && (bottom == index || IsUpperMinusIndex(bottom, upper, index))
+                        && !sawTop && !sawBottomK && !sawBottomRest:
+                        sawTop = sawBottomK = sawBottomRest = true;
+                        break;
                     case Powf(Factorialf(var argument), var power) when power == Integer.MinusOne && argument == index && !sawBottomK:
                         sawBottomK = true;
                         break;
@@ -98,7 +104,27 @@ internal static class BinomialSum
 
             Entity closed;
             if (angle is null)
-                closed = MathS.Pow((powerOfK ?? Integer.One) + (powerOfRest ?? Integer.One), upper);
+            {
+                var @base = ((powerOfK ?? Integer.One) + (powerOfRest ?? Integer.One)).InnerSimplified;
+                // A base that is zero, sum((-1)^k binomial(N, k)): 0^N is 1 at N = 0 and 0 for
+                // every N above it, and 0^N written as a power carries a condition that the
+                // piecewise below would read as "no value", making the sum 0 at N = 0 where it
+                // is 1. Said outright instead.
+                if (@base.Evaled is Complex { IsZero: true } || @base.Simplify().Evaled is Complex { IsZero: true })
+                {
+                    if (!sawTop)
+                        return null;
+                    Entity zeroPower = upper.Evaled is Integer whole
+                        ? (whole.EInteger.IsZero ? Integer.One : Integer.Zero)
+                        : MathS.Piecewise(new[]
+                        {
+                            new Providedf(Integer.One, new Equalsf(upper, Integer.Zero)),
+                            new Providedf(Integer.Zero, Entity.Boolean.True),
+                        });
+                    return (constant * zeroPower).InnerSimplified;
+                }
+                closed = MathS.Pow(@base, upper);
+            }
             else
             {
                 var half = angle / 2;

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

@@ -101,9 +101,57 @@ internal static Entity FactorizeFactorialMultiplications(Entity expr)
                     GatherFactorial(expr, any1, any1a, const1, 0),
                 Mulf(Factorialf(Sumf(Number const1, var any1)), var any1a) =>
                     GatherFactorial(expr, any1, any1a, const1, 0),
+
+                // The binomial coefficient's three identities, in the direction that collects.
+                // https://github.com/asc-community/AngouriMath/issues/1409
+                Sumf(Binomialf(var top1, var k), Binomialf(var top2, var j)) when top1 == top2 => PascalsRule(expr, top1, k, j),
+                Mulf(var n, Binomialf(var top, var j)) => ChairpersonsRule(expr, n, top, j),
+                Mulf(Binomialf(var top, var j), var n) => ChairpersonsRule(expr, n, top, j),
+                Binomialf(var top, var d) => SymmetricBinomial(expr, top, d),
                 _ => expr
             };
 
+        /// <summary>
+        /// <c>binomial(a, k) + binomial(a, k - 1)</c> is <c>binomial(a + 1, k)</c> -- Pascal's rule,
+        /// an identity of the falling factorial for every <c>a</c> and whole <c>k</c>, and of the
+        /// gamma function elsewhere -- read in either order of the two, with the lower index that
+        /// is one less found by simplifying the difference; <paramref name="whole"/> where neither is.
+        /// </summary>
+        internal static Entity PascalsRule(Entity whole, Entity top, Entity k, Entity j)
+        {
+            if (PartialFractions.Bare((k - j).Simplify()) == Integer.One)
+                return new Binomialf((top + 1).InnerSimplified, k);
+            if (PartialFractions.Bare((j - k).Simplify()) == Integer.One)
+                return new Binomialf((top + 1).InnerSimplified, j);
+            return whole;
+        }
+
+        /// <summary>
+        /// <c>n * binomial(n - 1, k - 1)</c> is <c>k * binomial(n, k)</c> -- the chairperson identity,
+        /// choosing the chair first or the committee first -- where the multiplier is one more
+        /// than the upper index; <paramref name="whole"/> otherwise.
+        /// </summary>
+        internal static Entity ChairpersonsRule(Entity whole, Entity n, Entity top, Entity j)
+        {
+            if (n.ContainsNode(top) || top.ContainsNode(n) ? PartialFractions.Bare((n - top).Simplify()) != Integer.One : (n - top).InnerSimplified != Integer.One)
+                return whole;
+            var k = (j + 1).InnerSimplified;
+            return k * new Binomialf(n, k);
+        }
+
+        /// <summary>
+        /// <c>binomial(n, n - k)</c> is <c>binomial(n, k)</c>, taken where the complement is the
+        /// smaller expression: the symmetry of the coefficient, an identity of the gamma
+        /// function; <paramref name="whole"/> where the lower index is already the smaller.
+        /// </summary>
+        internal static Entity SymmetricBinomial(Entity whole, Entity top, Entity d)
+        {
+            if (!d.ContainsNode(top) || top is Number)
+                return whole;
+            var complement = PartialFractions.Bare((top - d).Simplify());
+            return complement.Complexity < d.Complexity ? new Binomialf(top, complement) : whole;
+        }
+
         /// <summary>
         /// The factorial one term further on, where the term multiplying it is the next one — and
         /// <paramref name="whole"/> where it is not. A static method for the same reason

Sources/AngouriMath/Functions/Simplification/Simplificator.cs

@@ -306,7 +306,9 @@ void __IterAddHistory(Entity expr)
                     AddHistory(res = Simplified(recording, res.Rewrite(RewriteRules.InequalityEquality)));
                 }
 
-                if (res.Nodes.Any(child => child is Factorialf))
+                // A binomial coefficient is three factorials, and its identities live in the
+                // gathering set. https://github.com/asc-community/AngouriMath/issues/1409
+                if (res.Nodes.Any(child => child is Factorialf or Binomialf))
                 {
                     AddHistory(res = Simplified(recording, res.Rewrite(RewriteRules.ExpandFactorialDivisions)));
                     AddHistory(res = Simplified(recording, res.Rewrite(RewriteRules.FactorizeFactorialMultiplications)));

Sources/Tests/UnitTests/Core/BinomialIdentityTest.cs

@@ -0,0 +1,77 @@
+//
+// 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 binomial coefficient's identities: Pascal's rule, the chairperson identity and the
+    /// symmetry as rewrite rules, and the binomial theorem read backwards for a sum written
+    /// with <c>binomial(n, k)</c>. Item 7 of the reference's docket (Sullivan and Mackey,
+    /// §8.4: Props 8.4.1–8.4.4, Thm 8.4.8, Ex 8.4.9, §8.4.5 Try 3).
+    /// <see href="https://github.com/asc-community/AngouriMath/issues/1409"/>
+    /// </summary>
+    [Trait("Area", "Core")]
+    public sealed class BinomialIdentityTest
+    {
+        /// <summary>Props 8.4.1–8.4.3 as equalities of symbols, decided by rewriting one side into the other.</summary>
+        [Theory]
+        [InlineData("binomial(n, k) = binomial(n, n - k)")]
+        [InlineData("binomial(n, k) = binomial(n - 1, k) + binomial(n - 1, k - 1)")]
+        [InlineData("binomial(n + 1, k + 1) = binomial(n, k + 1) + binomial(n, k)")]
+        [InlineData("k * binomial(n, k) = n * binomial(n - 1, k - 1)")]
+        public void AnIdentityIsTrue(string identity)
+            => Assert.Equal(Boolean.True, identity.ToEntity().Simplify());
+
+        /// <summary>The rewrites themselves, each in the direction that collects.</summary>
+        [Theory]
+        [InlineData("binomial(n - 1, k) + binomial(n - 1, k - 1)", "binomial(n, k)")]
+        [InlineData("binomial(n, n - 2)", "binomial(n, 2)")]
+        [InlineData("binomial(n, n - k)", "binomial(n, k)")]
+        [InlineData("n * binomial(n - 1, k - 1)", "binomial(n, k) * k")]
+        [InlineData("binomial(7, 3) + binomial(7, 2)", "56")]
+        public void ARewriteCollects(string input, string expected)
+            => Assert.Equal(expected.ToEntity(), input.ToEntity().Simplify());
+
+        /// <summary>The symmetry fires only where the complement is the smaller expression: <c>binomial(n, 2)</c> stays.</summary>
+        [Fact]
+        public void TheSymmetryPrefersTheSmallerLowerIndex()
+        {
+            Assert.Equal("binomial(n, 2)".ToEntity(), "binomial(n, 2)".ToEntity().Simplify());
+            Assert.Equal("binomial(n, k)".ToEntity(), "binomial(n, k)".ToEntity().Simplify());
+        }
+
+        /// <summary>Thm 8.4.8, Prop 8.4.4, §8.4.5 Try 3 and Ex 8.4.9: the sum written with the node, in closed form.</summary>
+        [Theory]
+        [InlineData("sum(binomial(n, k), k, 0, n)", "piecewise((2 ^ n) provided (n >= 0), 0 provided True)")]
+        [InlineData("sum(binomial(n, k) * 2^(n - k), k, 0, n)", "piecewise((3 ^ n) provided (n >= 0), 0 provided True)")]
+        [InlineData("sum(binomial(n, k) * x^k * y^(n - k), k, 0, n)", "piecewise(((x + y) ^ n) provided (n >= 0), 0 provided True)")]
+        [InlineData("sum(binomial(n, n - k) * x^k, k, 0, n)", "piecewise(((x + 1) ^ n) provided (n >= 0), 0 provided True)")]
+        [InlineData("sum(binomial(4, k) * 2^(4 - k), k, 0, 4)", "81")]
+        [InlineData("sum(binomial(10, k), k, 0, 10)", "1024")]
+        public void ABinomialSumIsTheTheoremReadBackwards(string sum, string expected)
+            => Assert.Equal(expected.ToEntity().Evaled, sum.ToEntity().Evaled);
+
+        /// <summary>
+        /// Ex 8.4.9: the alternating sum is <c>0^n</c>, which is <c>1</c> at <c>n = 0</c> and
+        /// <c>0</c> above it. Written as the power it carried a condition the piecewise read as
+        /// no value, and the sum was <c>0</c> at <c>n = 0</c> where it is <c>1</c> -- in the
+        /// factorial spelling too, which is fixed by the same arm.
+        /// </summary>
+        [Theory]
+        [InlineData("sum(binomial(n, k) * (-1)^k, k, 0, n)", "piecewise(1 provided (n = 0), 0 provided True)")]
+        [InlineData("sum(n! / (k! * (n - k)!) * (-1)^k, k, 0, n)", "piecewise(1 provided (n = 0), 0 provided True)")]
+        [InlineData("sum(binomial(0, k) * (-1)^k, k, 0, 0)", "1")]
+        [InlineData("sum(binomial(4, k) * (-1)^k, k, 0, 4)", "0")]
+        public void TheAlternatingSumIsOneAtZero(string sum, string expected)
+            => Assert.Equal(expected.ToEntity().Evaled, sum.ToEntity().Evaled);
+    }
+}

Sources/Tests/UnitTests/Core/Transformations/AddressableRulesTest.cs

@@ -216,9 +216,9 @@
                 {
                     // The switch fell through to its discard arm, so no arm matched — and no rule
                     // may claim to have.
                     if (rule is not null && !rule.TryApply(node).Equals(node))
                         disagreements.Add($"{node.Stringize()}: the switch did nothing, "
                             + $"but '{rule.Name}' claims {rule.TryApply(node).Stringize()}");
                     continue;
                 }
 
@@ -299,7 +299,7 @@
             // are thirty-three; NumericNeat's sixteen are eleven, six of them being three rules
             // written once per side a negative factor can sit on; and the two factorial sets are
             // eight arms each written as three. Every other repointed set is one arm for one rule.
-            Assert.Equal(329, withRules.Sum(set => set.Rules.Count));
+            Assert.Equal(332, withRules.Sum(set => set.Rules.Count));
         }
 
         /// <summary>
@@ -392,7 +392,7 @@
             var step = Assert.Single(recording.Steps);
             Assert.Equal(RewriteRules.Common, step.RuleSet);
             Assert.NotNull(step.Rule);
             Assert.Equal("dividing-by-a-quotient-multiplies-by-its-reciprocal", step.Rule.Name);
             Assert.Equal("a / (b / c) = a * c / b", step.Rule.Description);
             // The matcher's spelling of the pattern, not the `switch`'s. This read
             // `Divf(var any1, Divf(var any2, var any3))` until `Common` was described by the rules