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

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. Goal: Math OS — a ten-year vision for AngouriMath as an open mathematical reasoning platform #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 Giving up on a resource is spelled the same as a mathematical negative #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.