A factor of -1 is a sign, not a factor to take out (#1167)

[Rafael-SOWNet]

Two things, on one branch because the second is what found the first.

A factor of -1 is a sign, not a factor to take out

Four rules bring a negative factor out of a numerator or a denominator. Given a magnitude of 1 they
took it out anyway, leaving the 1 behind as a literal 1 * factor that says nothing — and the
numerator rule and the denominator rule then undid each other around it. NumericNeat applied to
-x / (-y) grows by four nodes a pass and never reaches a fixed point.

They now decline a factor of -1, which is not a factor to take out but the sign the rewrite is
about; the two rules directly above them, (-a) * (-b) = a * b and (-a) / (-b) = a / b, already
answer that case. Closes #1167.

Both spellings changed together — the four MatchedRules and the eight switch arms in
Patterns.Common.cs that carry the same rules with their commutative variants. Twenty-seven of the
thirty sets no longer run their switch, but the agreement tests still hold the two forms to each
other.

The corpus that had to find it

RuleSetsDoNotCycleTest ran on hand-written seeds — shapes somebody thought of — and -x / (-y) was
in that list only because #1056 had already put it there. A check that confirms the last bug is not
the same as one that finds the next.

It now also generates the arithmetic grammar the growth check uses: nine leaves, seven unary and five
binary shapes, composed two and three deep and sampled at the third level.

It found the next one on its first run. #1171: Power contains an inverse pair —
two-powers-of-one-exponent-share-a-base collects a ^ b * c ^ b into (a * c) ^ b and
positive-power-of-a-product-distributes takes it straight back — so applying the set to a fixed
point alternates for ever:

Power: 1 ^ (-2) * x ^ (-2)    ->  (1 * x) ^ (-2)      ->  1 ^ (-2) * x ^ (-2)
Power: (-2) ^ 2 * (1/2) ^ 2   ->  ((-2) * 1/2) ^ 2    ->  (-2) ^ 2 * (1/2) ^ 2

Not fixed here, deliberately. Neither rule is wrong and each is wanted in its own direction; a
set holding both has no normal form to reach, and which of the three possible answers is right is a
decision about normal forms rather than a bug fix. Both loops are pinned by name with the issue.

Simplify is unaffected, and that was measured rather than assumed: 1 ^ (-2) * x ^ (-2) answers
1 / x ^ 2 and (-2) ^ 2 * (1/2) ^ 2 answers 1. The pipeline folds between passes, so 1 * x
collapses and the shape the second rule needs stops existing. What makes the cycle visible is
applying the set alone, which is what the transformation layer lets a caller do.

Both known-lists assert in the other direction

A pinned loop that stops happening fails the test, so a fix deletes the entry rather than leaving a
loop written out that no longer occurs. NumericNeat's entry is gone by exactly that route — the
#1167 fix made the test demand its deletion.

Three recorded verdicts moved, each because the fix worked

• RuleSetTerminationTest listed NumericNeat among the sets that settle only once the
  normalisation runs between passes — and its remark named the reason exactly: "rewrites --x
  through a product of ones that only collapses when the normalisation multiplies them out". That
  product of ones is the 1 * this fix stops making. It settles alone now and has left the list.
• RulePriorityTest recorded two conflicts left to declaration order in NumericNeat, one of
  them the numerator-and-denominator pair itself. Both are gone.
• That test's corpus had -1 as its only negative leaf, which is the one case these rules now
  exclude — so they matched nothing at all and the subsumption claims about them went unwitnessed.
  -2 is a leaf now.

Measured four ways rather than assumed, because the count moved in a way that looks like lost
coverage and mostly is not:

corpus	guard	witnessed
old leaves	off	513
old leaves	on	489
-2 added	off	501
-2 added	on	501

With -2 present the guard costs nothing — that is what says the leaf restores exactly what the
guard removed. The residual 513→501 is not coverage at all: level3 samples every eleventh element
of level2, so a longer level2 lands the sample on different expressions.

The corpus size is asserted alongside the witnessed count now. A coverage number means nothing
without what it was measured over, and both figures were prose in a remark that nothing held to
them.

A note added to InversePairTable.md

That document is about why the inverse-pair table cannot be derived, from syntax or from
MatchPattern. There is a third source it did not consider: run the sets and watch what comes
back. It is a lower bound rather than an enumeration — a pair that never fires is invisible to it,
and a pair split across two sets never meets — but it needs no reversibility mechanism at all, and it
answers the question equality saturation actually asks, which is which rewrites undo each other so
that it stops.

Checks

Full suite 9558 passed, 0 failed, 14 skipped — measured after rebasing onto #1170.

🤖 Generated with Claude Code

https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura