benbrastmckie/nvim/skill-lean-research-hard

# Lookup task
task_data=$(jq -r --argjson num "$task_number" \
  '.active_projects[] | select(.project_number == $num)' \
  specs/state.json)
 
# Validate exists
if [ -z "$task_data" ]; then
  return error "Task $task_number not found"
fi
 
# Extract fields
task_type=$(echo "$task_data" | jq -r '.task_type // "general"')
status=$(echo "$task_data" | jq -r '.status')
project_name=$(echo "$task_data" | jq -r '.project_name')
description=$(echo "$task_data" | jq -r '.description // ""')

[hard-mode] skill-lean-research-hard activated (session flag: hard)
Cost multiplier: ~3-5x standard lean4 research
Behavioral contracts: H2 (anti-analysis), H3 (lean4 reference grounding),
  H4 (adversarial self-verification), H5 (divergence audit on demand)

bash .claude/scripts/update-task-status.sh preflight "$task_number" research "$session_id"

# WARN-only: reports lean-lsp MCP registration drift without blocking dispatch. Two
# invocations: the no-flag call keeps the human-readable transcript message unchanged; the
# --dispatch-block call separately captures the evidence-tier block for Stage 3's
# lean_readiness field, so the finding reaches the subagent instead of being discarded after
# printing to the transcript. Not latency-critical on this (non-/orchestrate) path.
lean_readiness=""
if [ -x .claude/scripts/lean-mcp-preflight-check.sh ]; then
  bash .claude/scripts/lean-mcp-preflight-check.sh || true
  lean_readiness="$(bash .claude/scripts/lean-mcp-preflight-check.sh --dispatch-block 2>/dev/null)" || lean_readiness=""
fi

{
  "session_id": "sess_{timestamp}_{random}",
  "delegation_depth": 1,
  "delegation_path": ["orchestrator", "research", "skill-lean-research-hard"],
  "timeout": 3600,
  "effort_flag": "hard",
  "task_context": {
    "task_number": N,
    "task_name": "{project_name}",
    "description": "{description}",
    "task_type": "lean4"
  },
  "focus_prompt": "{optional focus — if contains 'divergence' or 'audit', agent activates H5}",
  "lean_readiness": "{Stage 2's captured --dispatch-block output; empty string when the probe is absent or this is not a Lean project}",
  "metadata_file_path": "specs/{N}_{SLUG}/.return-meta.json"
}

Tool: Agent (NOT Skill, NOT Plan)
Parameters:
  - subagent_type: "lean-research-hard-agent"
  - model: "opus"
  - prompt: [Include task_context, delegation_context, focus_prompt, metadata_file_path]
  - description: "Execute hard-mode Lean research for task {N}"

metadata_file="specs/${padded_num}_${project_name}/.return-meta.json"
 
if [ -f "$metadata_file" ] && jq empty "$metadata_file" 2>/dev/null; then
    status=$(jq -r '.status' "$metadata_file")
    artifact_path=$(jq -r '.artifacts[0].path // ""' "$metadata_file")
    artifact_type=$(jq -r '.artifacts[0].type // ""' "$metadata_file")
    artifact_summary=$(jq -r '.artifacts[0].summary // ""' "$metadata_file")
    adversarial_triggered=$(jq -r '.metadata.adversarial_verification_triggered // false' "$metadata_file")
    findings_count=$(jq -r '.metadata.findings_count // 0' "$metadata_file")
else
    echo "Error: Invalid or missing metadata file"
    status="failed"
fi

bash .claude/scripts/update-task-status.sh postflight "$task_number" research "$session_id"

if [ -n "$artifact_path" ]; then
    bash .claude/scripts/state-write.sh \
      '(.active_projects[] | select(.project_number == $num)).artifacts += [{"path": $path, "type": $type, "summary": $summary}]' \
      --session-id "$session_id" \
      --argjson num "$task_number" \
      --arg path "$artifact_path" \
      --arg type "$artifact_type" \
      --arg summary "$artifact_summary"
fi

bash .claude/scripts/git-commit-scoped.sh \
  --message "task ${task_number}: complete research" \
  --session "${session_id}" \
  --honest-index-rows "${task_number}" \
  -- "specs/${padded_num}_${project_name}/reports/" \
     "specs/${padded_num}_${project_name}/.return-meta.json" \
     "specs/TODO.md" \
     "specs/state.json"

Hard-mode research completed for task {N}:
- Found {findings_count} verified Mathlib lemmas/theorems
- H4 adversarial verification: {triggered revisions / no revisions needed}
- H5 divergence audit: {activated / not activated}
- H3 reference grounding tier: {Tier 1 / Tier 2 / Tier 3 / none}
- Created report at specs/{N}_{SLUG}/reports/MM_{short-slug}.md
- Status updated to [RESEARCHED]
- Changes committed