This skill should be used when choi 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 choi'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.