skill-lean-implementation-hard

name	skill-lean-implementation-hard
description	Implement Lean 4 proofs using hard-mode behavioral contracts with per-phase dispatch and sorry inventory tracking. Invoke for Lean-language implementation tasks when hard-mode is requested.
allowed-tools	Agent, Bash, Edit, Read, Write

Lean Implementation Hard Skill

Thin wrapper that delegates Lean 4 hard-mode proof implementation to lean-implementation-hard-agent subagent with per-phase dispatch context.

IMPORTANT: This skill implements the skill-internal postflight pattern. After the subagent returns, this skill handles all postflight operations (status update, artifact linking, sorry_inventory propagation, git commit) before returning.

Hard mode activates H2 (anti-analysis with formal proof line bar) and H9 (sorry inventory tracking with orchestrator handoff JSON at every dispatch). Cost is approximately 3-5x standard lean4 implementation.

Trigger Conditions

This skill activates when:

• Task type is "lean4" or "lean" (either accepted)
• /implement N --hard is invoked for a lean4 task
• Dispatched from skill-orchestrate-hard via per-phase dispatch mode
• Routed by command-route-skill.sh via routing_hard.implement.lean4

---

Execution Flow

Stage 1: Input Validation

Validate required inputs:

• task_number - Must be provided and exist in state.json
• Task status must allow implementation (planned, implementing, partial)
• Task type must be lean4/lean

# 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')

# Validate task_type (accept both "lean" and "lean4")
if [ "$task_type" != "lean" ] && [ "$task_type" != "lean4" ]; then
  return error "Task $task_number is not a Lean task (got: $task_type)"
fi

# Check terminal states
if [ "$status" = "completed" ] || [ "$status" = "abandoned" ] || [ "$status" = "expanded" ]; then
  return error "Task $task_number is in terminal state: $status"
fi

---

Stage 1.5: Hard-Mode Cost Note

Before proceeding, emit the cost note for session tracking:

[hard-mode] skill-lean-implementation-hard activated (session flag: hard)
Cost multiplier: ~3-5x standard lean4 implementation
Behavioral contracts: H2 (formal proof line bar), H9 (sorry inventory tracking)
Per-phase dispatch: each agent invocation handles exactly one plan phase

---

Stage 2: Preflight Status Update

Update task status to "implementing" BEFORE invoking subagent.

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

---

Stage 3: Plan Resolution and Phase Identification

Find the latest plan file and identify the next incomplete phase for per-phase dispatch:

# Find latest plan
padded_num=$(printf "%03d" "$task_number")
# Absolute anchor handed to the dispatched agent. SKILL_REPO_ROOT is exported by skill-base.sh
# when sourced; $(pwd) is a last-resort fallback for direct invocation.
task_dir_abs="${SKILL_REPO_ROOT:-$(pwd)}/specs/${padded_num}_${project_name}"
handoff_path_abs="${task_dir_abs}/.orchestrator-handoff.json"
plan_file=$(ls "specs/${padded_num}_${project_name}/plans/"*.md 2>/dev/null | sort -V | tail -1)

if [ -z "$plan_file" ]; then
  return error "No plan file found for task $task_number"
fi

# Read plan to find next incomplete phase. Sourced from the shared anchor
# (scripts/lib/phase-heading-patterns.sh) rather than re-derived inline -- this also gains
# decimal sub-phase support (e.g. "Phase 3.1"), which the prior digits-only pattern never had.
#
# Leaf-worker posture (same as skill-implementer-hard's Stage 3b): this check runs strictly
# before any Agent tool dispatch, so no handoff write is owed here, and adopts this file's own
# `return error` convention rather than a raw `exit`.
. .claude/scripts/lib/phase-heading-patterns.sh
phase_number=""
phase_scan_inconclusive=false
# --- resume-scan-conformance-gate:begin ---
# Whole-file conformance check BEFORE the filtered scan below. PHASE_HEADING_ERE admits
# conforming headings only, so a non-conforming heading is not merely unmatched by that grep --
# it is INVISIBLE to it, and the scan would silently select the next conforming OPEN heading
# instead, dispatching out of order on top of unfinished work. has_nonconforming_phase_headings
# is the required boolean predicate; the `nonconforming_phase_headings | grep -q .` pipe form is
# forbidden (unsafe under pipefail).
if has_nonconforming_phase_headings "$plan_file"; then
  warn_nonconforming "$plan_file" "lean-implementation-hard-next-phase" || true
  phase_scan_inconclusive=true
else
  # Extract phase number via the library's extract_phase_number rather than the prior PCRE-based
  # lookbehind extraction -- the PCRE grep flag is not available on every platform and was a
  # second, unnecessary divergence from every other consumer of this grammar.
  next_phase_heading=$(grep -E "${PHASE_HEADING_ERE} .*${PHASE_STATUS_OPEN_ERE}" "$plan_file" | head -1)
  if [ -n "$next_phase_heading" ]; then
    phase_number=$(extract_phase_number "$next_phase_heading") || phase_number=""
    if [ -z "$phase_number" ]; then
      # Defense-in-depth only, and unreachable by construction: the grep above already
      # guarantees this line matches PHASE_HEADING_ERE. Funnelled into the same sentinel so
      # there is exactly one inconclusive path, never a second silent one.
      phase_scan_inconclusive=true
    fi
  fi
fi
# --- resume-scan-conformance-gate:end ---

if [ "$phase_scan_inconclusive" = "true" ]; then
  return error "Non-conforming phase heading(s) found during resume-scan -- the filtered scan cannot see them, so the resume point is UNKNOWN. Refusing to guess. See the named, line-numbered warning above."
fi

# Read handoff for per-phase dispatch context (territory, continuation_context)
handoff_file=$(ls "${handoff_path_abs}" 2>/dev/null | head -1)
territory=null
continuation_context=null

if [ -f "$handoff_file" ] && jq empty "$handoff_file" 2>/dev/null; then
  territory=$(jq -c '.territory // null' "$handoff_file")
  continuation_context=$(jq -c '.continuation_context // null' "$handoff_file")
  # Import sorry_inventory from previous handoff for propagation
  prev_sorry_inventory=$(jq -c '.sorry_inventory // []' "$handoff_file")
fi

---

Stage 4: Prepare Delegation Context

Prepare delegation context for the subagent with per-phase dispatch parameters:

{
  "session_id": "sess_{timestamp}_{random}",
  "delegation_depth": 1,
  "delegation_path": ["orchestrator", "implement", "skill-lean-implementation-hard"],
  "timeout": 7200,
  "effort_flag": "hard",
  "task_context": {
    "task_number": N,
    "task_name": "{project_name}",
    "description": "{description}",
    "task_type": "lean4"
  },
  "plan_path": "specs/{N}_{SLUG}/plans/MM_{short-slug}.md",
  "phase_number": {N_or_null},
  "territory": {territory_or_null},
  "continuation_context": {continuation_context_or_null},
  "metadata_file_path": "specs/{N}_{SLUG}/.return-meta.json",
  "task_dir": "{ABSOLUTE path to the task directory}",
  "handoff_path": "{ABSOLUTE path the agent MUST write its handoff to}",
  "dispatch_seq": "{dispatch_seq from this skill's own delegation context, forwarded unchanged; omit if absent}"
}

Forward dispatch_seq unchanged. If this skill's own delegation context carries a dispatch_seq field, forward it into the sub-agent's delegation context above verbatim — the same pass-through treatment already given to territory and handoff_path. Never invent, increment, or recompute a value at this layer; only the orchestrator mints one. If absent, omit the field. See context/patterns/dispatch-report-not-termination.md.

---

Stage 5: Invoke Subagent

CRITICAL: You MUST use the Agent tool to spawn the subagent.

Required Tool Invocation:

Tool: Agent (NOT Skill, NOT Plan)
Parameters:
  - subagent_type: "lean-implementation-hard-agent"
  - model: "opus"
  - prompt: [Include task_context, delegation_context, plan_path, phase_number,
             territory, continuation_context, metadata_file_path, handoff_path]
  - description: "Execute hard-mode Lean implementation for task {N} phase {P}"

DO NOT use Skill(lean-implementation-hard-agent) - this will FAIL.

The subagent will:

• Apply H2 anti-analysis contract (formal proof line bar within 30% of tool calls)
• Apply H9 wrap-up discipline (sorry_inventory in every dispatch end)
• Implement ONLY the specified phase (per-phase focus)
• Use lean_goal before and after each tactic application
• Use lean_multi_attempt before applying edits
• Run final verification (sorry check, axiom check, lake build — detached, via the build guard, see context/project/lean4/operations/long-builds.md)
• Write the orchestrator handoff (with sorry_inventory) to the ABSOLUTE path given as handoff_path in the delegation context — never a bare .orchestrator-handoff.json filename
• Create implementation summary
• Write metadata to specs/{N}_{SLUG}/.return-meta.json
• Return a brief text summary (NOT JSON)

---

Stage 5b: Self-Execution Fallback

CRITICAL: If you performed the work above WITHOUT using the Agent tool, you MUST write a .return-meta.json file now before proceeding to postflight.

If you DID use the Agent tool, skip this stage.

---

Postflight (ALWAYS EXECUTE)

Stage 6: Parse Subagent Return

Read the metadata file:

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")
    phases_completed=$(jq -r '.metadata.phases_completed // 0' "$metadata_file")
    phases_total=$(jq -r '.metadata.phases_total // 0' "$metadata_file")

    # Read verification results (agent is responsible for verification)
    verification_passed=$(jq -r '.verification.verification_passed // false' "$metadata_file")
    sorry_count=$(jq -r '.verification.sorry_count // 0' "$metadata_file")

    # Read sorry_inventory from agent output
    sorry_inventory=$(jq -c '.sorry_inventory // []' "$metadata_file")
else
    echo "Error: Invalid or missing metadata file"
    status="failed"
    verification_passed="false"
    sorry_inventory="[]"
fi

---

Stage 6a: Plan Compliance Check (Read from Metadata)

This stage only runs if status from metadata is "implemented".

Read the agent-reported compliance result from metadata:

if [ "$status" = "implemented" ]; then
    compliance_check=$(jq -r '.metadata.compliance_check // "skipped"' "$metadata_file" 2>/dev/null)

    case "$compliance_check" in
        "failed")
            echo "Stage 6a: Plan compliance check FAILED (agent reported)"
            status="partial"
            ;;
        "passed")
            echo "Stage 6a: Plan compliance check PASSED"
            ;;
        "skipped"|*)
            echo "Stage 6a: INFO — compliance_check absent or skipped; proceeding"
            ;;
    esac
fi

---

Stage 6b: Sorry Inventory Propagation

After agent returns, propagate sorry_inventory to .orchestrator-handoff.json:

handoff_file="${handoff_path_abs}"

if [ -f "$handoff_file" ] && jq empty "$handoff_file" 2>/dev/null; then
    # Merge with previous sorry_inventory (prev + new — resolved)
    # The agent writes the authoritative sorry_inventory to the handoff JSON
    echo "Stage 6b: sorry_inventory propagated via agent handoff JSON"
    echo "  Current sorry count: $(echo "$sorry_inventory" | jq 'length')"
else
    echo "Stage 6b: WARNING — no .orchestrator-handoff.json found"
    echo "  Agent should have written this file. Check agent output."
fi

---

Stage 7: Update Task Status (Postflight)

If status is "implemented" AND verification_passed is true AND sorry_count is 0:

bash .claude/scripts/update-task-status.sh postflight "$task_number" implement "$session_id" --phase-check=warn

Then add completion_data to state.json:

completion_summary=$(jq -r '.completion_data.completion_summary // ""' "$metadata_file")
roadmap_items=$(jq -c '.completion_data.roadmap_items // []' "$metadata_file")

if [ -n "$completion_summary" ]; then
    bash .claude/scripts/state-write.sh \