A canonicalisation framework on the rewrite graph

[Rafael-SOWNet]

#746 tier 2 asks for "a canonicalisation framework built on" the rewrite graph. This is that:
Transformation.CanonicalizationOverGraph(budget, widest) saturates under a rule set, then extracts
the least member of the root class under a total order.

Offered, not applied. CanonicalForm.md §8 says wiring a canonical form into Simplify is a release
decision of its own, and this does not take it.

The order is the piece that had to be new

A cost model answers "which is nicer" with a double, so two forms it cannot separate tie — and a
tie is settled by whichever was reached first, an accident of traversal. A canonical form cannot be
built on that. No double carries a total order on trees, so EntityOrder.Canonical is a comparison:

• size first, so the representative is the smallest member and canonicalising never enlarges;
• then structural, so it is total up to Equals.

Deliberately not the printed form — (x + y) + a and x + (y + a) print alike and are different
trees. Deliberately not Entity.SortHash, which orders operands within a commutative chain: a
different question, and the two do not compete.

EGraph.ExtractLeast is the same walk as Extract choosing by an order instead of a number. They
share one recursion rather than two copies of a subtle one, over a struct selector under a generic
constraint — compiled in rather than dispatched, and no selection allocated per class.

The saturation loop moves to Saturation.Run, shared with EqualitySaturation. Two transformations
wanting it is the reason: they differ only in what they extract, not in what is charged, which rules
can be skipped unattempted, or which matching path a rule takes.

Three things measured, two of which corrected what I had assumed

The safe rules are already confluent, so over that ceiling a graph earns nothing. Two rewrite
chains run from each of 1458 generated expressions produced no divergent pair at all under
Collects and Rearranges. A rule pass already reaches the form a graph would.

The growth ceiling is a much smaller knob than it looks. Of the sound rules in MatchedRules:

growth	rules
Collects	26
Rearranges	17
Expands	9
Unknown	270

Those 270 are unjudged because their replacement is code rather than a written pattern, so nothing
counted it. Over six expression pairs equal only through a larger intermediate form:

ceiling	proves
Rearranges	2 / 6
Expands — all nine expanding rules added	2 / 6, the same two
Unknown	3 / 6

So the dial that matters is not how far a rule may enlarge; it is whether rules nobody classified may
fire at all. Unknown is therefore the widest stop rather than an excluded value — refusing it
refuses 84% of the library — and naming it as the widest setting makes it a request a caller has to
make on purpose. The default stays narrow, because the widest setting is where the harness's 7,147×
blow-up lives.

And the graph does not sort commutative operands. The rules that do are among the 270, so no
ceiling below the widest admits them, and x + y and y + x canonicalised to themselves.
Transformation.Canonicalization already sorts and flattens and is already measured idempotent, so it
runs on each side of the graph step rather than being written again.

ProvesEqual is the half to rely on, and it is not a transformation

Bringing two expressions separately to a canonical form and comparing decides equality only where
the rules are confluent. Otherwise one side reaches a form the other cannot, and two equal
expressions end in different forms having each been canonicalised correctly. Measured, on
(x + y) * (x - y) against x ^ 2 - y ^ 2: the product's graph reaches the difference of squares,
the difference of squares' graph does not reach the product, and the two forms are the same size — so
each canonicalises to itself.

Asking in one graph has no such gap: both are inserted, every equality the rules reach from either
is merged, and the question is whether they ended in one class. That does not depend on confluence,
only on reaching far enough within the budget.

Saturation.ProvesEqual is internal here. It wants a public home and a name chosen by someone who
owns the surface.

Tests

43 new, in CanonicalExtractionTest: the order's totality and antisymmetry, that extraction never
enlarges, idempotence of the composed transformation, the budget being respected and reported, and the
confluence gap above as an explicit expectation rather than a surprise.

Full suite on this branch, rebased onto master after #1104: 8962 passed, 14 skipped, 0 failed.

Part of #746 tier 2.