Forty-three rules say how they change the size of what they match (#825)

[Rafael-SOWNet]

Fifteen rearrange and nine collect. 255 rules were at Unknown; 231 are.

Each is argued from the shape of the replacement, and checked against the corpus as well — the
argument is what licenses the declaration, the corpus is what would refute it.

The rearrangements

Operators map one for one and every hole is used exactly once on both sides:

(a / b) * c = (a * c) / b        a / (b / c) = a * c / b        a / b / c = a / (b * c)
a * (b / c) = (a * b) / c        (a / b) * (c / d) = (a * c) / (b * d)
(a ^ n) ^ m = a ^ (n * m)        a ^ (-1) = 1 / a

and the negation-literal swaps — x + (-a) = x - a, (-a) - (-b) = b - a, (-a) * (-b) = a * b,
(-a) / (-b) = a / b, x - (-a) = x + a, a + (c * b) = a - (-c) * b — where one operator becomes
another and a literal is replaced by its magnitude, one node for one.

The collections

Something matched twice, written once. a ^ n * a ^ m = a ^ (n + m) matches its base twice and
writes it once, so the delta is -(1 + |a|): two nodes for a base of one node, more for a larger
one. The same covers a^n / a^m, a^n * b^n, a^n / b^n and k*p +- k*q = k*(p +- q). And
a + (-1) * b = a - b, where the -1 and its product go entirely.

Something collapsed to a constant. cosec(a) * sin(a), tan(a) * cotan(a) and
sin(a)^2 + cos(a)^2 become the literal 1; arcsin(a) + arccos(a) becomes pi/2. The pattern is
a fixed frame around two copies of the angle and the replacement holds no operand at all, so the
delta is -(k + 2|a|) — at most −2, −4 and −8 respectively, and further the larger the angle.

The corpus reported a flat number for all of these, and the argument is stronger than the
measurement — it saw -2 for the power rules only because the bases it generates are single
nodes. A corpus can refute a claim; it cannot tell you how strong the true one is.

These change what runs

Unlike the seven Expands of #1159, all twenty-four sit inside SafeRules — Saturation.RulesUpTo
builds its set as the rules up to Rearranges — so they join the rules equality saturation fires.

Three left alone, each measuring as cleanly as the ones above

This is the part worth reviewing. All three look declarable from the data and are not.

a-reciprocal-rational-factor-is-a-division — a * (1/c) = a/c, 0 across all 17 firings.
IsWholeReciprocal accepts a rational literal like 1/3, which is one node, and a written 1 / c,
which is three. The delta is 0 in one spelling and −2 in the other.

a and False = False and a or True = True — −2 wherever they fire. But the replacement is not
the constant; it is the constant wrapped in .Provided(a.DomainCondition).Provided(b.DomainCondition),
and a large operand's domain condition can exceed the pattern it replaces.

The fifteen rules that drop a negative divisor or factor out of a comparison with zero — −2 at
every point the corpus reaches, and the pattern count gives -(|k| + |zero|) <= -2. Both said
Collects. Both are wrong: the replacement is built with < or >, which chain, so on
((x > y) / (-2)) > 0 the seven nodes of the pattern become the seven of x > y and y < 0 and the
delta is 0.

That last one is not a near miss — the comment on a-equals-with-zero-on-the-left-turns-round
already records that EqualTo does not chain "the way Equalizes and the comparison operators do",
and its comparison twins were left undeclared for precisely this reason. #1160 adds the shapes that
let the corpus refute it too.

Verification

Full suite 9552 passed, 0 failed, 14 skipped — and green against the wider corpus of #1160,
which exercises 194 rules rather than 84. That is the stronger check of these twenty-four; this PR
does not depend on it and the two touch no file in common.

MostSoundRulesHaveNoJudgedGrowth had to move: it asserted that fewer than a quarter of sound rules
carry a judged growth, and the share went from 69 of 324 to 93. Re-pinned at not the majority,
since the share is meant to rise while #825 lands.

Part of #825.