The perfect-square collapse asks the rewrite graph before it asks Simplify

[Rafael-SOWNet]

#746 tier 2's last open item is a production caller for the rewrite graph, with the standing
performance condition measured. #1198 measured the graph on the corpus and found it cheap and never
ahead of Simplify on extraction — so the caller worth having is one that needs the graph's
proof, not its form. The library has exactly one place that decides an equality by subtracting
and simplifying: the perfect-square collapse, whose remark calls that test "the whole cost of this
rule".

What changes

After the numeric pre-filter passes, the collapse asks Saturation.ProvesEqual(crossTerm, w)
first, at the safe ceiling, under 2,000 steps / 50 ms, and falls through to the three Simplify
calls only where the graph does not prove. A false from the graph is "not proved", never
"unequal", so nothing the site reached before is lost, and the numeric disposer at the end treats
both routes the same. Saturation.SafeRules is the rule list built once, lazily; the catalogue's
private copy reads it.

Measured, per stage

cross term vs candidate	graph	symbolic test it replaces	whole collapse	whole Simplify
2·√2·√3 vs 2·√6	proved, 0.55 ms	1.67 ms	3.1 ms	1.3 ms
2·√a·√b vs itself	proved, 0 ms	3.29 ms	163 ms	48 ms
2·√x·√y vs 2·√(xy)	not proved, 0.24 ms — correctly: the branch-cut identity	2.85 ms	19 ms	37 ms
2·√1·√(x/2) vs √(2x)	not proved, 0.24 ms	5.14 ms	50 ms	59 ms

So: where the graph proves it is 3–6× faster than what it replaces; where it doesn't it costs
0.24 ms; and at the level of a whole Simplify the change is inside the noise (before/after
medians over 15 runs: 52.4 → 50.5 ms, 60.4 → 60.2, 46.9 → 46.3), because the collapse's cost is
in the candidate's own Simplify and the numeric checks, not in the equality test. This is a
caller that meets the condition — it runs only after the numeric pre-filter, bounded — and not a
speed-up to advertise. What made the proved case reachable at all is #1198's constant fold
(2·3 → 6 inside the graph).

PerfectSquareProofTest pins the two facts the caller rests on — the graph proves the surd
product; it refuses √x·√y = √(xy), so a loosened guard fails there before it reaches the rule
— and that the collapse answers exactly what it answered.

Part of #746. With this, tier 2's list from the session stands at: items 1–4 done, item 5 has its
first caller; what remains is the e-matcher over the 35 two-sided rules (EMatching.md), which
changes speed rather than reach.

Checks

Full suite 9610 passed, 0 failed, 14 skipped — 9 of them new.

🤖 Generated with Claude Code

https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura