docs: reflect 2026-06-02 session updates (#110/116/117/118/120/121/122/123) (#126)

- CHANGELOG: extend 2026-06-02 entry with later CI/impl/proof PRs
- README: note 4 annotated admits + Idris2 parse fixes + strict oracle
- STATE.a2ml: second 2026-06-02 session-history entry

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

.machine_readable/6a2/STATE.a2ml

@@ -77,6 +77,7 @@ note = "Promotion to C-grade dogfooding evidence requires real daily-driver use
 # 2026-04-19: .expect("TODO") anti-pattern sweep CLOSED (~512 sites); admitted=0 → admitted=1 declared; [dogfooding-status] section added; impl/rust-ffi/ deleted as duplicate; 19 per-directory READMEs landed (coverage 23% → all originally-missing addressed); Phase 4C Lean-extraction docs archived; FIFO-path race fixed; ROADMAP populated; ANCHOR + alkahest email drift fixed
 # 2026-06-01: Three-phase day — foundation (#59-#73), full sweep (#40 #47 #48 #52-#55), Option-2 (#74-#75) + license-batch SPDX sweep (#95-#102) + governance SHA-pin (#103) + changelog (#104). single_op_reversible Qed-closed (PR #67). Coq build oracle re-enabled (#55). 3 new Admitted markers surfaced → tracked as #56/#57/#58. 757 tests passing.
 # 2026-06-02: Post-merge sweep — Idris2 layer cleanup. PR #105 (RMO theorem-shape redesign, closes #60+#61), PR #106 (Idris2 build oracle, closes #70), PR #108 + #109 (10 partial markers cleared, closes #89), PR #112 (AuditEntry.proof keyword-clash rename), PR #113 (hardwareEraseIrreversible signature parse fix), PR #114 (doc refresh), PR #115 (reverseConcat closed via revAppend). PR #107 dropped codeql.yml. Branches cleaned to main-only; safedom orphan branch deleted with #111 salvage decision filed. Idris2 partial count 10 → 0, hole count 21+8 → 22.
+# 2026-06-02 (later): Governance + impl + proof followups. PR #110 (clear 2 governance reds inherited by 4 open PRs), PR #116 (doc followup gathering #112/#113/#115), PR #117 (RMO.idr overwriteIrreversible + auditTrailCompleteness type fixes), PR #118 (Idris2 build oracle flipped strict), PR #120 (#94 Gap 9 — O_NOATIME discipline + fs_pure.rs + 8 call sites + 6 unit tests; 757→764 tests), PR #121 (Cat A non-theorem redesigns, closes #119A), PR #122 (idris-verification chez symlink fix), PR #123 (equivSym Qed-closed via Data.Bool.andCommutative, 1/5 Cat B). 4 admits in proofs/coq/rmo_operations.v annotated with explicit obligations.
 
 [crg]
 grade = "C"

CHANGELOG.adoc

@@ -53,6 +53,18 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ==== Doc + housekeeping
 - Stale sweep: 4 `claude/issue-*` branches deleted post-merge (#105/#106/#108/#109 squash-merge cleanup) + 1 orphan `claude/safedom-res-stale-sweep` branch removed (PR #34 merged 2026-05-27; 3 subsequent campaign commits were superseded). Salvaged `.github/copilot/coding-agent.yml` decision filed as #111.
 - PROOF-NEEDS.md + `proofs/idris2/README.md` + ROADMAP.adoc refreshed to reflect zero `partial` count + 3-admit Coq state.
+- State refresh after the 2026-06-02 post-merge sweep (PR #114).
+- Doc followup gathering PRs #112 / #113 / #115 into a single coherent note (PR #116).
+
+==== CI follow-ups (later in the day)
+- Inherited governance reds cleared on 4 open PRs (PR #110).
+- RMO.idr `overwriteIrreversible` + `auditTrailCompleteness` type fixes (PR #117).
+- Idris2 build oracle flipped to strict (PR #118, closes #70 follow-up).
+- Implementation: `O_NOATIME` discipline landed via PR #120 (merge of the #94 Gap 9 work cited above).
+- Idris2 Category A non-theorem redesigns (PR #121, closes #119A).
+- CI: `idris-verification` install chez symlink for Ubuntu's chezscheme (PR #122).
+- Proof: `equivSym` closed via `Data.Bool.andCommutative` (PR #123, 1/5 Cat B).
+- 4 admits annotated in `rmo_operations.v` with explicit obligations; Idris2 keyword/parse fixes accompany.
 
 === Added — 2026-06-01
 

README.adoc

@@ -320,6 +320,7 @@ To reach production: Close extraction gap (Coq → OCaml verification).
 * Operations on `p1` don't affect `p2` (when `p1 ≠ p2`)
 * Composition: sequences of operations reverse correctly
 * ~478 theorem candidates proven across 6 verification systems (1 real gap + 2 axioms remain — see `docs/PROOF_HOLES_AUDIT.md`)
+* 2026-06-02 snapshot: 4 admits in `proofs/coq/rmo_operations.v` are annotated with explicit obligations; Idris2 0.8.0 keyword/parse fixes landed alongside (#112/#113/#115/#117) and the build oracle is strict (#118).
 
 === ❌ What Is NOT Guaranteed