implement_plan_micro

Five modal logics via fusion with bridge principles:

• JL: Justification Logic - evidence-backed claims
• IEL: Inferential Erotetic Logic - question handling
• TEL: Temporal Epistemic Logic - phase sequencing
• SDL: Standard Deontic Logic - obligations/permissions
• DEL: Dynamic Epistemic Logic - action modalities

```

# Justification terms

[h]:context(task_n) # Handoff h justifies task context

[v]:verified(phase_n) # Verification v justifies completion

[p]:plan(tasks) # Plan p justifies task list

# Evidence production

[read(f)]exists e. [e]:content(f)

[verify(c)]exists v. [v]:pass(c) | [v]:fail(c)

# Handoff chain: evidence propagates

[h_n]:complete(task_n) -> [h_{n+1}]:context(task_{n+1})

proceed(task) <-> exists h. [h]:validated

```

```

# Mode and blocker questions

?{direct, orchestration} # Mode selection

?{continue, retry, ask_user} # Blocker resolution

mismatch(plan, reality) -> ?{how_proceed}

no_validation -> ?{run_validation_first}

```

```

# File reading constraints

[](mentioned(f) -> <>read_fully(f)) # Eventually read

[](mentioned(f) -> not spawn U read_fully(f)) # No spawn until read

[](partial_read(f) -> false) # Partial reads forbidden

# Phase sequencing

[](phase(n) -> P(phase(n-1) & verified(n-1))) # Verified before next

[](automated_pass -> <>manual_verify) # Automated gates manual

[](manual_pass(n) -> <>phase(n+1)) # Manual gates next phase

# Handoff persistence

[](handoff_created(h) -> []exists_on_disk(h)) # Survives compaction

# Termination

<>(all_complete | abandoned)

```

```

# Reading obligations

O(read_fully(plan))

O(read_fully(f)) <- mentioned_in_plan(f)

O(check_existing_checkmarks)

F(partial_read)

# Verification obligations

O(run_automated) <- impl_complete

O(pause_for_manual) <- automated_pass

O(present_manual_checklist)

F(checkoff_manual) <- not user_confirmed

# Mode selection

O(orchestration) <- tasks >= 4

P(direct) <- tasks <= 3

O(respect_user_preference)

# Orchestration obligations

O(read_previous_handoff) <- exists_handoff(task_{n-1})

O(create_handoff) <- agent_completes

O(update_ledger) <- task_complete

F(batch_tasks) # One agent per task

F(proceed_on_mismatch) <- not user_guidance

```

```

# Implementation actions

[read(plan)]K(tasks) & K(phases) & K(criteria)

[read(handoff_n)]K(context_{n+1})

[spawn(agent, task)]<>result(agent)

[verify(c)](K(pass) | K(fail))

# Composed workflows

[select_direct][implement ; verify_auto ; present_manual ; wait]*

[select_orchestration][prepare ; spawn ; wait ; read_handoff ; update]*

# Recovery

[compaction ; read_ledger ; list_handoffs ; read_last]resume

# Mismatch

[detect_mismatch ; stop ; present ; wait]proceed_or_abort

```

```

# Evidence persistence (JL-TEL)

[h]:context(n) -> [][h]:context(n)

# Evidence obligations (JL-SDL)

O(exists h. [h]:validated) <- pre_implement

O(exists v. [v]:pass(auto)) <- pre_manual

# Handoff chain (full integration)

[h_n]:complete(n) -> O([spawn]<>[h_{n+1}]:context(n+1))

compaction -> (forall h. persists(h))

```

```

INIT --> READ_PLAN --> MODE_SELECT --+--> DIRECT: [IMPL -> AUTO -> MANUAL -> WAIT]*

|

+--> ORCHESTRATION: [PREP -> SPAWN -> WAIT -> HANDOFF]*

|

v

COMPLETE

```

```yaml

handoff_path: "thoughts/handoffs//task-[NN]-[desc].md"

schema:

required: [status, task_desc, files_modified[], verification_results, context_for_next]

optional: [blocker, decisions[], open_questions[]]

tracking:

plan: "- [x] Task N: description"

ledger: "[x] Task N"

```

---

# Prose (Where Logic Insufficient)

| Tasks | Context Critical | Mode |

|-------|------------------|------|

| 1-3 | No | Direct |

| 1-3 | Yes | Orchestration |

| 4+ | Any | Orchestration |

User preference overrides.

Mismatch:

```

Issue in Phase [N]:

Expected: [plan says]

Found: [actual]

How should I proceed?

```

Manual Verification Pause:

```

Phase [N] Complete - Ready for Manual Verification

Automated passed: [list]

Please verify: [manual items from plan]

Let me know when done.

```

Agent Spawn:

```

Task(subagent_type="general-purpose", model="claude-opus-4-5-20251101", prompt="""

[implement_task SKILL.md]

• Ledger: [content]
• Plan: [section]
• Task: [N]/[Total]: [desc]
• Previous Handoff: [content or "first task"]
• Handoff Dir: thoughts/handoffs//

""")

```

Recovery (post-compaction):

1. Ledger auto-loaded by SessionStart
2. ls thoughts/handoffs//
3. Read last handoff
4. Resume next task

---

# Validity Constraints

```

forall phase. has_auto_criteria(phase) & has_manual_criteria(phase)

forall task. one_agent_per_task(task)

forall h. on_disk(h) -> recoverable(h)

compaction -> (forall h. persists(h))

forall i < j. completed(task_i) before started(task_j)

```