Three things about a rule that can be measured rather than declared (#825)

[Rafael-SOWNet]

Whether a rule ever fires, whether it changes where its result has a value, and which way it moves
the cost the simplifier selects by.

Each could be a field beside RewriteRuleGrowth, and each would then be one more thing to write down
wrongly. Measuring costs nothing at run time — none of it runs in production — and it cannot go stale
against the rules it describes.

The definedness check finds one

k - k = 0 is declared Sound and assumes k has a value. At x = 0, x^(-2) - x^(-2) is
undefined and 0 is not, so the rewrite invents an answer. Its sibling for the same shape,
a / a = 1, attaches provided a is not zero; this one attaches nothing. Filed as
#1169, pinned here as the one known
exception so a new one fails and so does this one going away.

This is contract obligation O4, which is otherwise only as true as whoever wrote the rule
remembering the Provided.

Asked only of Sound rules, because that tier is what claims nothing is assumed.
SoundUnderAssumptions already says otherwise — a / (b / c) = a * c / b turning NaN into 0 at
c = 0 is a rule saying so, not a defect. Without that scoping the check reported 68 rewrites,
every one of them a declaration being read back.

Two things had to be right before it could see anything

Both were wrong on the first pass, and the check was silently vacuous:

• Zero has to be among the check points. Arithmetic definedness changes where a denominator
  vanishes, a logarithm reaches its pole, a root turns negative. Four comfortable reals ran the whole
  check without ever asking the question it exists to ask.
• NaN is a Number. Testing Evaled is Number calls the undefined case defined. Validated
  by removing the Provided from a / a = 1 — the check did not bite until it asked for a
  finite number.

The cost check says something growth cannot

growth counts nodes; candidate selection uses MathS.Settings.ComplexityCriteria. A rule can
shrink a tree and raise the number that decides whether its answer is taken.

Measured, they agree: rules declared Collects lower the cost far more often than they raise it.
Reported as a comparison rather than asserted to be perfect, because the two measures are allowed to
disagree and where they do it is a fact about the rule rather than a defect.

Hit rate

123 of 324 rules fire on this corpus, asserted as a count that moves. A rule the corpus never fires
is one the checks above say nothing about.

Verification

Full suite 9557 passed, 0 failed, 14 skipped.

Part of #825.