Solving a system is bounded whichever internal path takes it (#896)

[Rafael-SOWNet]

Closes #896.

The issue left the choice open between three options, and said option 3 "rests on an assumption that ... is not measured". I took that measurement first, and it turned out to settle the whole thing.

The measurement

The worry about bounding the fall-through was that it would cost the systems the fast path declines for reasons unrelated to difficulty — five uncoupled quartics with 1024 solutions, above the quotient-dimension cap, which the elimination answers cheaply.

system	Gröbner	time before handing over
a^4-1 … e^4-1 uncoupled — must not regress	declined	8 ms
cyclic-4	declined	3 ms
cyclic-5	declined	7569 ms

8 milliseconds. So a whole-call bound leaves the elimination essentially all of it, and that case survives untouched — it still answers 1024 solutions. Option 1 was never the threat it looked like, and option 3's exit-reason discrimination isn't needed: a shared budget discriminates by construction, since a fast decline leaves the budget nearly full and a slow one does not.

Two things I got wrong on the way, both caught by measuring

1. Sharing the BudgetLedger itself is wrong. The Gröbner path uses one mechanism for a genuine resource ceiling and for a structural refusal like "not polynomial", and a ledger that has recorded any ceiling refuses every later spend. So sharing it read "declined in 8 ms because the system is uncoupled" as "the budget is gone" — and the 1024-solution case raised instead of answering. What crosses the boundary is the clock, not the ledger.

2. A wall-clock bound is flaky, and a step bound is incomplete. The clock version passed in isolation and failed inside the full suite: under parallel load the good case exceeded five seconds and was cut off. A bound that makes the same system answer or decline depending on what else the machine is doing is a worse failure than a slow answer.

But steps alone don't bound cost either — cyclic-4 spends 4946 ms in eight branches.

So the default carries both, sized from measurement

A step is one candidate solution explored, which is what compounds: each elimination turns the next level's coefficients into nested radicals.

system	branches explored
symbolic 2×2	2
cyclic-4	8
a^4-1 ×5, the largest that answers	341
cyclic-5	>100 000, did not finish in 40 minutes

Steps = 10_000 — thirtyfold headroom over anything known to work, and far below the runaways. Time = 60s as a loose backstop for the arbitrarily-expensive single step.

The honest limitation

The bound is cooperative and checked once per branch, so a call can overshoot by the cost of the branch that was running when the budget ran out. Cyclic-6 returns in about two minutes, where before it did not return at all. That is BudgetLedger's stated design — an algorithm that does not ask cannot be bounded, and a bound enforced from outside is a thread abort in the middle of a rewrite. It is a bound where there was none, not a tight one.

Cyclic-6 is deliberately not in the test suite: two minutes is two minutes on every run, and even a ceiling of twenty takes half an hour on it, because its branches are individually enormous. The mechanism is demonstrated instead by a system the elimination answers in two candidates, which declines under a ceiling of one in milliseconds. Its own measurement is recorded in BREAKING-CHANGES.md.

Behaviour

	before	now
cyclic-6	exceeded 20 s, unbounded	declines, returns in ~2 min
a^4-1 ×5 (1024 solutions)	answers	unchanged
cyclic-4 (158 solutions)	answers	unchanged
every ordinary system	answers, fast	unchanged
Budget set below what the solve needs	answered anyway	raises

BudgetTest.ExhaustionDoesNotChangeTheAnswer asserted the old promise — that exhausting the bounded path left the answer alone because the caller carried on regardless. That promise is exactly what this changes, so it is split into the two that are now true: a budget not reached changes nothing, and a budget reached bounds the whole call.

A recording now also sees two outcomes per solve rather than one, named Gröbner and SolveSystem, so what stopped each is separately visible — which the issue notes a caller previously could not find out.

Failed: 0, Passed: 9136, Skipped: 14 locally on net10.0, with suite time unchanged.

🤖 Generated with Claude Code

https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura

[Rafael-SOWNet]

Merged master in for #1129's BREAKING-CHANGES.md and .editorconfig — both append-only, resolved keeping both sides, and the diff against master is now purely additive.

One extra commit, and it is worth reading before the rest. OneSidedLimitTest.ADifferenceOfReciprocalLogarithms started failing about two runs in three on the integration branch while passing every time in isolation. The obvious suspect was this PR's own budget, so I measured it rather than assuming:

	with the new budget	without
the limit, three runs each	6906 / 6908 / 6924 ms	6970 / 6896 / 6917 ms

Identical. The budget never fires there. The test wraps its limit in task.Wait(60s) — a wall clock in a parallel suite, guarding work that costs about seven seconds — and this branch adding nine tests was enough to tip it. The guard is widened to three minutes, which still catches a hang in a suite that takes seven, with the measurement in the comment.

Full suite green twice on the merged tree: Failed: 0, Passed: 9195, Skipped: 14.