[M4-3a] Record and ship an agent proof session (asciinema replay)

[williamdemeo]

Feeds #25 (M4-3) directly: ADR-008 conditions the portfolio's whole ordering on the AI page shipping a checkable worked example. This issue produces that example and its player.

Record a real session of an agent (Claude) driving Agda through agda-native-air to a finished proof; ship it as a self-hosted asciinema replay on the M4-3 page, annotated beat by beat.

Why

• A typechecker as dense, unfakeable reward signal, and an agent loop shaped around it — this is precisely the intersection the target roles sit at. Watching it run says more than any paragraph.
• asciinema-player is two files (JS + CSS) plus the .cast recording, all servable from this origin (https://docs.asciinema.org/manual/server/embedding/) — make offline-audit stays green by construction.
• The same recording seeds the strongest M6-4 blog-post candidate ("watch Claude prove a theorem"), and the .cast file is itself a checkable artifact, checked into the repo.

Tasks

• Choose the lemma: small enough to replay in ~60–90 seconds, real enough to be honest work (a kernel-is-a-congruence-shaped result reads well).
• Record the session (asciinema rec), trim dead air, keep the recovery-from-error beat if one occurs — that beat is the most credible part.
• Vendor asciinema-player.min.js + CSS under docs/assets/, pinned by hash like the fonts; wire the page embed.
• Annotate alongside: what the model saw, which tool it called, what the typechecker said back.
• Check the .cast into the repo next to the proof it produced; link both from the page.
• Confirm player weight is paid only on the M4-3 page.

Acceptance criteria

• [M4-3] AI for formal verification — agda-mcp, Claude Skills, agent workflows #25's "concrete worked example" criterion is satisfiable by pointing at this page.
• Replay works keyboard-only; honors reduced motion (no autoplay).
• make offline-audit green — no request leaves the origin.