The e-graph is a congruence closure and nothing can ask it whether two expressions are equal

Measured on `2dbeedf7`.

`EGraph` is `internal sealed` and is a congruence closure — `Find`, `Merge`, e-classes — with `Saturation` over it, a `WorkBudget` bounding it and pluggable extraction. It is reachable publicly only as a *simplifier*, `Transformation.EqualitySaturation(budget, costModel)`, which saturates and then extracts one representative.

The question it could answer and is never asked is **whether two expressions are equal**: put `a` and `b` in one graph, saturate under a rule set, and report whether they landed in the same class.

That is not the same question as `a.Simplify() == b.Simplify()`. Two expressions can be equal under the rule set without either reaching a common normal form — simplification picks one representative per input by cost, and the two searches can settle in different places while the classes have already merged. The e-graph merges the classes whether or not extraction would agree.

What the public surface has today is neither:

* `MathS.UnsafeAndInternal.AreEqualNumerically(a, b)` — sampling. Evidence, not a proof, and named accordingly.
* `Matrix.EntityTensorWrapperOperations.AreEqual(a, b)` — structural, on the tensor wrapper.

### Why it seems worth doing

* It is a **decision procedure over the rule set**, which is a different capability from the whole `Simplify` pipeline rather than a convenience over it.
* It is a **verifier**. #746's design principle 6 argues explicitly that "language models are strong proposers and weak verifiers; the platform must be the verifier", and that a design choice making verification cheap is worth more than one making generation slightly better. A cheap `AreEqual` is the smallest instance of that.
* Tier 3 (the theorem graph) is recorded as "not started", and this is its cheapest entry point — an equality oracle over a rule set is the thing a fact database would be queried through.
* The soundness metadata already lets the answer be qualified: `Saturation` knows which rules fired, and rules declare `Sound` vs `SoundUnderAssumptions`, so "equal, using only sound rules" and "equal, using conditional ones" are distinguishable rather than one boolean.

### Questions rather than a design

* Where should it live — `MathS.AreEqual(a, b, budget)`, or on `Entity`?
* What is the third answer? Saturation runs to a budget, so the honest result is three-valued: *equal*, *not shown equal within the budget*, *budget exhausted* — and #1036 is precedent for not spelling a resource limit the same as a mathematical negative. `BudgetOutcome` already exists to carry the third.
* Should it report the weakest soundness used, the way `DerivationPath` takes the weakest across a step?
* Is `EGraph` cheap enough to make this worth calling, given `EqualitySaturationReviewFindings.md` recommended against running `Simplify` on the graph by default? The recommendation was about the default simplification path; an explicitly-invoked equality query is a different cost question and should be measured on its own rather than inherited.

Part of #746, tier 3.

Start by reading EGraph, Saturation, and BudgetOutcome, then compare the guidance in EqualitySaturationReviewFindings.md and issue #1036. Done requires resolving where the public equality query lives, how budget and soundness outcomes are represented, and measuring its cost separately from default simplification.

Written by the indexing model from the issue text.