fix(autotrain): consume proof-bound screening budgets

[Tyler-R-Kendrick]

Summary

• calculate the symmetric arm wall from the registered Lean-parity bound and re-evaluate it against the measured whole-second remainder after setup
• bind the theorem-selected screening sample to eval_limit and authorize that field in campaign manifests
• scope power evidence to its measured metric and supersede stale rebuild actions with content-bound proof receipts
• restore between-cycle console matrices
• wake governed supervisor backoff when an action/heal receipt lands
• make the pinned Torch bootstrap work on aarch64/Nix without widening the libc search path
• keep orchestration-only autoresearch commands off the OpenUI DSL import path

Evidence

• initial bound: max=180, reserves=15/15, kill grace=10, stages=2 -> 70s arm / 55s payload
• cycle 2370 refit: measured remaining=134.555s, proof input=134 -> 47s arm / 32s payload
• cycle 2388 refit: measured remaining=149.410s, proof input=149 -> 54s arm; executed --experiment-wall-seconds 54.000000
• cycle 2389 refit: measured remaining=150.321s, proof input=150 -> 55s arm; executed --experiment-wall-seconds 55.000000
• cycle 2390 refit: measured remaining=77.450s, proof input=77 -> 18s arm / 3s payload; both arms executed --experiment-wall-seconds 18.000000 and timed out without scoreboards
• cycle 2391: setup exhausted the calculated remainder before arm launch and failed closed
• cycle 2392 refit: measured remaining=77.482s, proof input=77 -> 18s arm / 3s payload; candidate timed out in package-root DSL import before producing a scoreboard
• screening sample: decidability floor=6, power floor unavailable for eval_nll, budget ceiling=21, suite ceiling=24 -> chosen n=6
• import-light repair: CLI help 9.70s; explicit DSL load 4.49s; 4 import-hygiene tests pass; Ruff, repository policy, and version-stamp policy pass
• wider changed-file hook: 617 pass / 4 fail; all four failures reproduce unchanged at connector head 5c7b96ff
• connector delivery: c2387-c2392 docs and all repairs are committed through head b724f8a5

Cycles 2390 and 2392 rendered the canonical four-table matrix and classified their proof-bounded timeouts as incomplete measurement, not model verdicts. Cycle 2391 failed closed before arm launch. The startup repair preserves eager package-root compatibility by default, selects the light path only for the autoresearch CLI, and explicitly loads the DSL for commands that require it.

[vercel]

The latest updates on your projects. Learn more about Vercel for GitHub.

Project	Deployment	Actions	Updated
slm-training	Ready	Preview	Sep 1, 2026 2:00am UTC

[coderabbitai]

Important

• 🔍 Trigger review

This repository does not receive automatic reviews because it has fewer than 10 stars.

⚙️ Run configuration

Configuration used: defaults

Review profile: CHILL

Plan: Team

Run ID: 3fe78258-a6c1-45e7-88e8-ed11b58c013c

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands.}