[Rafael-SOWNet]

#1199 recorded Saturation overshooting a 2 s wall by up to 35×. Now that the perfect-square
collapse (#1201) relies on a 50 ms budget inside Simplify, a budget that can be overshot is the
most important thing the graph work left open. This closes it, with the cause measured rather
than the one I guessed in the issue.

Where the time went

Instrumenting the loop on the worst input, three layers down:

layer	finding
the saturation loop	99% in TryEMatchApply; Extract, Rebuild, Apply, Add ≈ 1% together
one attempt	1,918 ms on a thirteen-member class, returning on its first binding
that binding's steps	the whole 1,918 ms in one graph.Extract of one bound class, on a 253-node graph

The walk was top-down with a visiting cycle guard and a memo that fills only on completion. A
graph full of union-made cycles defeats that: any class on the stack blocks memoisation of
everything beneath it, so sibling paths walk the same subgraph again and again — exponential in
practice. My guess in #1199 (the ledger not consulted often enough) was wrong: Spend() reads
the clock every call; the problem was a single un-spendable 1.9 s step.

The fix

• Extraction is a fixed point from the leaves up: a round recomputes every class from its
  children's current best, in class order and member order so ties fall as they did, until a
  round changes nothing. No recursion, so no depth guard and no stack to exhaust — a chain 300
  deep extracts as itself where it came back null (the test that pinned the null is rewritten
  to say so). The result is kept while the graph is unchanged and the cost is the same delegate;
  only a union can change what an existing class extracts as, so Union drops it.
• The e-matcher charges the ledger per binding tried after the first, so an attempt over a
  thousand-member class is a thousand steps, not one.

Measured

Same inputs, same budget (20,000 steps / 2 s):

	before	after
x / x * x * 1/2 total	2,435 ms	2,000 ms
x / x * -x total	2,595 ms	2,000 ms
longest single attempt	1,918 ms	4 ms
longest single extraction	1,918 ms	3 ms

Every Transformations pin holds — the corpus figures, the safe-ceiling 2-of-5, the ablation,
the breadth, the canonical-extraction ties.

A correction of my own

With extraction no longer the cost, the inputs #1200 called a stall are two things:
x ^ 2 / x, x / x * -x and x / x * x * 1/2 are genuine runaways (10–12k e-nodes in 30 s,
~400 a second), and 2 * x * 1/2 and its relatives plateau at ~560 e-nodes and stop only when
200,000 steps run out. "Bounded at 135–583 e-nodes after thirty seconds" was the slow extraction,
not the graph. ConstantFoldTest says so now and its pin is renamed to what it pins — bounded by
the budget, extracting right. #1200 gets the corrected figures.

Changed answers

None, measured on a build of master (0285c71a) and of this branch through the public
Transformation.CanonicalizationOverGraph and Saturation.ProvesEqual: the 300-deep chain is
300 + x on both (the rule pass on either side of the graph folds it before the graph sees it, so
the old null never reached a caller), x / x * -x is -x and x ^ 2 / x is x on both, and
the two perfect-square proofs succeed on both at 50 ms. What changed is the clock: x ^ 2 / x
against a 2 s budget took 2,216 ms on master and 2,006 ms here. No BREAKING-CHANGES.md row,
since no value moved.

Part of #746. Fixes #1199.

Checks

Full suite 9610 passed, 0 failed, 14 skipped.

🤖 Generated with Claude Code

https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura