Seventy-one rules say how they change the size of what they match (#1161)

Seventy-one rules say how they change the size of what they match

Growth is `Unknown` for a code replacement unless it is declared, and 261 rules
sat there. Seventy-one can say what they do, each argued by counting the pattern
against the replacement in terms of the holes, and each checked against the
generated corpus as well.

The arguments fall into a few shapes. Operators mapping one for one with every
hole used once rearranges: the quotient re-associations, (a^n)^m = a^(n*m), the
negation-literal swaps, log(a, b^n) = n * log(a, b), the inverse reciprocals,
and the even parity rules. A hole matched twice and written once collects by
-(1 + |a|), which is stronger than the corpus shows since the corpus fills its
holes with single nodes: the power-merging rules, k*p +- k*q, and the two that
gather logarithms of one base. A replacement holding no hole at all collects by
the whole pattern: the trigonometric identities that become 1 or pi/2. And the
odd parity rules expand by exactly the two nodes of the negation they add.

The seven equals rules of the drops-out family are declared where their thirty-
odd comparison siblings are not, and the difference is the one the comment on
`a-equals-with-zero-on-the-left-turns-round` already recorded: `EqualTo` is a
bare `Equalsf` and does not chain the way the comparison operators do. Reading
that as "the comparison rules are hopeless" rather than "`EqualTo` is the safe
one" had left seven declarable rules undeclared.

WritingARule.md now carries the shapes that are declarable and the four that
look declarable and are not -- a replacement built with the chaining comparison
operators, one that attaches a Provided sized by its operands, a hole that can
be filled by two spellings of one thing, and a repeated hole that gets squared.
Each of those measures a clean constant delta over the corpus and is false
anyway; each was found by walking into it.

Two rules are left undeclared with the reason beside them rather than silently.
The boolean distributions count plainly as -(1 + |k|), and declaring one is what
makes equality saturation fire it -- which it never has, since RulesUpTo builds
its set as the rules up to Rearranges. Fired, it takes `a and b or a and not b`
to `a and (b or not b)` and the value moves at 0.37. That is a defect in a rule
marked Sound, filed as #1162, and the general lesson of the batch: a growth
declaration moves a rule into the set saturation runs, so it can expose a rule
whose soundness was wrong all along.

MostSoundRulesHaveNoJudgedGrowth is re-pinned at "not the majority" rather than
"under a quarter", since the share is meant to rise while #825 lands.

Full suite 9552 passed, 0 failed on the earlier commits; the later batches are
verified by the targeted tests -- the growth check, the census, the canonical
extraction and every transformation test including
EqualitySaturationNeverChangesTheValueItClaimsToPreserve -- and by CI here.

Part of #825.

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

Author: Rafael-SOWNet