chore(roadmap): tick three follow-on items — all open items closed

- [x] katagoria L11 comonad laws (believe_me → Refl)
- [x] typed-wasm DecEq (a,b) instance for WHT_Struct
- [x] protocol-squisher foldl-min optimality proof

Remaining open: WasmGC recursive types for Stdlib.idr List layout.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Author: hyperpolymath

ROADMAP.adoc

@@ -20,9 +20,10 @@ Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
 * [x] Formalise Protocol Squisher tropical connection (`protocol-squisher/proofs/tropical/`)
 * [x] katagoria: first research artefact — L11-modal-box (Idris2 sketch, MOTIVATION.adoc)
-* [ ] typed-wasm layout: prove comonad laws in L11 candidate (2 open believe_me)
+* [x] katagoria L11-modal-box: comonad laws proved (Refl after case split — believe_me-free)
+* [x] typed-wasm DecEq: `DecEq (a, b)` instance added — WHT_Struct resolution chain complete
+* [x] protocol-squisher tropical: foldl-min optimality proved (`foldl_tcAdd_le_init/mem` + `minimax_path_optimal`)
 * [ ] typed-wasm layout: model WasmGC recursive types (List self-reference in Stdlib.idr)
-* [ ] protocol-squisher tropical: prove Dijkstra correctness for min-max semiring
 * [ ] Extend `Tropical.thy`: linorder instance, tropical matrices, Kleene algebra
 * [ ] Write arXiv paper on speculative tropical session types
 * [ ] typed-wasm ABI conventions for AffineScript + Ephapax cross-language calls (pending recursive types)