Preserve native proof budgets and repair stale capture dependencies

[Vilin97]

Whole-pool captures could remain stuck even though the native source built successfully. A saved project marker checked only root artifacts and setup hashes, allowing missing imported artifacts to go unnoticed. After dependency restoration, one MarkoffModP file also failed with the default typeclass heartbeat limit under compact instrumentation while a fresh native Lean check passed.

Always ask Lake to incrementally validate project module targets before capture; successful capture receipts still allow recorded files to be reused. Inside compact source scopes, remove internal trace options rather than merely setting trace.profiler false. Lean's Options.hasTrace fast path then matches untraced execution, avoiding typeclass-budget charges from disabled trace checks. Source timers, outer declaration/async scopes, and native proof limits remain intact.

Validation:

• npm test: 65 passed; npm run check passes.
• npm run test:source-focused: compact same-run event/range/thread/declaration/query parity, configured options, async=false, kernel rejection, heartbeat rejection, and both new integration tests pass. Linux raw-clock oracle is skipped on macOS.
• New native Lake integration test removes a transitive dependency artifact behind a valid root/setup checkpoint and verifies it is rebuilt.
• New heartbeat integration test preserves the internal-tracing fast path and the original typeclass budget; genuinely insufficient budgets still fail and preserve the prior output.
• Azure Lean 4.35.0-rc3: the exact previously failing LeanPool MarkoffModP file passes a fresh native Lean check and a compact capture with this driver (8,515 events), with its original options and heartbeat limits.

The companion weekly runner recovery and independent health checks are in LeanPool/lean-pool#661. Notifications remain disabled.