SK_EFT_Hawking

In-loop development guidance for an autonomous /goal Lean-proof loop in SK_EFT_Hawking. This skill should be used when developing Lean 4 proofs inside a goal loop, deciding whether to fan work out to parallel worktree slots or stay solo, resetting a worktree slot, hitting a recurring Lean tactic/ elaboration friction, or sharding the lab notebook. It surfaces the MCP-first proof loop, kernel-purity rules, the worktree fan-out flow, and a symptom-indexed friction catalog. Invoke it at the start of a development stretch and whenever you hit proof-mechanics friction or need the parallel-dev recipe.

Goal-mode LAUNCH + always-on posture for an autonomous /goal dev loop. On invocation it composes the /goal condition AND registers the session with the harness; its core posture re-attaches after compaction. Use when STARTING a managed /goal dev loop, or writing/refining a goal prompt + acceptance criteria. (For IN-LOOP development guidance — the MCP proof loop, worktree fan-out, friction catalog — use the goal-dev skill instead.)

Off-hot-loop System-2 harvest. Reads each managed /goal session's transcript from a byte-offset watermark, extracts process/harness signal (Haiku) — crossing the compact boundary for the pre-vs-post-compact delta and ingesting the guard's blocked-question log — and a register-AWARE Opus consolidator files/combines it into the four-section register (Open / Process Wins / Closed / Misfiled) — re-opening a recurring closed finding, grouping semi-related ones, filing real wins to Process Wins (capped at agent-reviewed, never injected), and dropping noise (never writing Misfiled — that is /debrief's human sweep) — then refreshes the open-only active-issues view. Invoked by a Desktop scheduled task or a second-session /loop — never inside a /goal session.

Interactively review the System-2 dev-process harvest — promote agent-reviewed findings to human-reviewed (or close them), and triage GAP-A gate proposals. Runs over the register-aware harvest's already-synthesized register (it files/combines/re-opens continuously); debrief is the human governor — only it promotes to human-reviewed. Use when you want to sign off on what the autonomous loop learned about HOW it ran.

Run the full mechanical Stage-12 sync (counts, tables, deps, citation cache) in one command. Use before a wave gate, or whenever counts/tables/figures may have drifted from the Lean/Python sources.

Close a wave deterministically — run the gate prerequisites, dispatch the fresh-context adversarial review, and record the close. Use once per wave when the wave's bricks are shipped and validate is green.