From 9c5ba978b761a47135d7908f9fd8579cf95d27d5 Mon Sep 17 00:00:00 2001 From: Rafael Vuijk Date: Mon, 7 Sep 2026 00:48:41 +0000 Subject: [PATCH 1/2] Power and Factorization declare the rest of the collecting family #1195 made Collects mean never larger and smaller for some input, and declared the thirteen rules of Common that are a hole matched twice and written once beside one new node. The guide named the relatives in Power and Factorization as next, and this declares them, each on its own count. Power declares nine. Eight are the family -- a ^ n * a, a / a ^ n, a ^ n / a, a ^ n * (a * rest), (c / a) ^ d * a, a / b / b, a / b ^ n / b and a / b / b ^ n -- and every one is 1 - |a| for the repeated hole: a base or a divisor matched twice and written once, against the one node the 1 in the new exponent or the exponent itself costs. The ninth, (c / a) ^ d * a ^ e = c ^ d * a ^ (e - d), was named a relative and is not one: the exponents fold to a leaf and the quotient goes, so it is -1 - |a| outright. Three more stay Unknown and say why beside the rule -- the logarithm of its own base attaches the node's domain condition, and the two radical rules compute through a helper whose answer is a whole times a root or a whole alone. Factorization declares its four: k + k*q, k + k, k - k*q and k*q - k, each 1 - |k|. Seven shapes join the corpus so that each newly declared rule fires on it at least once -- a power beside its own base on either side of a product or a quotient, and a divisor repeated, which the arithmetic grammar builds only with a power of a leaf. No pin moved this time: the safe ceiling still moves two of the five ordinary inputs. The census is 124 collect, 46 rearrange, 31 expand, 123 unjudged; the safe ceiling admits 170 of 324. Part of #746. Full suite 9579 passed, 0 failed -- one of them a throwaway census probe, not committed. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura --- .../Transformations/Matching/MatchedRules.cs | 73 +++++++++++++++---- .../Core/Transformations/Saturation.cs | 4 +- .../Docs/Contributing/WritingARule.md | 9 ++- .../Transformations/ProvidedInAnEClassTest.cs | 2 +- .../Transformations/RuleAuthoringGuideTest.cs | 4 +- .../RuleGrowthAgreesWithTheCorpusTest.cs | 6 ++ 6 files changed, 76 insertions(+), 22 deletions(-) diff --git a/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs b/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs index 1a8178ed0..0ac876040 100644 --- a/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs +++ b/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs @@ -1450,7 +1450,10 @@ is var (divided, remainder) MatchPattern.Commutative(MatchPattern.Any("k"), MatchPattern.Any("q"))), bound => bound["k"] * (1 + bound["q"]), Soundness.Sound, - description: "k + k*q = k*(1 + q)"), + description: "k + k*q = k*(1 + q)", + // The shared term is matched twice and written once, and the 1 is one node more: + // the delta is 1 - |k|, nothing at a leaf and a shrink beyond it. + growth: RewriteRuleGrowth.Collects), // k + k -> 2k new MatchedRule( @@ -1458,7 +1461,10 @@ is var (divided, remainder) MatchPattern.Node(MatchPattern.Any("k"), MatchPattern.Any("k")), bound => 2 * bound["k"], Soundness.Sound, - description: "k + k = 2k"), + description: "k + k = 2k", + // The term is matched twice and written once, and the 2 is one node more: the + // delta is 1 - |k|, nothing at a leaf and a shrink beyond it. + growth: RewriteRuleGrowth.Collects), // k*p - k*q -> k*(p - q). The outer node is a difference and stays one. new MatchedRule( @@ -1480,7 +1486,10 @@ is var (divided, remainder) MatchPattern.Commutative(MatchPattern.Any("k"), MatchPattern.Any("q"))), bound => bound["k"] * (1 - bound["q"]), Soundness.Sound, - description: "k - k*q = k*(1 - q)"), + description: "k - k*q = k*(1 - q)", + // The shared term is matched twice and written once, and the 1 is one node more: + // the delta is 1 - |k|, nothing at a leaf and a shrink beyond it. + growth: RewriteRuleGrowth.Collects), // k*q - k -> k*(q - 1) new MatchedRule( @@ -1490,7 +1499,10 @@ is var (divided, remainder) MatchPattern.Any("k")), bound => bound["k"] * (bound["q"] - 1), Soundness.Sound, - description: "k*q - k = k*(q - 1)"), + description: "k*q - k = k*(q - 1)", + // The shared term is matched twice and written once, and the 1 is one node more: + // the delta is 1 - |k|, nothing at a leaf and a shrink beyond it. + growth: RewriteRuleGrowth.Collects), // k - k -> 0 new MatchedRule( @@ -2767,7 +2779,10 @@ is var (divided, remainder) MatchPattern.Any("a")), bound => new Powf(bound["a"], bound["n"] + 1), Soundness.SoundUnderAssumptions, - description: "a ^ n * a = a ^ (n + 1)"), + description: "a ^ n * a = a ^ (n + 1)", + // The base is matched twice and written once, and the 1 added to the exponent is + // one node more: the delta is 1 - |a|, nothing at a leaf and a shrink beyond it. + growth: RewriteRuleGrowth.Collects), new MatchedRule( "two-powers-of-one-base-multiply-by-adding-exponents", @@ -2900,7 +2915,11 @@ is var (divided, remainder) MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("n"))), bound => new Powf(bound["a"], 1 - bound["n"]), Soundness.SoundUnderAssumptions, - description: "a / a ^ n = a ^ (1 - n)"), + description: "a / a ^ n = a ^ (1 - n)", + // The base is matched twice and written once, and the 1 the exponent is taken + // from is one node more: the delta is 1 - |a|, nothing at a leaf and a shrink + // beyond it. + growth: RewriteRuleGrowth.Collects), new MatchedRule( "a-power-over-its-own-base-lowers-the-exponent", @@ -2909,7 +2928,10 @@ is var (divided, remainder) MatchPattern.Any("a")), bound => new Powf(bound["a"], bound["n"] - 1), Soundness.SoundUnderAssumptions, - description: "a ^ n / a = a ^ (n - 1)"), + description: "a ^ n / a = a ^ (n - 1)", + // The base is matched twice and written once, and the 1 taken from the exponent + // is one node more: the delta is 1 - |a|, nothing at a leaf and a shrink beyond it. + growth: RewriteRuleGrowth.Collects), new MatchedRule( "a-number-raised-to-a-logarithm-of-itself-is-the-antilogarithm", @@ -2957,7 +2979,10 @@ is var (divided, remainder) MatchPattern.Commutative(MatchPattern.Any("a"), MatchPattern.Any("rest"))), bound => new Powf(bound["a"], bound["n"] + 1) * bound["rest"], Soundness.SoundUnderAssumptions, - description: "a ^ n * (a * rest) = a ^ (n + 1) * rest"), + description: "a ^ n * (a * rest) = a ^ (n + 1) * rest", + // The base is matched twice and written once, and the 1 added to the exponent is + // one node more: the delta is 1 - |a|, nothing at a leaf and a shrink beyond it. + growth: RewriteRuleGrowth.Collects), // Taking a factor out from under a root needs that factor positive, or the root to be // a whole power. https://github.com/asc-community/AngouriMath/issues/752 @@ -3001,7 +3026,11 @@ is var (divided, remainder) bound => new Powf(bound["c"], bound["d"]) * new Powf(bound["a"], 1 - (Number)bound["d"]), Soundness.SoundUnderAssumptions, - description: "(c / a) ^ d * a = c ^ d * a ^ (1 - d), for numeric c and d"), + description: "(c / a) ^ d * a = c ^ d * a ^ (1 - d), for numeric c and d", + // The two numbers are leaves and 1 - d folds to one; the base is matched twice + // and written once, and the second power is one node more than the quotient it + // replaces: the delta is 1 - |a|, nothing at a leaf and a shrink beyond it. + growth: RewriteRuleGrowth.Collects), new MatchedRule( "a-power-of-a-numeric-reciprocal-times-a-power-of-its-own-denominator-subtracts-the-exponents", @@ -3013,7 +3042,10 @@ is var (divided, remainder) bound => new Powf(bound["c"], bound["d"]) * new Powf(bound["a"], (Number)bound["e"] - (Number)bound["d"]), Soundness.SoundUnderAssumptions, - description: "(c / a) ^ d * a ^ e = c ^ d * a ^ (e - d), for numeric c, d and e"), + description: "(c / a) ^ d * a ^ e = c ^ d * a ^ (e - d), for numeric c, d and e", + // The three numbers are leaves and e - d folds to one; the base is matched twice + // and written once, and the quotient goes: the delta is -1 - |a|, at most -2. + growth: RewriteRuleGrowth.Collects), new MatchedRule( "dividing-twice-by-one-thing-squares-it", @@ -3022,7 +3054,10 @@ is var (divided, remainder) MatchPattern.Any("b")), bound => bound["a"] / new Powf(bound["b"], 2), Soundness.SoundUnderAssumptions, - description: "a / b / b = a / b ^ 2"), + description: "a / b / b = a / b ^ 2", + // The divisor is matched twice and written once, and the exponent is one node + // more: the delta is 1 - |b|, nothing at a leaf and a shrink beyond it. + growth: RewriteRuleGrowth.Collects), new MatchedRule( "dividing-by-a-power-and-then-by-its-base-raises-the-exponent", @@ -3033,7 +3068,10 @@ is var (divided, remainder) MatchPattern.Any("b")), bound => bound["a"] / new Powf(bound["b"], bound["n"] + 1), Soundness.SoundUnderAssumptions, - description: "a / b ^ n / b = a / b ^ (n + 1)"), + description: "a / b ^ n / b = a / b ^ (n + 1)", + // The divisor is matched twice and written once, and the 1 added to the exponent + // is one node more: the delta is 1 - |b|, nothing at a leaf and a shrink beyond it. + growth: RewriteRuleGrowth.Collects), new MatchedRule( "dividing-by-a-thing-and-then-by-a-power-of-it-raises-the-exponent", @@ -3042,7 +3080,10 @@ is var (divided, remainder) MatchPattern.Node(MatchPattern.Any("b"), MatchPattern.Any("n"))), bound => bound["a"] / new Powf(bound["b"], bound["n"] + 1), Soundness.SoundUnderAssumptions, - description: "a / b / b ^ n = a / b ^ (n + 1)"), + description: "a / b / b ^ n = a / b ^ (n + 1)", + // The divisor is matched twice and written once, and the 1 added to the exponent + // is one node more: the delta is 1 - |b|, nothing at a leaf and a shrink beyond it. + growth: RewriteRuleGrowth.Collects), new MatchedRule( "dividing-by-two-powers-of-one-base-adds-the-exponents", @@ -3092,6 +3133,8 @@ is var (divided, remainder) MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("a")), (node, bound) => new Providedf(1, ((Logf)node).DomainCondition), Soundness.SoundUnderAssumptions, + // Left Unknown: the condition attached is the node's own domain condition, whose + // size nothing here bounds. description: "log(a, a) = 1, where log(a, a) is defined"), // ln(1/b) = -ln(b) is false on the negative reals: at b = -0.63 the two differ by the @@ -3174,6 +3217,8 @@ is var (divided, remainder) Soundness.Sound, when: bound => Functions.Patterns.ReduceRadical( (Integer)bound["radicand"], (Rational)bound["power"]) is not null, + // Left Unknown: the helper answers a whole times a root, two nodes more than the + // pattern, or a whole alone, two fewer. description: "sqrt(8) = 2 * sqrt(2), and its like for a positive whole radicand"), // The rule above takes a whole power out from under one root; this takes a root out @@ -3192,6 +3237,8 @@ is var (divided, remainder) bound => Functions.Patterns.DenestRadical(bound["radicand"])!, Soundness.Sound, when: bound => Functions.Patterns.DenestRadical(bound["radicand"]) is not null, + // Left Unknown: the helper computes the answer, and the radicands it denests take + // more shapes than one count covers. description: "sqrt(5 + 2*sqrt(6)) = sqrt(2) + sqrt(3)")); /// diff --git a/Sources/AngouriMath/Core/Transformations/Saturation.cs b/Sources/AngouriMath/Core/Transformations/Saturation.cs index 41836bea1..2fc5236a8 100644 --- a/Sources/AngouriMath/Core/Transformations/Saturation.cs +++ b/Sources/AngouriMath/Core/Transformations/Saturation.cs @@ -44,8 +44,8 @@ internal static class Saturation /// ceiling should refuse — it means the rule's growth was not judged, because its /// replacement is code rather than a written pattern, so admitting it accepts a rewrite /// nobody measured. But it is where the rules are: of the 324 rules in - /// , 111 collect, 46 rearrange, 31 expand and 136 are - /// unjudged. A ceiling that refuses the fourth value still refuses 42% of the library, + /// , 124 collect, 46 rearrange, 31 expand and 123 are + /// unjudged. A ceiling that refuses the fourth value still refuses 38% of the library, /// and what is left could not do much when this was written — over six expression pairs /// equal only through a larger intermediate form, the /// ceiling proved two, and diff --git a/Sources/AngouriMath/Docs/Contributing/WritingARule.md b/Sources/AngouriMath/Docs/Contributing/WritingARule.md index 905581a9b..e06b88c92 100644 --- a/Sources/AngouriMath/Docs/Contributing/WritingARule.md +++ b/Sources/AngouriMath/Docs/Contributing/WritingARule.md @@ -135,7 +135,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 — **136** rules sit at `Unknown` — but declare it where you can justify it: +honest default — **123** 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, @@ -181,9 +181,10 @@ corpus, and each is false: Two more used to be listed here and are not. The repeated hole that pays a literal to be gathered — `a * (a * b) = a ^ 2 * b`, `k + k = 2 * k` and their relatives, every one `1 - |a|` — was undeclarable only while `Collects` was read as "always fewer"; it is the commonest collecting shape -there is, and `Collects` promises never larger. `Common`'s thirteen are declared, with the count in -each one's comment; the relatives in `Power` and `Factorization` — `a ^ n * a`, `a / b / b` and -theirs — are the next to declare, each on its own count. And the reciprocal-factor rules were said +there is, and `Collects` promises never larger. `Common`'s thirteen, `Power`'s eight and +`Factorization`'s four are declared, with the count in each one's comment — and the count is worth +doing, since `Power`'s ninth relative, `(c / a) ^ d * a ^ e`, turned out to be `-1 - |a|` outright +rather than one of the family. And the reciprocal-factor rules were said to admit two spellings of one thing; `IsWholeReciprocal` is `entity is Rational(...)`, so it admits the literal only, and the pair is exactly `Rearranges` and exactly `Expands`. diff --git a/Sources/Tests/UnitTests/Core/Transformations/ProvidedInAnEClassTest.cs b/Sources/Tests/UnitTests/Core/Transformations/ProvidedInAnEClassTest.cs index abf8ce0ca..aacf1fb5c 100644 --- a/Sources/Tests/UnitTests/Core/Transformations/ProvidedInAnEClassTest.cs +++ b/Sources/Tests/UnitTests/Core/Transformations/ProvidedInAnEClassTest.cs @@ -94,7 +94,7 @@ public void NoWrittenPatternIntroducesACondition() /// before the graph is wired into anything. /// /// - /// SafeRules is RulesUpTo(Rearranges), 157 of 324 rules. The 136 sitting at + /// SafeRules is RulesUpTo(Rearranges), 170 of 324 rules. The 123 sitting at /// Unknown are excluded by design, since their growth was never judged — so the /// ceiling that is safe to run finds little, and the ceiling that finds things admits /// rewrites nobody measured. That trade is the open part of tier 2, and this pins where it diff --git a/Sources/Tests/UnitTests/Core/Transformations/RuleAuthoringGuideTest.cs b/Sources/Tests/UnitTests/Core/Transformations/RuleAuthoringGuideTest.cs index 04e98e45b..588e5a034 100644 --- a/Sources/Tests/UnitTests/Core/Transformations/RuleAuthoringGuideTest.cs +++ b/Sources/Tests/UnitTests/Core/Transformations/RuleAuthoringGuideTest.cs @@ -89,7 +89,7 @@ public void ReplacementAPatternOrCode() "how many rules have a pattern on both sides"); Stated(33, rules.Count(rule => rule.Reversed is not null), "how many two-sided rules have a direction"); - Stated(136, rules.Count(rule => rule.Growth is RewriteRuleGrowth.Unknown), + Stated(123, rules.Count(rule => rule.Growth is RewriteRuleGrowth.Unknown), "how many rules sit at Unknown growth"); // The rest of the census, because `Saturation.RulesUpTo` argues from it in prose and @@ -97,7 +97,7 @@ public void ReplacementAPatternOrCode() // rearrange, 9 expand and 270 unjudged", measured before the growth declarations // went in. The argument survived; the arithmetic did not. A number a remark reasons // from belongs somewhere that fails when it moves. - Stated(111, rules.Count(rule => rule.Growth is RewriteRuleGrowth.Collects), + Stated(124, rules.Count(rule => rule.Growth is RewriteRuleGrowth.Collects), "how many rules are declared Collects"); Stated(46, rules.Count(rule => rule.Growth is RewriteRuleGrowth.Rearranges), "how many rules are declared Rearranges"); diff --git a/Sources/Tests/UnitTests/Core/Transformations/RuleGrowthAgreesWithTheCorpusTest.cs b/Sources/Tests/UnitTests/Core/Transformations/RuleGrowthAgreesWithTheCorpusTest.cs index 679c11971..da183e168 100644 --- a/Sources/Tests/UnitTests/Core/Transformations/RuleGrowthAgreesWithTheCorpusTest.cs +++ b/Sources/Tests/UnitTests/Core/Transformations/RuleGrowthAgreesWithTheCorpusTest.cs @@ -145,6 +145,12 @@ public sealed class RuleGrowthAgreesWithTheCorpusTest // a sum or a difference of itself -- and the sign-times-absolute-value cancellation. "x + x * y", "x + (x + y)", "x + (x - y)", "x - (y - x)", "(y - x) - x", "sgn(x) * (y * x) / abs(x)", + + // A power beside its own base, on either side of a product or a quotient, and a + // divisor repeated -- the collecting shapes of `Power` that the arithmetic grammar + // builds only with a power of a leaf. + "x ^ 2 * x", "x / x ^ 2", "x ^ 2 / x", "(2 / x) ^ 3 * x", "(2 / x) ^ 3 * x ^ 2", + "x / y / y", "x / y ^ 2 / y", }; private static List Corpus() From ed770fce593f1c56e639c080f013fd94a1e83012 Mon Sep 17 00:00:00 2001 From: Rafael Vuijk Date: Mon, 7 Sep 2026 00:54:55 +0000 Subject: [PATCH 2/2] Record the answers the thirteen declarations change Measured on a build of master (4b105e69) and of this branch, with one throwaway probe run on each. Over Transformation.CanonicalizationOverGraph(budget), (2 / x) ^ 3 * x was left as (2 * 1 / x) ^ 3 * x and is 8 * x ^ (-2); (2 / x) ^ 3 * x ^ 2 is 8 * 1 / x. The other Power shapes are unchanged for a measured reason -- x ^ 2 * x reaches x ^ (2 + 1) over the graph, no smaller at a leaf, and no safe rule folds the exponent, so the input is kept -- and Factorization's four have Common twins declared in #1195, so a + a * b was already (1 + b) * a. Entity.Canonicalize() is unchanged on every input probed. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura --- BREAKING-CHANGES.md | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) diff --git a/BREAKING-CHANGES.md b/BREAKING-CHANGES.md index da8b0f73d..945c7bdbc 100644 --- a/BREAKING-CHANGES.md +++ b/BREAKING-CHANGES.md @@ -74,6 +74,8 @@ read first. | | the same on `x + x`, and `x + x * y` | `x + x`, `x * y + x` — left as written | `2 * x`, `(1 + y) * x` | | **Silent** | `RewriteRules.Common.Rules[i].Growth`, for sixteen rules | `Unknown` | `Collects` for fourteen, `Rearranges` and `Expands` for the reciprocal-factor pair | | **Silent** | what `RewriteRuleGrowth.Collects` promises | fewer nodes for every input | never more, and fewer for some — every rule that was `Collects` still is | +| | `Transformation.CanonicalizationOverGraph(budget).ApplyOrKeep("(2 / x) ^ 3 * x")`, and its like with a power of the denominator | `(2 * 1 / x) ^ 3 * x` — left as written | `8 * x ^ (-2)`; `(2 / x) ^ 3 * x ^ 2` is `8 * 1 / x` | +| **Silent** | `RewriteRules.Power.Rules[i].Growth` for nine rules, and `Factorization`'s for four | `Unknown` | `Collects` | ### A cancelled quotient says its operand is defined, not only non-zero @@ -900,6 +902,30 @@ and answers exactly as before on every input below. | `RewriteRules.All` by growth | 97 / 45 / 30 / 152 | 111 / 46 / 31 / 136 | | what `RewriteRuleGrowth.Collects` promises | fewer nodes for every input | never more, and fewer for some | +### `Power` and `Factorization` declare the rest of the collecting family + +The entry above named the relatives of the `1 − |a|` shape in `Power` and `Factorization` as next. +Nine rules of `Power` — `a ^ n * a`, `a / a ^ n`, `a ^ n / a`, `a ^ n * (a * rest)`, +`(c / a) ^ d * a`, `(c / a) ^ d * a ^ e`, `a / b / b`, `a / b ^ n / b`, `a / b / b ^ n` — and four of +`Factorization` — `k + k * q`, `k + k`, `k - k * q`, `k * q - k` — declare `Collects`, each on its +own count; three more of `Power` stay `Unknown` with the reason written beside the rule. The safe +ceiling admits 170 of 324 rules where it admitted 157. + +On ordinary input little moves, and for a measured reason: `x ^ 2 * x` reaches `x ^ (2 + 1)` over +the graph, which is no smaller at a leaf, and no safe rule folds the exponent, so the input is kept; +and `Factorization`'s four have twins in `Common` that were declared in the entry above, so +`a + a * b` was already `(1 + b) * a`. What does move is the power of a reciprocal beside its own +denominator, whose exponents fold as the replacement is built. + +| | Was | Is | +|---|---|---| +| `Transformation.CanonicalizationOverGraph(budget).ApplyOrKeep("(2 / x) ^ 3 * x")` | `(2 * 1 / x) ^ 3 * x` — left as written | `8 * x ^ (-2)` | +| the same on `(2 / x) ^ 3 * x ^ 2` | `(2 * 1 / x) ^ 3 * x ^ 2` | `8 * 1 / x` | +| the same on `x ^ 2 * x`, `x / x ^ 2`, `x ^ 2 / x`, `x / y / y`, `a + a * b`, `a + a` | `x ^ 2 * x`, `1 / x ^ 2 * x`, `1 / x * x ^ 2`, `(1 / y) ^ 2 * x`, `(1 + b) * a`, `2 * a` | the same | +| `RewriteRules.Power.Rules` by growth — collects / rearranges / expands / unknown | 13 / 6 / 1 / 13 | 22 / 6 / 1 / 4 | +| `RewriteRules.Factorization.Rules` by growth | 4 / 0 / 2 / 5 | 8 / 0 / 2 / 1 | +| `RewriteRules.All` by growth | 111 / 46 / 31 / 136 | 124 / 46 / 31 / 123 | + ## 2.4.0 — since 2.3.0 Released 2026-08-28. These entries sat under “Unreleased” while 2.4.0 was tagged and