A rule's declared growth is checked against the corpus (#825)

[Rafael-SOWNet]

RewriteRuleGrowth is a claim about every expression a rule fires on: Collects says the
replacement is smaller, Rearranges the same size, Expands larger. For the 35 rules with a
pattern on both sides it is counted from the two patterns. For the rest it is declared by hand, and
nothing checked it.

Running those declarations against the generated corpus finds one that is wrong.

The one it caught

a-common-factor-is-collected-out-of-a-whole-sum declared Collects, and the reason was in the
code:

// Declared, because the replacement is code and nothing counts it: the whole point of it is to be smaller.
growth: RewriteRuleGrowth.Collects));

Over fourteen hundred expressions it fires 42 times, never shrinks, and grows by as much as eight
nodes:

-x + x + -1/2   ->   x * (-1 + 1) + -1/2         seven nodes for seven

Which of the four is true, checked rather than chosen: Collects wants every firing smaller and a
delta of 0 refutes it; Rearranges wants every one the same size and +8 refutes it; Expands wants
every one bigger and 0 refutes it. Unknown is the only one left, and that is what it now says,
with the counterexample recorded next to it.

Why this is not documentation

Saturation.RulesUpTo selects by growth. A rule saying Collects or Rearranges is one equality
saturation fires; one left at Unknown is one it does not. So that rule has been in SafeRules on
a claim nobody tested, and a declaration wrong in the shrinking direction tells the saturation a
rewrite is safe to run when nobody established it.

That also means the 262 undeclared rules are not a documentation backlog. Each declaration is a
behavioural change, which is why this PR adds the check and no new declarations.

What is deliberately not done

The rule is not made to collect for real. Declining where it does not shrink would make
Collects true, but that changes what the rule does rather than what it says about itself — and
x * (-1 + 1) folding to zero looks like how -x + x reaches 0, so it would have to be
established that the step is not load-bearing first. Separate change, separate measurement.

What the corpus can and cannot say

It can only refute. Firing on fourteen hundred expressions without contradicting a claim is
evidence for it, not proof, since the claim is about every expression there is. So the test fails on
a contradiction and says nothing about a rule it could not make fire — and the doc now says the same
to anyone declaring one.

84 rules reach the corpus, 18 of them carrying a declaration, and the test asserts both counts so
that it cannot pass by never running.

The other 66

They are the measured evidence for declaring more, and — the useful part — the measurement separates
the ones that can be declared from the ones that cannot:

observed	rule
+2 on all 84 firings	a-negative-factor-in-a-denominator-comes-out
-2 on all firings	two-powers-of-one-base-multiply-by-adding-exponents
0 on all 84 firings	a-thing-times-a-quotient-keeps-the-divisor-outermost
-2 to 0	a-term-added-to-itself-doubles — honestly Unknown
0 to +4	a-sum-chain-is-sorted-and-grouped — honestly Unknown

A declaration still has to be arguable from the code; the corpus is what stops one being a guess,
and what refutes it when it is.

Part of #825.