[ejgallego]

This PR stops runAt tactic probes from reporting success when their result uses the declaration being proved. While a declaration elaborates, Lean exposes it to its own body as an auxiliary local and checks every such use for termination only when it finalizes the declaration. A probe has no finalization step, so a probe such as exact countDown n or exact tacticSelf previously returned success: true whether or not the real edit would pass Lean's termination check, including for unsound circular proofs.

• Tactic probes whose assigned terms reference the enclosing declaration's auxiliary local, or another member of its mutual block, now return success: false with the original proof state, no successor handle, and a message naming the declaration and pointing to edit-and-sync.
• The check covers only the terms assigned to the probe's starting goals; the rest of the body was already checked by the document's own elaboration. Each handle step is checked against its own starting goals.
• Valid structural or well-founded recursion, and partial/unsafe definitions, now also report the probe as unchecked rather than succeeding. That is a deliberate trade: no probe answer is wrong, at the cost of requiring edit-and-sync for recursive proofs. Running Lean's termination check on a speculatively completed declaration is possible later work.
• Command probes are unchanged; they elaborate complete declarations through Lean's normal termination checks.
• Docs (STATUS, MCP, skill workflow reference) describe the new boundary; tests cover tactic, term, hole, structural recursion, and mutual-block self-reference plus later declarations staying unknown.