Make the open-theory shared learned-clause limit executable and fixed-work safe

[rasros]

What

Route an explicit shared learned-clause limit, a reduction cadence, and a counted shared-decision allowance
into open-theory search. ComponentPlan.search currently constructs the session with default
SearchLearnedDbParams, OpenTheoryEngine.solve uses SearchRestart.Never, and reduceLearnedDb runs only
at a restart, so max-learned cannot reduce the shared store on the QF_IDL route that exercises it.

Use the frozen DTP s9, s12, and s18 instances from #1631 for an equal-decision comparison. Record
decisions-to-verdict, peak retained clauses, dropped clauses, and learned watch visits. A bounded policy
must preserve verdict soundness and must not reduce the number of completed instances at equal work.

Why

#1631 measured clause policies through experiment-only wiring and found policy-sensitive tradeoffs; it did
not establish that standard activity retention is unsound or generally unhelpful. The production limit remains
unreachable on the only measured shared-store consumer. Until the route and reduction boundary are wired, the
configured cap is not an executable policy and cannot be evaluated safely.

[rasros]

The corrected #1631 fixed-work report, including the false-UNSAT boundary and production-wiring prerequisite, is archived in the public #1557 evidence gist.

[rasros]

A self-contained cheaper-model implementation/PR handoff is archived as klause-1768-cheap-model-handoff.md in the public #1557 evidence gist. It corrects the stale activity conclusion, specifies production parameters and the sibling-budget regression, and requires #1771 to merge first.

[rasros]

The public handoff was refreshed after #1787: sibling-budget handling is an already-landed invariant, not work to reimplement. #1793 is the final accounting cleanup prerequisite; it corrects poll telemetry and the published event classification without changing openWork.

[rasros]

Implemented in #1811. The frozen DTP raw evidence is public at https://gist.github.com/rasros/4d1afd6470eecb34428c9cb2dc1548ed. Every arm used fresh JVMs, presolve off, max-decisions=50000, and shared-restart=1000; s9 was SAT while s12 and s18 were budget unknown, never false UNSAT. Caps 500, 1000, and 2000 all executed reductions and dropped clauses. #1631 remains open: this PR wires the current LBD-plus-use controls and does not accept or reject learned-clause activity.