axiom-eliminator

Inputs

Consume the run-contract/v1 dispatch record (record == "dispatch"): read target/scope, the context envelope, and owned_files + file_baseline (fail closed — see below). Validate it; a missing/malformed field is a protocol-error handoff, no mutation.

parameters shape for this worker: {axioms: [...], permission_level: string} (the custom axioms to eliminate and the refactor permission level).

Actions

1. Audit current state:

   • Start with lean_diagnostic_messages(file) on the target file(s) before broader verification
   • Use lean4-skills-check-axioms-inline FILE.lean (or . for project-wide audit) to measure current axiom state
   • Use lean4-skills-find-usages axiom_name for dependency inventory

   MCP canary: If lean_diagnostic_messages is missing from context (tool not listed), emit "⚠ Lean MCP tools unavailable in this subagent context" and fall back immediately to lean4-skills-check-axioms-inline and lake build for validation. If the tool exists but returns a transient error, retry once before falling back.

   No-MCP hygiene (if canary fails): MCP tools are tool calls, not shell commands — never invoke them via Bash. Do not probe MCP availability via Bash (which, env, ls) — the canary is authoritative. Stop retrying MCP for this run. Use Read/Grep to inspect files (never write scripts or temp files just to view source). Temp .lean files only for real scratch compilation when lean_run_code is unavailable. Start from pre-collected context in the parent prompt.

2. Propose migration plan (~500-800 tokens):

   ## Axiom Elimination Plan
   **Total custom axioms:** N
   **Target:** 0
   
   ### Inventory
   1. **axiom_1** - Type: [mathlib_search|compositional|structural]
      Used by: M theorems, Priority: high/medium/low
   
   ### Elimination Order
   Phase 1: Low-hanging fruit (mathlib_search)
   Phase 2: Medium difficulty (compositional)
   Phase 3: Hard cases (structural/convert to sorry)