Seven rules say how much they expand (#1159)

Seven rules say how much they expand

Growth is `Unknown` for a code replacement unless it is declared, and 262 rules
sat there. Seven of them can say what they do, each argued from the shape of the
replacement rather than from the corpus, and each measured against the corpus as
well.

Two mechanisms, the same arithmetic. Six are negation rules -- (-a) + (-b),
(-a) - x, and the four that bring a negative factor out of a product, a
numerator or a denominator -- where the operators map one for one, the literal
is replaced by its magnitude, and the negation the replacement puts round the
whole of it is two nodes. The seventh is a ^ n = 1 / a ^ (-n), where the power
stays a power with its exponent replaced one for one and the quotient and its
numerator are the two.

Expands rather than the other two on purpose, and not only because it is what
they do. Saturation.RulesUpTo builds its set as the rules up to Rearranges, so
Collects and Rearranges are declarations that change which rules equality
saturation fires while Expands is one that does not. These seven record what was
already true without moving anything, which is the right first batch; the ones
that would change the saturation want it measured before and after, and that is
a separate change.

An eighth was measured at +2 on all 18 of its firings and is left alone.
`a-negated-reciprocal-rational-factor-is-a-negated-division` counts five nodes to
five when I work through its pattern, so the measurement and the reading disagree
and I cannot argue the claim. WritingARule.md says to leave such a rule Unknown,
and that applies to the person who wrote the sentence.

Full suite 9552 passed, 0 failed.

Part of #825.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura

Author: Rafael-SOWNet

Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs

@@ -373,7 +373,13 @@ internal static class MatchedRules
                 // than an identity that needs one. Measured at 0 as well as away from it before
                 // the tier was written down.
                 Soundness.Sound,
-                description: "a ^ n = 1 / a ^ (-n), for a negative integer n"));
+                description: "a ^ n = 1 / a ^ (-n), for a negative integer n",
+                // Three nodes become five, for every input: the power stays a power with its
+                // exponent replaced one for one, and the quotient and the numerator 1 the
+                // replacement wraps it in are the two. A different mechanism from the negation
+                // rules that share this figure, and the same arithmetic. Measured at +2 on all
+                // 27 firings over the corpus.
+                growth: RewriteRuleGrowth.Expands));
 
         /// <summary>
         /// <see cref="Functions.Patterns.InvertNegativeMultipliers"/>, as data.
@@ -924,7 +930,11 @@ is var (divided, remainder)
                     MatchPattern.Any<Real>("r", value => value.IsNegative)),
                 bound => -((-(Real)bound["l"]) + (Entity)(-(Real)bound["r"])),
                 Soundness.Sound,
-                description: "(-a) + (-b) = -(a + b)"),
+                description: "(-a) + (-b) = -(a + b)",
+                // Three nodes become five, for every input: the negation the replacement puts
+                // round the whole sum is two nodes, and each literal is replaced by its
+                // magnitude one for one. Measured at +2 on all 9 firings over the corpus.
+                growth: RewriteRuleGrowth.Expands),
 
             // x + (-a) -> x - a, either way round
             new MatchedRule(
@@ -964,7 +974,11 @@ is var (divided, remainder)
                     MatchPattern.Any("x")),
                 bound => -(bound["x"] + -(Real)bound["n"]),
                 Soundness.Sound,
-                description: "(-a) - x = -(x + a)"),
+                description: "(-a) - x = -(x + a)",
+                // Three nodes become five, for every input: the difference becomes a sum, one
+                // operator for one, and the negation round the whole of it is the two.
+                // Measured at +2 on all 27 firings over the corpus.
+                growth: RewriteRuleGrowth.Expands),
 
             // (-a) * (-b) -> a * b
             new MatchedRule(
@@ -996,7 +1010,12 @@ is var (divided, remainder)
                     MatchPattern.Any("y")),
                 bound => -((-(Real)bound["n"]) * (bound["x"] * bound["y"])),
                 Soundness.Sound,
-                description: "(-a * x) * y = -(a * (x * y))"),
+                description: "(-a * x) * y = -(a * (x * y))",
+                // Five nodes become seven, for every input: the two products are regrouped, two
+                // operators for two, the literal is replaced by its magnitude one for one, and
+                // the negation round the whole of it is the difference. Measured at +2 on all
+                // 63 firings over the corpus.
+                growth: RewriteRuleGrowth.Expands),
 
             // (-a * x) / y -> -(a * (x / y))
             new MatchedRule(
@@ -1008,7 +1027,11 @@ is var (divided, remainder)
                     MatchPattern.Any("y")),
                 bound => -((-(Real)bound["n"]) * (bound["x"] / bound["y"])),
                 Soundness.Sound,
-                description: "(-a * x) / y = -(a * (x / y))"),
+                description: "(-a * x) / y = -(a * (x / y))",
+                // Five nodes become seven, by the same count as its two neighbours: operators
+                // for operators, magnitude for literal, and the negation is the two. Measured
+                // at +2 on all 63 firings over the corpus.
+                growth: RewriteRuleGrowth.Expands),
 
             // y * (-a * x) -> -(a * (x * y))
             new MatchedRule(
@@ -1020,7 +1043,10 @@ is var (divided, remainder)
                         MatchPattern.Any("x"))),
                 bound => -((-(Real)bound["n"]) * (bound["x"] * bound["y"])),
                 Soundness.Sound,
-                description: "y * (-a * x) = -(a * (x * y))"),
+                description: "y * (-a * x) = -(a * (x * y))",
+                // Five nodes become seven, the mirror of the left-product rule above and by the
+                // same count. Measured at +2 on all 84 firings over the corpus.
+                growth: RewriteRuleGrowth.Expands),
 
             // y / (-a * x) -> -(y / (a * x)). What is left stays under the line: written the
             // other way, as the numerator rules above are, the quotient came back inverted --
@@ -1034,7 +1060,11 @@ is var (divided, remainder)
                         MatchPattern.Any("x"))),
                 bound => -(bound["y"] / ((-(Real)bound["n"]) * bound["x"])),
                 Soundness.Sound,
-                description: "y / (-a * x) = -(y / (a * x))"));
+                description: "y / (-a * x) = -(y / (a * x))",
+                // Five nodes become seven, for every input: the quotient and the product stay
+                // as they are, the literal is replaced by its magnitude, and the negation round
+                // the whole of it is the two. Measured at +2 on all 84 firings over the corpus.
+                growth: RewriteRuleGrowth.Expands));
 
         /// <summary>
         /// <see cref="Functions.Patterns.BooleanRules"/>, as data.

Sources/AngouriMath/Docs/Contributing/WritingARule.md

@@ -133,7 +133,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 — **262** rules sit at `Unknown` — but declare it where you can justify it:
+honest default — **255** 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,

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

@@ -84,7 +84,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(262, rules.Count(rule => rule.Growth is RewriteRuleGrowth.Unknown),
+            Stated(255, rules.Count(rule => rule.Growth is RewriteRuleGrowth.Unknown),
                 "how many rules sit at Unknown growth");
 
             // And the two the document names. By their own names rather than by what the prose