git:20261019.bb109ab to git:20261019.7bdc90e

---

name: rederive

description: "This skill should be used when a contributor names a skill whose Lean contract is to be re-derived — a core protocol, or a utility skill whose formal block is or becomes Lean — or invokes /rederive. Runs the per-skill flow: gather the pre-understanding, derive the skill'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 skill per run, whose formal block is Lean or becomes Lean in the run: a core protocol in `scripts/load-protocols.js` `CANONICAL_PROTOCOL_SET`, or a utility skill in `LEAN_CONTRACT_UTILITIES` there, which a utility still carrying a text-DSL block enters in its run. Below, *the protocol* names that skill whichever kind it is. The object is the 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, which for a utility may be one chart several skills' runs share; 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).

- Definition history: for each suite-level definition the protocol's contract leans on — the COMPOSITION operator, a GROUND term, a convention another surface states for it — the commit that introduced it and each later commit that narrowed or widened it, in the definition itself and at the places this contract uses it (`git log -L` on the definition, `git blame`, `git log -S` on its terms at each use site), read as the intent the current text carries forward.

- Real use: `~/.claude/projects/*/*.jsonl` sessions where the skill ran — typed by the contributor or invoked through its delivery path (exclude `-private-tmp*`); what the deficit looked like there, and where the run went wrong or right. Where the skill runs rarely by nature, its sessions leave little; the commit history of the artifact its deficit is resolved in — each time that deficit came up and was resolved, by this skill or another route — is the real use read instead.

3. **Derive the solution** — the protocol's epistemic solution, from the gathered material, not from the current block: deficit → resolution, first stated as its solution sentence, 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, the domain boundary — what the transformation itself carries and what lies past its hand-off, which the contract names at its delegation point and does not prescribe (ROO-67 decide dad26302) —, 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 carried clause, constructor, or slot is tested against this protocol's deficit and governing surfaces 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, its domain boundary among them, 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 → nothing is taken as a decide; whether the run waits or goes on past the gate is judged from its context, and going on follows *Without the contributor* below.

**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 or goes on past a gate the contributor has not answered, each gate in it that holds the contributor's judgment is taken provisionally on the branch the settled decides and premise support, and the run goes on; where a repair can proceed only by choosing between provisional directions still in contention, that choice is a horizon-fusion point — the case that distinguishes them is kept for the contributor, that branch is refined no further until the contributor answers, and independent work 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, the provisional gates are presented in the contributor's language, starting from the scenario the sketch replays, before and after; 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, or taken provisionally under *Without the contributor*.

- 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>^`); where the block is still the DSL, that version is the current block. 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 the current Lean block no longer carries, `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 — those, and each obligation whose carrier the sketch or a later repair removes — carries a disposition, to the sketch gate or with the repair that removes its carrier — 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: where the passes carry one, 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 closes nothing and auto-selects nothing; which steps need one is read under the checklist's **Gate earns its place**.

- 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 a Lean contract lacks nothing and carries nothing extra, the run goes to the close with that diagnosis recorded on the chart; a still-DSL contract goes on to the sketch for its first Lean block.

6. **Sketch** — before/after flow, a table of what changes, what stays, and the scenario replayed on the new shape. Before it is shown, the check step 11 makes on a second wording runs on each clause the sketch would add to the contract (ROO-67 decide 6b4385c0). For each outcome that hands off, show the payload it supplies and how any referenced material remains reachable. 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 — with the provisional gate records where gates were taken provisionally —, 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 a Lean block 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 proved at the boundary it claims in `lean/EpistemicProtocols/<Namespace>/Theorems.lean`. A guarantee that claims run behavior takes the run's provenance as premise, and its docstring claims no more than its statement. A person-origin guarantee identifies the filled occurrence and its own citation; a still-DSL block takes this shape in commit B, its first Lean block written from the taken solution;

- commit B: the re-derivation, with the surfaces that describe the changed interface swept before the PR and again after each interface-changing repair (co-change) — where the protocol has `/realize` cases, they stay as main has them and the closing note records that they still judge the earlier contract — their re-derivation (graders, scripted turns, oracle, observation window) is ROO-88's own unit (ROO-67 decide 41cc4259); 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 keeps the record current through review and carries `Part of ROO-67`; where the protocol chart is shared, the body names it after `Part of` as well and the PR title leaves its id out, so the merge leaves the chart open for the other runs; no merge.

Check the fork's report against the branch, CI and the decide texts before relaying it. A choice in it whose materially different alternatives remain compatible with those texts returns through step 4 before work that depends on it.

10. **Dogfood** — run the new `SKILL.md` by hand in this session on a live target, with the contributor's turns, before convergence is declared. Each mismatch, a reading the contributor disputes included → 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 grounds only the behavior and the revision it exercised, and a rehearsal — a pass with no contributor turn, which exercises no person-held closure — is not the run's runtime evidence; a later change stays unexercised until it is replayed.

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). A finding grounds a repair only through a scene, observed or derived from the contract, in the domain step 3 bounds where one of the protocol's operations fails; a failing verification or a missing termination path counts as such a failure, and a collision between clauses counts only as it surfaces in such a scene (ROO-67 decide 10e8d01c). Each finding is read against prior rounds' findings, repairs and dispositions; one that answers an earlier repair rather than the base is traced along that chain to its first addition, which is walked back, keeping what a scene still requires. A repaired obligation is exercised across the branches and consumers it affects. Each apply pass takes step 9's verify and renews step 10's evidence for any behavior it changes. 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, ask whether `origin/main` carried it, what it says is judged or recorded, and what fixes how that is shown: a Lean doc states only what is judged or recorded, and how it is shown is fixed in the prose alone, which adds no obligation the block lacks (ROO-159 decide 23cca4f0, ROO-67 decide 3cba063c). Removing text `origin/main` carried, or the only statement of either, is 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. On a shared chart each run writes its own structure delta, closing note and follow-ups, and the chart is closed with the last of its runs.

13. **Skill retrospective** — after the close, this session and an independent `/codex-plus:codex` consult each read the run's trace for where the flow sent it around and where the contributor brought something in at a gate. This session's candidates are withheld from the consult until its reading returns. The two readings are then compared, and each fused candidate is presented 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 a person's ending — withdrawing, stopping — carry no result constructor, the ending and what was taken up to it staying in the context (ROO-67 decide b5de0e8b)? Turning to other work closes nothing; routing is not a closure kind.

- **Next move** — does the hand-off stop at the delegation point the domain boundary taken at the fusion gate sets, prescribing nothing past it; does it name only the next move the person declared, with its citation, claiming nothing about how the next protocol runs, and are document edges and AI tags presented as proposals?

- **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? Tell a failed judgment apart from a carrier that cannot preserve its obligation (`premise/specification-and-judgment.md`). Keep the answer a `supports` judgment, and type only an independently grounded constraint that a demonstrated contract gap requires. A reviewer repeating an assertion is not, by itself, a demonstrated failure.

- **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?