Coordinate recursive proofs within the existing search budget

[samth]

Draft: the full checked case-study build found four scheduling regressions. Do not merge in its current form.

Recursive proofs can exhaust ordinary search before the useful combination of functional induction, interface simplification, and cases at blocked computations is tried. Add a bounded final coordination trial to default search for local or explicitly supplied recursive theories.

The engine reserves at most 256 attempts, capped at one quarter of the caller's total effort; ordinary search runs first. Both phases share the existing attempt ledger, ambient heartbeat limit, rollback, and complete-goal validation. Small budgets and nonrecursive theories retain their full ordinary allowance. The committed mode keeps its existing schedule.

Hooks.postlude supplies the general scheduling interface. Coordination uses the existing critics, moves, and policy callbacks, with stable move enumeration for recorded-plan replay and ordinary-command suggestions. It contains no checkpoint cache or output generalization and is independent of #3.

Validation so far:

• Full lake build and lake test pass on Lean 4.30.0 and 4.33.1.
• Regressions check aggregate accounting, the ambient deadline, failed-state restoration, mandatory siblings, recorded-plan replay, and waterfall? command compilation.
• All six previously observed VProver gains succeed with the original 1,000 total attempts, compared with failures on unmodified main under the same limits.

Full VProver comparison: 31 → 37/156, six gains and no losses/timeouts; aggregate raw heartbeats increase 5.24%. Both arms use 1,000 total attempts and 200 million raw heartbeats. The complete 111-goal panel is unchanged at 99 → 99/111, with no losses, timeouts, or fatal diagnostics; aggregate raw heartbeats increase 0.214%. Its existing hints and 10,000-attempt/800-million-heartbeat budget are unchanged.

The unchanged checked case-study corpus passes on main and fails at four declarations on this PR: select_all_le_of_components, compare_correct, test_der1, and quiz4_answer. Focused controls recover all four by disabling only the final trial, restoring the ordinary allowance within the same 1,000-attempt cap. They need 873, 835, 839, and 980 ordinary attempts respectively, exceeding the reservation's 750-attempt cutoff. All four control files pass.

This isolates the regression to budget scheduling. The reserved trial adds useful proofs, but the activation/reservation policy needs revision before default enablement. The planned 2,777 forced-site comparison is deferred because the candidate fails the checked corpus. No corpus proofs or budgets were adjusted to hide these losses. All measurements use Lean 4.30.0 against main 8d5f164, with exact source/runtime hashes and unchanged benchmark infrastructure.

Full report, exact provenance, and reproducible evidence. The task-owned cluster files have been backed up, verified, and removed.

[samth]

I prototyped removing the 750/250 root split and using one search: a depth-16, strength-2 contour first, with the coordinated moves preferred at each node and every remaining ordinary move offered afterward. Later fair contours remain reachable if budget remains.

This finds all six new VProver proofs in 45–249 total attempts, but is not a strict improvement at the original 1,000-attempt limit. Two of ten previously successful VProver controls now exhaust the budget; PR #4 closes those in 382 and 13 attempts. In the unchanged checked corpus, 11-TrieCaseStudy.lean acquires failures at lines 312 (10,000 attempts) and 457 (1,000 attempts). 12-PriqueueCaseStudy.lean also reports a new exhaustion at line 198 and retains the loss at line 222; I stopped that file after the decisive failures. Starting the deep contour at strength 1 still loses both VProver controls and one of the six gains.

The deep contour reaches the new proofs quickly, but wrong branches can spend the entire finite budget before the shallow contours that find established proofs. Simple root reordering has not resolved the scheduling problem. I would keep this PR draft until one schedule retains the checked corpus and the new gains at the same limits. Prototype patches, exact timers, and the partial corpus log are preserved in the research notes (private).

[samth]

Two independent simplification prototypes look useful even though neither fixes the attempt split:

• Lazy extra moves: cheap descriptors defer blocked-case observation, simp-command construction, and applicability checks until a move is considered. The six new gains and ten previously successful VProver controls all retain identical attempt and node counts; aggregate raw heartbeats fall 3.47% across those 16 goals. lake test, recorded-plan replay, and checked suggestion rendering pass. The prototype changes draft action ordinals for some extra moves, so stored plans would need migration if those ordinals have escaped this PR.
• Simpler closer: keeping only proposition-valued extra simp facts preserves all six gains but barely changes cost. Calling global simp_all followed by omega, without per-node rule classification, also preserves the six and reduces their aggregate raw heartbeats 3.09%. These goals have recursive definitions in the global simp set and no explicit lemma hints, so they do not establish that supplied facts can be omitted generally.

Both retain the current reservation and were not shown to recover its four checked corpus losses. They are separable performance/code-size experiments, not evidence that the default integration is ready to merge.