RewriteRules.Common does not terminate: a three-cycle on -x * 1/2

[Rafael-SOWNet]

RewriteRules.Common iterated on -x * 1/2 never reaches a fixed point, with or without the
normalisation between passes. Found by a new test that puts #746 tier 2's "termination checked by
tooling rather than asserted by authors" into the build rather than into a workspace harness.

The cycle

Printed forms are not enough to see it — two of the three trees print the same string — so this is
the shape:

0: -x * 1 / 2   Divf(Mulf(Mulf(-1, x), 1), 2)
1: -1/2 * x     Mulf(-1/2, x)
2: -x / 2       Mulf(-1, Divf(x, 2))
3: -x / 2       Divf(Mulf(-1, x), 2)
4: -1/2 * x     Mulf(-1/2, x)      <- step 1 again

So the cycle proper is

Mulf(-1/2, x)  ->  Mulf(-1, Divf(x, 2))  ->  Divf(Mulf(-1, x), 2)  ->  Mulf(-1/2, x)

three distinct trees printing as two distinct strings. Each step is Common.ApplyOnce(...) followed
by .InnerSimplified, which is how Simplificator runs the set.

ApplyOnce is deterministic — -x / 2 parsed fresh always rewrites to -1/2 * x. The apparent
non-determinism in a printed trace is only the two trees at steps 2 and 3 sharing a string.

What it does and does not break

Simplify does not hang: it bounds its own iteration, and "-x * 1/2".Simplify() is
-1/2 * x in about 40 ms. So this is not a user-visible defect today.

It matters because tier 2 makes rule sets first-class data that a caller may apply on its own, and
Common is not a terminating rewrite system on its own. Two rules disagree about which of
c * x and (c * x) / d is the destination, and nothing records that the orientation is a choice.

Why it was not found before

work/rulecheck has measured termination for a while and reports Power and NumericNeat as
settling only in composition. Its corpus has no unary shape applied to a compound expression, so
-x * 1/2 is not in it. The corpus was the limit, not the check.

Not fixed here

Choosing an orientation changes the output shape of a set that runs on nearly every simplification,
and CanonicalOrderExact and the normalisation already interact in ways that have been surprising
before. That is a deliberate decision rather than a patch, so this is filed rather than fixed.

The new test names Common in a list of known non-terminating sets and asserts the list in both
directions, so a set that starts cycling fails and a set that stops cycling has to leave the list.

[Rafael-SOWNet]

The three arms are identified, and the normalisation is not one of them.

Applying Common without InnerSimplified between passes reproduces the cycle unchanged, so the
normalisation is a bystander here — every step is a pure Common rewrite:

1: -1/2 * x   Mulf(-1/2, x)          -> raw  Mulf(-1, Divf(x, 2))
2: -x / 2     Mulf(-1, Divf(x, 2))   -> raw  Divf(Mulf(-1, x), 2)
3: -x / 2     Divf(Mulf(-1, x), 2)   -> raw  Mulf(-1/2, x)

Each rewrite was attributed by asking every addressable rule in RewriteRules.Common.Rules which
one reproduces the observed output — which is what the arm-level registry is for, and is the only
reason this can be named rather than guessed at:

step	arm	rule
-1/2 * x → -(x / 2)	CommonRules:237	Mulf(Rational(var mOne, var den), var any1) => -(any1 / den)
-(x / 2) → (-1 * x) / 2	CommonRules:88	Mulf(var any1, Divf(var any2, var any3)) => any1 * any2 / any3
(-1 * x) / 2 → -1/2 * x	CommonRules:82	Divf(Mulf(Number const1, var any1), Number const2) => const1 / const2 * any1

Reading the arm order in the source would have got this wrong: CommonRules:19 is
Divf(Mulf(Number const1, var any1), var any2) => const1 * (any1 / any2), sits far above
CommonRules:82, and matches the third shape — it is simply not the arm that fires. That was worth
finding out by measurement rather than by reading.

The orientation is not undetermined; it is specified and unimplemented. Docs/Contributing/CanonicalForm.md
§4 gives Mulf's canonical form as "flat, ordered, numeric factors folded into one leading factor",
which makes Mulf(-1/2, x) the canonical member of the three and CommonRules:237 the arm pointing
away from it. So the question is not which of the three is the destination — the specification
already answers that — but whether Common may stop offering the quotient form at all, given that
237 and its three neighbours (234–238) exist so that x / 2 is printed rather than 1/2 * x.

That is a printed-output change across a wide surface rather than a rule fix, which is why this
stays open rather than being closed by a patch.