/rederive

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