Rule priorities, computed from the patterns rather than typed

[Rafael-SOWNet]

#746 tier 2 asks for "rule priorities and conflict resolution, with confluence and termination
checked by tooling rather than asserted by authors". This is the priorities half;
RuleConfluenceTest was already the confluence half.

A rule set is first-match-wins, so where two rules fire at one node and disagree, whichever is
tried first decides the answer — and until now that was where somebody typed it.

The one place it is written down is a comment on MatchedRules.CollapseMultipleFractions: the set
"is order-dependent, since Mulf(Divf, Divf) has to be tried before Mulf(a, Divf) or the more
general rule would swallow the special one". That is subsumption, observed by hand and then
maintained by hand.

MatchPattern.Subsumes

A matching problem, not a size comparison. A hole repeated across a pattern is an equality
constraint, so Mulf(a, a) matches strictly less than Mulf(a, b) while having the same node
count — comparing NodeCount would call those two equally general and get the ordering wrong in
the one case the ordering exists for. So this matches one pattern against the other as a term,
carrying an assignment from the wider pattern's holes to the narrower one's subpatterns and requiring
a repeated hole to be assigned consistently.

Sound in one direction only. true is a structural claim about every expression; false means not
proved, never disproved — a hole carrying a predicate is arbitrary code, an Exact literal can be
equal to a value of another runtime type (a rational that reduced to an integer), and an n-ary
Gathered pattern matches a family this does not attempt to reason about. Each refuses, and leaves
the pair ordered as written, which is what the code did before.

MatchedRuleSet.RulesByPriority applies it as a stable topological sort: no rule is tried before a
rule its pattern subsumes, declaration order everywhere else.

Four things measured

Subsumption does not lie. Over all 322 rules — the relation is about patterns, and nothing about
it stops at a set boundary — 961 ordered pairs claim it, 513 are put to the test by the
corpus containing something the narrower pattern matches, and none is contradicted across 56,892
nodes. The count of witnessed claims is asserted as well, so a corpus that stopped reaching these
shapes cannot quietly turn that into a test which passes by asking nothing.

It changes no answer today. Of the 5,480 within-set rule pairs, subsumption has an opinion about
28, and in every one the specific rule is already declared first. None is mutual.

set	pairs
InequalityEquality	8
Boolean	6
CollapseMultipleFractions	4
CollapseTrigonometricFunctions, Common, ExpandFactorialDivisions, FactorizeFactorialMultiplications, Power	2 each

So this orders what was already ordered. What it adds is that inserting a general rule above a
specific one no longer silently reverses an answer — and one of those eight sets says anything about
it in its own documentation, which is the argument for computing it rather than writing it down.
RulePriorityTest holds the two orders equal, so the file stays readable as well as correct.

The existing confluence corpus cannot see any of it. RuleConfluenceTest grows its third level
with unary shapes only, so it never builds a quotient of quotients or a product of quotients — which
is exactly where a special rule and the general rule that would swallow it meet. On that corpus
none of the 28 pairs overlaps at all. Growing the third level with binary shapes too takes the
conflicts from 3 to 45:

• 6 settled by priority — a general and a special case of one rewrite meeting on a nested
  quotient, four of them the pair CollapseMultipleFractions describes in prose;
• 39 where neither pattern subsumes the other, so the answer is decided by which was written
  first and by nothing else.

Those 39 are recorded by name. The data rules have names, which is what the note on
AConflictIsReportableAsThePatternsItIsBetween asks for — "the failure message has to name the
arms, not their indices — an index moves whenever somebody edits the switch, which is exactly when
this test fires" — and what a switch arm cannot supply. None of the 39 changes what Simplify
returns; the normalisation and the passes after it converge.

And one test asserted the opposite of this. TheOrderOfTheRulesIsLoadBearing built the set with
its rules reversed and required the general rule to swallow the special one. It does not any more,
which is the whole point, and the test's own comment gave the reason: a switch gets its ordering
"by accident of being written top to bottom", and an accident is what an ordered list of values
does not have to inherit. Replaced by two — the specific rule wins however the set is written,
and where neither rule subsumes the other the order still decides everything.

One thing the classification surfaced and this leaves alone

quotient-of-two-quotients answers 0 where the general rule answers NaN, on
x / (1/2) / (1 / 0). Left alone deliberately: Simplify returns NaN for that input, priority
picks the same arm the declared order already picked so nothing here changes it, and the missing
hypothesis is what Soundness.SoundUnderAssumptions on that rule is declaring. Recorded because the
tooling found it, not because this PR fixes it.

State

No public API change. Full suite on this branch: 8925 passed, 14 skipped, 0 failed.

Independent of #1105 — the two touch no file in common and can merge in either order.

Part of #746 tier 2.