---
phase: 142-m2f-statement-compilation-pilot
plan: 01
type: execute
wave: 1
depends_on:
  - 141-01
files_modified:
  - research/knowledge-hub/knowledge_hub/statement_compilation_support.py
  - research/knowledge-hub/knowledge_hub/lean_bridge_support.py
  - research/knowledge-hub/knowledge_hub/aitp_service.py
  - research/knowledge-hub/knowledge_hub/aitp_cli.py
  - research/knowledge-hub/knowledge_hub/kernel_markdown_renderers.py
  - research/knowledge-hub/knowledge_hub/topic_shell_support.py
  - research/knowledge-hub/knowledge_hub/topic_dashboard_surface_support.py
  - research/knowledge-hub/knowledge_hub/runtime_bundle_support.py
  - research/knowledge-hub/runtime/schemas/statement-compilation-packet.schema.json
  - research/knowledge-hub/runtime/schemas/proof-repair-plan.schema.json
  - research/knowledge-hub/runtime/schemas/statement-compilation-active.schema.json
  - research/knowledge-hub/runtime/schemas/progressive-disclosure-runtime-bundle.schema.json
  - research/knowledge-hub/runtime/scripts/run_statement_compilation_acceptance.py
  - research/knowledge-hub/tests/test_aitp_cli.py
  - research/knowledge-hub/tests/test_aitp_service.py
  - research/knowledge-hub/tests/test_runtime_scripts.py
  - research/knowledge-hub/tests/test_schema_contracts.py
  - research/knowledge-hub/tests/test_statement_compilation_contracts.py
  - research/knowledge-hub/README.md
  - research/knowledge-hub/runtime/README.md
  - research/knowledge-hub/runtime/AITP_TEST_RUNBOOK.md
autonomous: true
requirements:
  - REQ-M2F-01
  - REQ-M2F-02
must_haves:
  truths:
    - statement compilation must be explicit and precede proof repair
    - the packet must not be Lean-only even if Lean is one downstream target
    - existing candidate/theory-packet artifacts remain the only formalization inputs
---

<objective>
Pilot one production statement-compilation lane that compiles bounded informal
theory statements into declaration skeletons and explicit proof-repair plans,
then feeds the existing Lean bridge from that packet.
</objective>

<tasks>

<task type="auto">
  <name>Task 1: Materialize statement-compilation and proof-repair packets</name>
  <files>research/knowledge-hub/knowledge_hub/statement_compilation_support.py, research/knowledge-hub/knowledge_hub/aitp_service.py, research/knowledge-hub/knowledge_hub/aitp_cli.py, research/knowledge-hub/runtime/schemas/statement-compilation-packet.schema.json, research/knowledge-hub/runtime/schemas/proof-repair-plan.schema.json, research/knowledge-hub/runtime/schemas/statement-compilation-active.schema.json</files>
  <read_first>research/knowledge-hub/knowledge_hub/lean_bridge_support.py</read_first>
  <action>Add one production `statement-compilation` CLI/service surface that writes candidate-scoped statement-compilation packets, proof-repair plans, and one active runtime index.</action>
  <verify>python -m pytest research/knowledge-hub/tests/test_aitp_cli.py -q -k "statement_compilation or lean_bridge"</verify>
  <acceptance_criteria>
    - one production CLI/service path materializes statement-compilation packets
    - packets contain declaration skeletons plus explicit proof holes
    - proof-repair plans name verifier targets without being Lean-only
  </acceptance_criteria>
  <done>Statement-compilation is a first-class production surface.</done>
</task>

<task type="auto">
  <name>Task 2: Feed Lean bridge and runtime surfaces from statement compilation</name>
  <files>research/knowledge-hub/knowledge_hub/lean_bridge_support.py, research/knowledge-hub/knowledge_hub/topic_shell_support.py, research/knowledge-hub/knowledge_hub/topic_dashboard_surface_support.py, research/knowledge-hub/knowledge_hub/runtime_bundle_support.py, research/knowledge-hub/runtime/scripts/run_statement_compilation_acceptance.py, research/knowledge-hub/tests/test_aitp_service.py, research/knowledge-hub/tests/test_runtime_scripts.py, research/knowledge-hub/tests/test_schema_contracts.py, research/knowledge-hub/tests/test_statement_compilation_contracts.py, research/knowledge-hub/README.md, research/knowledge-hub/runtime/README.md, research/knowledge-hub/runtime/AITP_TEST_RUNBOOK.md</files>
  <read_first>research/knowledge-hub/runtime/AITP_TEST_RUNBOOK.md</read_first>
  <action>Make `prepare_lean_bridge()` consume the compiled statement packet, expose statement-compilation status in runtime surfaces, and add isolated acceptance/docs/tests.</action>
  <verify>python research/knowledge-hub/runtime/scripts/run_statement_compilation_acceptance.py --json</verify>
  <acceptance_criteria>
    - Lean bridge packet records statement-compilation and repair-plan refs
    - runtime surfaces expose statement-compilation summary as a first-class step before Lean bridge
    - isolated acceptance proves statement-compilation plus downstream Lean bridge consumption on a temp kernel root
  </acceptance_criteria>
  <done>Phase `142` is ready to summarize and verify.</done>
</task>

</tasks>
