verify-prose: check inline / value claims; bump checkout v4 → v7

[nandanito]

Closes both open items left after lesson 04 (#13).

1. Inline claims are now verified

verify-prose checked output blocks only. Lesson 01 states almost every output as a trailing / 2f comment, so it was nearly uncovered — 1 block against 18 such claims. Now 49 blocks and 37 inline claims across lessons 01–04.

A comment counts as a claim only when it opens with something shaped like a q literal (2f, -7h, 00011b, `a`b`c, 0 1 3 6 10, ,`qty), optionally followed by prose. Prose-only comments assert nothing and are skipped — lesson 04 has 14 commented q lines and 0 claims, which is a useful built-in control that the classifier doesn't over-trigger.

The obvious design was the wrong one. Executing the README's own q lines looks natural — they're complete expressions — but prototyping killed it. Lessons legitimately contain ```q blocks that error by design (lesson 01's fork parse failure, lesson 04's s-fail/u-fail demos), so running the README aborts. And lesson 01 deliberately re-shows an earlier result out of execution order — 10 again, when (+/) is introduced as the mechanism under sum — so order-checking inline claims would flag good writing.

The first working version passed its own negative control by accident. Membership testing — "the claimed value appears somewhere in the capture" — caught 2 of 3 deliberate corruptions. The miss: flipping lesson 02's type d annotation from 99h to 98h, which passes because 98h is a real value elsewhere in that same lesson. A wrong claim that collides with a genuine value is exactly the wrong claim a reader would believe.

So claims are re-evaluated instead: each expression appended to the lesson's own verify-clean q source, where the narrative's state (d, t, kt, r, w) already exists. The deliberate error demos are never appended, because their comments are prose rather than values.

All three corruptions now fail, naming both sides:

lessons/02-dict-to-table/README.md:38: WRONG CLAIM — `type d` is annotated '98h' but evaluates to '99h'.

A containment check is not an equality check, and it fails precisely on the inputs where the two differ. Three corruptions was also the smallest control set that could have exposed this — one would have passed and been called proof.

2. actions/checkout v4 → v7

v4 runs on deprecated Node 20 (the warning on #13's run). Checked first that v7's fork-PR hardening targets pull_request_target and workflow_run, which neither workflow uses — j-verify is pull_request, q-verify is schedule/dispatch/push-to-main.

Verification

make verify green end to end — six legs, exit 0 — on KDB-X CE 5.0 and J 9.7.1. This PR is also the first real exercise of the v7 bump, since j-verify runs on it.

🤖 Generated with Claude Code