---
name: rederive
description: "This skill should be used when a contributor names a core protocol whose Lean contract is to be re-derived, or invokes /rederive. Runs the per-protocol flow: gather the pre-understanding, derive the protocol's epistemic solution and fuse it with the contributor's horizon, then read the current contract against it, through sketch, edit, dogfood, review, merge, the chart close and a retrospective on this skill. Project-local contributor tooling."
allowed-tools: Bash, Read, Grep, Glob, Agent, Skill
---

# Re-derive a protocol contract

One protocol per run. The object is the core protocol itself — its `SKILL.md` on `origin/main`; an open PR whose branch carries the chart id, where one exists, is one more piece of material, never the anchor. Anchor chart: the protocol's own `ROO-*` chart; suite-wide ground: ROO-67.

**What a re-derivation answers to.** The target is the morphism that the `AGENTS.md` Northstar and the premise axiom Context and Utterance as First-Class Ground (`premise/recognition-and-authority.md`) admit, in the form `lean/EpistemicProtocols/Ground.lean` fixes: the fused context — turns bound to who sent them — and the person's utterance are the ground; the structure fixes only what the harness knows; everything else is the model's inference, declared as a documented judgment inside the types. The solution is derived from the gathered pre-understanding and taken at the fusion gate before the current contract is read; the pre-Lean DSL, the current block, any open PR and earlier decides are evidence read against that solution, never the target.

## Steps

1. **Trigger** — a contributor names the protocol. Resolve its chart; where the protocol's earlier chart is Done, open a new chart linked to it and to ROO-67 (ROO-67 decide 5e64392d). The order across protocols is the contributor's and session-local; nothing here fixes it.
2. **Gather the pre-understanding** — afresh every run, since what it holds moves between runs:
   - Ground: the Northstar, the premise axiom above, `Ground.lean`, and the protocol's declared deficit and resolution type — its Type line and Definition only, not the formal block; the fusion gate may revise them.
   - Decide coordinates: both charts' decide comments, the protocol chart's Open questions and its related issues; a later decide that supersedes an earlier one says so (ROO-67 decide 78e615b4).
   - Literature: delegate to a subagent — primary sources on the cognitive deficit this protocol takes and the resolution it yields; where a source's setting differs from the one the protocol runs in, the claim names that transfer. Every claim carries its verification strength and names the weakest link (`AGENTS.md` §Settled Directions, Academic grounding).
   - Real use: `~/.claude/projects/*/*.jsonl` sessions where the contributor typed the command (exclude `-private-tmp*`); what the deficit looked like there, and where the run went wrong or right.
3. **Derive the solution** — from the gathered material, not from the current block: deficit → resolution, first stated as one sentence of what the person can then say or recognize — the repair direction every later finding is read against; the coordinates only the person fills, the closure kinds, and the conditions that hold only where a ground carries them — Northstar, premise, literature, the contributor's utterance, a decide, or observed use; any other morphism step is scaffolding, carried as guidance on a documented judgment (ROO-67 decide 0d3b1e3b). Each part names what grounds it. A shape carried from a sibling protocol's re-derivation is pre-understanding: each constructor or slot it brings is tested against this protocol's deficit before it enters the solution.
   - Independent derivation: `/codex-plus:codex` with an English prompt carrying the locations of the gathered material, the literature findings as a file, and the question this step answers — never this session's solution; it may read beyond the list. Compare the two derivations part by part.
4. **Fusion gate** — present the derived solution beside the ground of each part, where the independent derivation agrees and splits, the real-use reading, the contrary grounds and live alternatives with their consequences, and the limits of what was searched. Branches:
   - the contributor takes it → write the solution decide on the protocol chart (`/unfold decide`) and go to the reading step;
   - the contributor corrects or replaces part of it → fuse the utterance and derive again;
   - the correction moves the pre-understanding (a source, a decide, a reading of use) → gather again where it moved, then derive;
   - the contributor stops → the run ends; what was gathered and derived is recorded on the protocol chart;
   - no utterance → the gate holds; nothing is taken.

   **Re-entry.** A later finding — in the reading, the sketch, the sketch consult, dogfood, or the review — is triaged by what it does to a taken part: one that moves the ground of a taken part returns the run to the earliest step that part depends on and then to this gate, naming the part it moves; one that applies a taken part is a fix. Findings are presented grouped by the part they bear on, not as an item list. Parts whose ground did not move stand; a pass that moves no ground re-opens nothing.

   **Without the contributor.** Where the run proceeds unattended, each gate in it that holds the contributor's judgment is taken provisionally, in place of holding, on the branch the settled decides and premise support, and the run goes on. The gates are recorded as one comment on the protocol chart headed as provisional gate records, never as a decide — per gate what was shown, the options, the provisional choice with its ground, and what would change it — and the PR marks what rests on them as provisional. When the contributor returns, each gate's answer becomes a decide on the chart.
5. **Read the current contract against the solution** — in a scratch tree at `origin/main` (`git worktree add --detach <scratch> origin/main`), with the open PR branch merged into it where one exists. Run `node .claude/skills/verify/scripts/lean-contract.js generate . && lake build --wfail` and `node .claude/skills/verify/scripts/static-checks.js .`; record failures, fix nothing; remove any scratch tree. This and the walks below up to the termination graph, except each lost obligation's disposition, do not depend on the solution: another context may prepare them before the fusion gate, and this session opens them once the solution is taken.
   - Pre-Lean diff: the block's last DSL version is the parent of the first commit that put a `lean` block in that `SKILL.md` (`git log <ref> --reverse --format=%h -S'```lean' -- <SKILL.md> | head -1`, then `<sha>^`). Walk it clause by clause against the current block, and list every field read with no write or written with no read on either side. For each obligation that is gone, `git log -S'<clause or field>'` and `git blame` find the commit that removed it; a decide or a commit message that states the removal marks it intended, anything else is a regression reported with its locator. Each lost obligation carries a disposition to the sketch gate — held elsewhere in the solution, naming the line that carries it, retired on a named ground, or a challenge to the solution that goes through re-entry; one held with no line to name is such a challenge.
   - Ablation row: the protocol's row in the ROO-67 document of the second Λ ablation pass (the #961 four: the first pass), its GROUND terms read against decide 78e615b4.
   - Termination graph: every way a run ends, and who closes it (person · AI relay · evidence). An unanswered checkpoint that requires the person's answer holds; nothing auto-selects.
   - Replay the real-use scenario where the current contract bites.
   - Apply the checklist below with `file:line` evidence. The result is a diagnosis: what the current contract carries that the solution does not, and what it lacks. Where it lacks nothing and carries nothing extra, the run goes to the close with that diagnosis recorded on the chart.
6. **Sketch** — before/after flow, a table of what changes, what stays, and the scenario replayed on the new shape. Present the lost obligations with their dispositions and the choices whose cost the reader bears as a gate. A sketch choice the gathered literature does not reach sends one targeted search back to the gathering step, fed into the gate, never as a verdict.
7. **Sketch consult** — `/codex-plus:codex` with an English prompt carrying the sketch's material and question, conclusions withheld; compare with this session's reading and report agreements and splits.
8. **Decides** — one per settled point: protocol-local → the protocol chart; suite-wide → ROO-67; a principle that holds beyond this repository → a proposal on the premise chart (ROO-77), never a `premise/` edit in this PR. Each via `/unfold decide`; wherever the run cites a decide — commit messages and the PR body among them — the citation names its chart beside its id.
9. **Edit in a fork** — a fork in a worktree, given the decide ids as its spec, on the open PR's branch rebased onto `origin/main`, or on a new branch from `origin/main` carrying the protocol chart id:
   - commit A, where the contract is not yet in this shape: GROUND copied from `lean/EpistemicProtocols/Ground.lean`, model judgments as documented `axiom`, a `Nonempty` instance per axiom type and each guarantee stated and proved together in `lean/EpistemicProtocols/<Namespace>/Theorems.lean`;
   - commit B: the re-derivation, with the surfaces that describe the changed interface swept before the PR (co-change) — where the protocol has `/realize` cases, their graders and scripted turns re-derived against the taken solution, not only re-quoted; another protocol's contract that names this one goes to a ROO-67 follow-up rather than this PR;
   - plugin version: one minor step over main's (ROO-67 decide db1de854);
   - verify: `lean-contract.js check` (generate, `lake build --wfail`, `lake lint`) and `lake test`, static checks, the `AGENTS.md` §Development test bundle, and `static-checks.test.mjs` in its own `node --test` run;
   - PR body carries the record and `Part of ROO-67`; no merge.
   Check the fork's report against the branch and CI before relaying it.
10. **Dogfood** — run the new `SKILL.md` by hand in this session on a live target. Each mismatch → a gate → the contributor's answer → a decide → a fork fix → re-judge. Close the run with the intents taken, quoting the contributor's words. This dogfood is the run's runtime evidence.
11. **Review** — this session drives `/review-loop` over the PR: landing `head`, codex and code-review at `xhigh` as parallel sources — code-review called level first (`xhigh <target>`) and told to keep its repository operations inside a review-only checkout —, the decide texts with the contributor's words as design intent, reaching each source's review agent (arguments alone do not carry them). Each round's repair, from the first round, is a root repair over the accumulated context — every prior round's findings, repairs and dispositions — toward subtraction rather than an addition per finding; each apply pass is checked with step 9's verify. A finding that asks to state an obligation the contract already satisfies as written in a second place changes nothing, since a second wording is read as a second meaning; where the contract states one obligation twice in different words, the repair keeps one statement in its authoritative home, and a rephrase for preferred wording alone is made only where an exercised reading failed (ROO-67 decide 6b4385c0). Where a contract clause overlaps what the harness, the system prompt, or the environment already supplies, treat the overlap as a conflict: make the clause orthogonal to it or remove it; an ablation is the test that settles which (ROO-67 decide fa09bb7d). Before removing text a source calls a duplicate, check whether `origin/main` carried it and whether it is the user-facing rendering of a behaviour; either makes its removal a contract change, not a cleanup. Where sources pull one clause opposite ways — remove it as a copy, or state it in the Rules or prose — the surface that governs that clause settles it once, not the latest round. At the start of each round and again before the merge, fetch `origin/main` and read what has changed since the run began in this skill, in the suite chart's decides, and on sibling protocol charts that touch this protocol; each change is triaged by step 4's re-entry rule. Commits that land after the last round — the contributor's decides on its findings applied among them — re-enter the loop over the range from the last reviewed head, before the merge.
12. **Merge and close** — merge only on the contributor's instruction. The close runs whatever status the chart shows: `/unfold close` on the protocol chart — structure delta, closing note with commit and PR locators, follow-ups with one pointer back.
13. **Skill retrospective** — after the close, read this run for where the flow sent it around and where the contributor brought something in at a gate. Present each candidate with its ground (a source, a decide, the premise, or this run's trace), the surface it reads as belonging to — this skill, the protocol chart, ROO-67, or a premise proposal on ROO-77 — and what it would make unnecessary here. Branches:
    - the contributor takes a candidate → it lands where the contributor placed it; a change to this skill is its own commit under ROO-67;
    - the contributor corrects or re-places one → fuse and present again;
    - no utterance → nothing changes.

## Checklist (reading step)

- **Translation or re-derivation** — does a stage machine (projected gate or phase state) return inside the fused context; do rule chains that guarded a changing Λ survive (premise "Cases in Place of a Judgment")?
- **Λ ablation** — each state field: a projection of the fused context → deleted; the occupant of an open coordinate → a `Coord` with citation, admits and supports; harness state (interrupt, steering, persistence) → a named delegation point, not a type; none of these → removed.
- **Gate earns its place** — a judgment gate stands where its answer is irreversible or is the held judgment the closure needs; a reversible step the person can interrupt through the harness takes no added gate. Reversibility grants no relay.
- **Relay reach** — the AI fills a judgment coordinate only where reachable evidence settles it or a grant covers it; discretion is not relay; a delegated fill is recorded as the AI's.
- **Place of observation** — is evidence adoption needs observed before the presentation, not after closure?
- **Focus and decision** — is a value on the record made only by a person's turn: its standing read from what that turn did, its proposer judged apart, adoption only for a value shown on a map or sheet before that turn, and of everything the sheet showed when that turn takes it, with no second permission for any line (ROO-67 decide 4ad45b5f; a record rule, not a gate on the closing transition; per-value deciding evidence, contrary grounds and ownership marks are welcome, not required), and its reach re-read on the fused context as it now stands with no read-once layer? Does focus — the inventory, the read-back, the presentation, whether an utterance bears on the run — compute no record value and harden into no obligation?
- **Closure kinds** — where the person closes, is that closure a result constructor kept apart from the AI's relay; where completion is structural, does it ask for no closing turn; and does withdrawal carry a result exactly where the person's ending requires an independently grounded account of the work's standing that existing outcomes cannot carry? Turning to other work leaves the gate holding and closes nothing; routing is not a closure kind.
- **Next move** — is a hand-off set only by a chain the person declared, an adopted routing policy, or an explicit grant, with document edges and AI tags presented as proposals?
- **After closure** — is the AI's contrary ground shown before the gate and attached to the closure record when the person closes over it; is re-raising bound to new evidence, and owed before a dependent irreversible step; is "accepted, evidentially disputed" representable; does the AI never rewrite or veto the closed value?
- **No premature typing** — does the sketch, or a repair in the review, close a model judgment (item identity, per-item kind, turn form, iteration, ordering, scope) into a type or new Lean structure? Keep it a `supports` judgment until dogfood observes that judgment failing.
- **Presentation** — for a protocol that revises a map or plan: the current sheet plus a change ledger; a picture only where paths diverge; every change since the sheet the person answered is on the ledger — edits, values re-filled because of them, and anything else that moved — and marking a re-drafted line necessary consequence or proposal is welcome, not required.
- **One slot, two meanings** — does any field carry two orthogonal meanings at once?