docs(consolidate): sweep AFFIRMATION + status + handover to verified main (214a08f)

Roadmap item (4) — consolidation after #49/#50/#51 merged to main. Docs-only;
no code or proof changes.

- AFFIRMATION.adoc: re-affirmed at 214a08f / 2026-06-20. L10 -> "done (static)"
  including rung-3b cross-handler-by-presence (#50); the "I do NOT affirm" list
  reduced to the single runtime follow-on (blocked on mutable agent state) plus
  the 2 CI-only proofs (mathcomp M2 / Coquelicot E1).
- docs/status/must-intend-wish-2026-06-19.adoc -> -2026-06-20.adoc (both xrefs
  updated): gap-fill intend -> done (imports + locales + choreographies +
  functions + types + agents); rung-3b -> static done / runtime follow-on;
  proof-suite reconciled to 35/37-verified; "last 3" -> "last 2" throughout.
- docs/handover/NEXT-CLAUDE-PROMPT.md: regenerated at 214a08f; open-work list
  now leads with "build mutable agent state" (the chosen prerequisite) then the
  explicit `residue <name>` runtime half.
- STATE.a2ml + session-log: recorded the consolidation; next_action set to the
  mutable-state build.

CHANGELOG [Unreleased] was already current and is untouched.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_018CaSgNjNURC7ocsyjYh9We

Author: claude

.machine_readable/6a2/STATE.a2ml

@@ -6,9 +6,9 @@
 
 @state(version="2.0"):
 phase: "implementation"
-next_action: "User roadmap — only (4) CONSOLIDATE remains. (1) gap-fill DONE (#49 fn/type/agent dup-detect; #46 import/locale/choreography). (2) L10 rung 3b STATIC half DONE (#50, branch l10-rung3b-static); rung-3b RUNTIME half (evaluator Holding/Spent replay) still a follow-on. (3) PROOF SUITE: verified 35/37 passing locally (full runner: idris2+agda+Rocq9), manifest labels refreshed to all-37-passing this branch; M2(mathcomp)+E1(Coquelicot) CI-only by github-only network. Optional leftovers: trace{} standalone-statement parse gap; M5/M1 were stale-labelled not actually missing. CONSOLIDATE = sweep docs/AFFIRMATION/status to the verified state, fold the open branches."
-last_action: "Roadmap item 3 — PROOF SUITE GREEN verified + manifest status refresh (branch claude/proof-suite-status-refresh). Ran the FULL canonical-proof-suite-runner with the local toolchain (idris2 0.8 + agda 2.6.3 + Rocq 9.0, now awk-portable via #47): Summary 35/37 passing, 2 regressed. CRUCIAL finding: M5-yoneda.agda is NOT a stub — it's a complete 386-line self-contained Yoneda formalization that COMPILES runner-style (my earlier 'agda 0/1' was the same path/module-name trap as idris — must cd into dir + basename); likewise ~20 'not-started'-labelled rocq entries (M6-M14,S6-S10,E6-E11) actually compile+define their symbol. So the suite was far greener than the labels. Refreshed 21 not-started + 1 in-progress(M1) -> passing (verified); M2(mathcomp)+E1(Coquelicot ndim) kept prior CI-canonical passing (network-blocked locally). Did NOT regenerate REPORT/sidecars (would show M2/E1 locally-regressed; nightly CI regenerates canonical). Manifest balanced 500/500, 37 entries all passing, revision-log entry added. Prior this session: rung-3b static (#50), #49 fn/type/agent dup, #48 docs, #47 awk fix, Rocq9 local, #46/#45."
-updated: 2026-06-19T21:45:00Z
+next_action: "Roadmap (1)-(4) ALL DONE. Next substantive work = the L10 rung-3b RUNTIME half, which is blocked behind a prerequisite the user chose: BUILD MUTABLE AGENT STATE FIRST. Today an agent handler gets a COPY of state (run_agent_handler in eval.rs: env.set(name, val.clone())) with NO write-back, and there is no state-assignment statement — so a runtime residue cell has nowhere to persist across handlers. Step A: add a state-assignment statement (additive ControlStmt variant, e.g. `set <field> = <expr>` / `<field> := <expr>`) + evaluator write-back into AgentInstance.state; spec+grammar(pest<->ebnf)+tests in lockstep. Step B: explicit `residue <name>` agent-member cell (user's chosen design, refining the static half's implicit agent_residue_names presence-set) + runtime snapshot-on-`reversible as` / restore-on-`reverse` with Holding/Spent (Idris takeForReverse:Maybe is the model). This closes the once-only discipline the static half could only check by presence."
+last_action: "Roadmap item (4) CONSOLIDATE — swept AFFIRMATION.adoc, the status doc, and the next-Claude handover prompt to the verified merged state at 214a08f (branch claude/consolidate-l10-rung3b-proofsuite). #50 (rung-3b static) merged to main via admin-merge; all four recent feature branches (#49/#50/#51 + earlier) deleted on origin, no open PRs, no dangling branches. Renamed docs/status/must-intend-wish-2026-06-19.adoc -> -2026-06-20.adoc and updated both xrefs (AFFIRMATION + handover). Row sweeps: gap-fill intend -> done (imports+locales+choreographies+functions+types+agents); L10 rung-3b -> static done / runtime is the named follow-on (needs mutable state first); proof-suite labels reconciled to 35/37-verified, last 2 (M2 mathcomp + E1 Coquelicot) CI-canonical. CHANGELOG [Unreleased] already current — not touched. Prior this session: rung-3b static (#50, merged), #51 proof-suite refresh (merged), #49 fn/type/agent dup (merged), #48 docs, #47 awk fix, Rocq9 local, #46/#45."
+updated: 2026-06-20T00:18:53Z
 
 @blockers:
 - id: proof-debt

.machine_readable/session-log.txt

@@ -46,3 +46,5 @@
 
 [2026-06-19 23:57:43] Roadmap item 3 — PROOF SUITE GREEN + manifest status refresh (branch claude/proof-suite-status-refresh off main c9a9e92). Ran full canonical-proof-suite-runner with local toolchain (idris2 0.8 + agda 2.6.3 + Rocq 9.0; runner awk-portable since #47): Summary 35/37 passing, 2 regressed. KEY: M5-yoneda.agda is a COMPLETE 386-line self-contained Yoneda proof that compiles runner-style — my earlier agda 0/1 was the path/module-name trap (run from repo-root vs cd-into-dir+basename, same as idris). ~20 not-started-labelled rocq entries (M6-M14/S6-S10/E6-E11) also compile+define-symbol. Refreshed 21 not-started + 1 in-progress(M1) -> passing (sed, verified by the runner pass); M2(mathcomp) + E1(Coquelicot ndim port) kept prior CI-canonical passing (their dep sources gitlab.inria.fr/erratique.ch are 403 in this github-only env). Did NOT commit the runner-regenerated REPORT/STATUS/sidecars (they show M2/E1 as locally-regressed; nightly CI regenerates the canonical evidence with full toolchain) — reverted them. Manifest now 37/37 passing, parens 500/500 balanced, 37 entries parse, revision-log entry added, last-manifest-update bumped to 2026-06-19. Only roadmap item (4) CONSOLIDATE remains; rung-3b RUNTIME half is a separate follow-on. Pushing -> draft PR.
 [2026-06-19 23:49:09] Roadmap item 2 — L10 RUNG 3b STATIC HALF (branch claude/l10-rung3b-static off pre-#49 main). Design (chosen autonomously per user "just drive"): IMPLICIT per-agent scope, static-half-first. check_agent_decl now collects agent_residue_names (all handlers reversible-as bindings, recursive collector mirroring collect_linear_lets) BEFORE the handler loop; the per-handler named_residues isolation stays (intra-body 3a linear discipline). take_named_residue changed Result<(),String> -> 3-way enum ResidueTake{Took,AlreadySpent,NotPresent}; ReverseNamed arm: Took=ok(3a consume), AlreadySpent=in-body double-reverse error, NotPresent=ok IFF agent_residue_names.contains(target) [cross-handler presence, rung 3b] else reverse-without-residue. Key correctness: AlreadySpent (in-body double) NOT masked by agent-presence; cross-FUNCTION still rejected (functions dont populate the set); cross-handler once-only deferred to RUNTIME (firing order unknown, takeForReverse:Maybe). Verified via CLI: r1 cross-handler OK, r2 undeclared->error, r3 in-body-double->error. 3 typechecker tests + examples/cross_handler_reversibility.007 (parse+check+RUN all pass). 900 oo7-core lib pass; fmt+clippy clean. Docs lockstep: spec TYPE-SYSTEM-SPEC new 11b.6, docs/echo-residue-integration.adoc (rung-3b static landed / runtime-half still open), CHANGELOG. REMAINING: 3b runtime half (evaluator replay); roadmap (3) full suite green [write M5 agda], (4) consolidate. Pushing -> draft PR.
+
+[2026-06-20 00:18:53] Roadmap item 4 — CONSOLIDATE (branch claude/consolidate-l10-rung3b-proofsuite off main 214a08f). #50 (L10 rung-3b static half) merged to main via admin-merge (sha 214a08f); webhook confirmed merged + auto-unsubscribed. State verified: no open PRs, all recent feature branches (#46/#48/#49/#50/#51 + earlier) deleted on origin, no dangling work. Swept the three governance docs to the verified merged state: (1) AFFIRMATION.adoc re-affirmed at 214a08f / 2026-06-20 — L10 now "done (static)" incl. rung-3b cross-handler-by-presence, the "I do NOT affirm" list reduced to the single runtime follow-on (mutable state) + the 2 CI-only proofs; (2) docs/status/must-intend-wish-2026-06-19.adoc renamed -> -2026-06-20.adoc (both xrefs updated), gap-fill intend -> done (imports+locales+choreographies+functions+types+agents), rung-3b row -> static done/runtime follow-on, proof-suite reconciled to 35/37-verified; (3) docs/handover/NEXT-CLAUDE-PROMPT.md regenerated at 214a08f — open-work list now leads with "build mutable agent state" (the user-chosen prerequisite) then the explicit `residue <name>` cell runtime half, fixed last-3->last-2 proof count, added the static->explicit-cell "evolution not reopen" note. CHANGELOG [Unreleased] already current (rung-3b static, fn/type/agent dup, just gate, proof gating all present) — not touched. STATE.a2ml next_action set to the mutable-state build (Step A: state-assignment ControlStmt + eval write-back into AgentInstance.state; Step B: explicit residue cell + snapshot/restore Holding/Spent). Docs-only consolidation; no code/proof changes, so no build delta to verify.

AFFIRMATION.adoc

@@ -9,8 +9,8 @@
 | Field | Value
 
 | Repository      | `hyperpolymath/007`
-| Affirmed at     | 2026-06-19T21:43:26Z (UTC)
-| Commit affirmed | `2c52cf639cce81538970a3121af4c3a118d09f3e` (branch `main`)
+| Affirmed at     | 2026-06-20T00:18:53Z (UTC)
+| Commit affirmed | `214a08f678c9554b31e2912de8bc36d9b1190c70` (branch `main`)
 | Scope           | 007 language + canonical proof suite + RSR contractile state
 | Method          | Local verification (`just gate`, the prover suite, the A2ML/K9 validators)
 | Affirmed by     | Agent session (Claude Code), pending maintainer counter-signature
@@ -43,11 +43,15 @@ verified:
 . *Harvard architecture.* Data and control languages are separated; the
   invariant is gated by `just verify-harvard` and the EBNF↔Pest grammar guard.
 . *Kategoria type safety L1–L10.* Levels L1–L9 are enforced in the type
-  checker. *Layer 10 (reversibility)* is now integrated into the type system:
-  `reversible`/`irreversible`/`reverse` are no longer checked identically — a
-  `reverse` requires a live `Linear<Echo<T>>` echo residue, and the named form
-  `reversible as <name>` / `reverse <name>` binds and consumes a residue at
-  most once (phases 1–3a, mechanised in `proofs/idris2/EchoResidue*.idr`).
+  checker. *Layer 10 (reversibility)* is integrated into the type system at the
+  *static* level: `reversible`/`irreversible`/`reverse` are no longer checked
+  identically — a `reverse` requires a live `Linear<Echo<T>>` echo residue, the
+  named form `reversible as <name>` / `reverse <name>` binds and consumes a
+  residue at most once, and (rung 3b static, #50) a cross-handler `reverse
+  <name>` type-checks by presence of the binding somewhere in the same agent
+  (phases 1–3a + rung 3b static, mechanised in
+  `proofs/idris2/EchoResidue*.idr`). The *runtime* replay is the one remaining
+  follow-on (see below).
 . *Honest proof discipline.* No proof-bypass escape hatches (unsafe coercions,
   totality overrides, holes, unproven assumptions); proofs are `--safe`/total. Enforced
   by the `bust` contractile and the canonical-proof-suite banned-scan.
@@ -57,32 +61,41 @@ verified:
 
 The machine-checked D-gate is *partially* met and honestly labelled
 `in_progress`: 35 of 37 canonical proofs compile under a locally-installed
-Rocq 9 (plus all Idris2/Agda entries), and the suite runner is now POSIX-awk
-portable so it runs locally as well as in CI.
+Rocq 9 (plus all Idris2/Agda entries), the manifest labels were swept to that
+verified state (#51 — the prior `not-started` labels were a labelling lag, not
+missing proofs; M5-yoneda is a complete 386-line Agda proof, and ~20 Rocq
+entries already compiled), and the suite runner is now POSIX-awk portable so it
+runs locally as well as in CI. The last 2 (mathcomp M2 / Coquelicot E1) remain
+CI-canonical because their dependency sources are network-walled locally.
 
 == I do NOT affirm — what is open or blocked
 
 In the interest of honesty, the following are *not* affirmed as done:
 
-* *L10 rung 3b* (cross-handler residues carried through agent state) is
-  `declared`, not built. It is irreducibly partly runtime.
-* *Duplicate-definition coverage* extends to imports, locales, and
-  choreographies only; functions/types/agents still silently last-win on
-  redefinition.
-* *Full proof suite green* — several canonical entries are `not-started`.
+* *L10 rung 3b runtime* — the *static* half is built and merged (#50:
+  cross-handler `reverse <name>` type-checks by presence), but the *runtime*
+  replay (an evaluator actually executing the reversal log across handler
+  firings, the `Holding`/`Spent` `takeForReverse : Maybe` semantics) is not.
+  It is blocked behind a prerequisite: 007 has no *mutable agent state* yet —
+  handlers receive a copy of agent state with no write-back — so there is
+  nowhere for a residue cell to persist across handlers at runtime. Building
+  mutable agent state is the agreed next step before the runtime half.
+* *Full proof suite green* — 35/37 verified locally; the last 2 (mathcomp /
+  Coquelicot) are verified in CI only, by network policy, not by lack of
+  effort.
 * *Two environmental blocks*, owner-side, not correctness:
   ** GitHub Actions billing — cloud CI is rejected before running; PRs this
      period were admin-merged through red CI after local verification.
   ** A github-only network policy blocks `gitlab.inria.fr` / `erratique.ch` /
-     `coq.inria.fr`, so the last 3 proofs' dependency sources (mathcomp ⇒
-     hierarchy-builder ⇒ coq-elpi ⇒ elpi ⇒ menhir + cmdliner; Coquelicot)
+     `coq.inria.fr`, so the last 2 proofs' dependency sources (mathcomp M2 ⇒
+     hierarchy-builder ⇒ coq-elpi ⇒ elpi ⇒ menhir + cmdliner; Coquelicot E1)
      cannot be fetched locally. These proofs are verified in CI instead.
 * *Echidna* (high-assurance interface verification) does not exist — it is a
   named ecosystem placeholder with no spec.
 
 == Evidence
 
-* Detailed tier-by-tier status: `docs/status/must-intend-wish-2026-06-19.adoc`.
+* Detailed tier-by-tier status: `docs/status/must-intend-wish-2026-06-20.adoc`.
 * Machine-readable project state: `.machine_readable/6a2/STATE.a2ml`.
 * Session ledger: `.machine_readable/session-log.txt`.
 * Local gate: `just gate` (green at the affirmed commit, all 9 stages).
@@ -92,8 +105,8 @@ In the interest of honesty, the following are *not* affirmed as done:
 
 ____
 I affirm that, to the best of this session's verification, the statements above
-are an honest account of the repository at commit `2c52cf6` on
-2026-06-19T21:43:26Z. Hard invariants labelled *done* were checked locally;
+are an honest account of the repository at commit `214a08f` on
+2026-06-20T00:18:53Z. Hard invariants labelled *done* were checked locally;
 items labelled *in_progress*, *declared*, or *blocked* are not claimed as
 complete.
 ____
@@ -102,7 +115,7 @@ ____
 |===
 | Signatory | Detail
 
-| Agent              | Claude Code session, 2026-06-19
+| Agent              | Claude Code session, 2026-06-20
 | Maintainer         | Jonathan D.A. Jewell (hyperpolymath) — _counter-signature pending_
 | Verification basis | local `just gate` + prover suite (cloud CI billing-blocked)
 |===