diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml
index 9170490..9a4860f 100644
--- a/.machine_readable/6a2/STATE.a2ml
+++ b/.machine_readable/6a2/STATE.a2ml
@@ -6,7 +6,7 @@
 [metadata]
 project = "gossamer"
 version = "0.3.1"
-last-updated = "2026-04-25"
+last-updated = "2026-05-20"
 status = "active"  # active | paused | archived
 
 [project-context]
@@ -120,3 +120,41 @@ depends-on = ["ephapax", "idris2", "zig", "webkitgtk"]
 #             [6] integration_test.zig: 9 new tests (null handle, empty path, nonexistent .so, double-unload,
 #                 idempotent unload, empty list JSON, isPluginLoaded semantics).
 #             HANDOVER-gossamer-plugin-system.md deleted on completion.
+# 2026-05-20: standards#131 close-out — all four formerly-deferred ABI proof
+#             modules from gossamer#22 wired into gossamer-abi.ipkg. Idris2
+#             0.8.0 `--typecheck` now passes 13/13 (was 4/4 before #22; 8/9
+#             after #22; 9/9 after #36; 11/11 after #40; 13/13 after #41).
+#             Discharge PRs:
+#             - #36 GrooveTermination (MERGED): renamed local types with
+#               `Term` prefix to disambiguate from Gossamer.ABI.Groove;
+#               added impossible-clauses to `boundSuccess`/`boundFailure`
+#               for the index-absurd reject/establish branches.
+#             - #40 LayoutStability + IPCIntegrity (MERGED): module-qualified
+#               LayoutStability's concrete-record names (OWED note's `choose`
+#               hint was a misdiagnosis — lowercase-implicit-binding shadow
+#               was the real issue); reordered IPCIntegrity so VerifiedReceive
+#               + accessors precede hashPreservation, added verifiedReceipt
+#               + verifiedReceived accessors, restated hashPreservation type,
+#               marked hashPreservation and seqMonotonicity 0-quantity (the
+#               erased-witness-extraction defect surfaced only on first build);
+#               also fixed latent seqMonotonicity bug — original stated
+#               `LTE (S n) (S n)` (reflexivity) instead of `LTE n (S n)`
+#               (monotonicity).
+#             - #41 PanelIsolation + ResourceCleanup (open, ready, rebased
+#               onto post-#40 main, local idris2 ✓ 13/13): added gossamer's
+#               FIRST class-J axiom `stringNotEqCommut` (commutativity of
+#               primitive String `==`), `%unsafe`-marked + believe_me ()-bodied,
+#               documented at use site with same trust posture as boj-server
+#               `Boj.SafetyLemmas.charEqSym`; chose Option 1 (axiom) over
+#               Option 2 (Distinct-refactor) because Option 2 relocates
+#               rather than eliminates the axiom (`decEq String` is the same
+#               primitive at one more level of indirection). ResourceCleanup
+#               needed unrelated fixes (missing Data.DPair import, lowercase
+#               `exists` → `Exists` typo).
+#             PROOF-NEEDS.md updated with Class-J axioms section + Discharge
+#             ledger + the meta-lesson: OWED notes from never-built modules
+#             systematically misdiagnose root cause (4/4 in gossamer#22's
+#             list). Build is the only oracle for proof-bearing code.
+#             standards#131 CLOSED owner-authorised at the discharge point
+#             with #41 merge-pending honestly noted in the closing comment.
+#             Epic standards#124 progress: 5/12 sub-issues closed (was 4/12).
diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md
index c629631..651b926 100644
--- a/PROOF-NEEDS.md
+++ b/PROOF-NEEDS.md
@@ -14,7 +14,9 @@
 - `src/interface/abi/ResourceCleanup.idr` — Resource cleanup on teardown proofs ✅
 - `src/interface/abi/WindowStateMachine.idr` — Window state machine correctness (GS1) ✅ NEW 2026-04-11
 - `src/interface/abi/IPCDispatch.idr` — IPC handler type safety, 25 handlers (GS2) ✅ NEW 2026-04-11
-- No `believe_me`, `sorry`, `postulate`, or `assert_total` in ABI layer
+- **All 13 ABI modules above are now wired into `gossamer-abi.ipkg` and pass `idris2 0.8.0 --typecheck` cleanly** (2026-05-20, `standards#131` close-out). Prior to `gossamer#22` / `#36` / `#40` / `#41`, several modules were excluded from the ipkg and had never been built — their PROOF-NEEDS ✅ markers reflected an unverified posture; build is now the oracle.
+- **One class-J axiom**: `Gossamer.ABI.PanelIsolation.stringNotEqCommut` — sanctioned principled assumption over the Idris2 backend primitive `prim__eq_String` (content-symmetry on every supported backend; cannot be derived inside Idris2). `%unsafe`-annotated, `believe_me ()`-bodied, documented at the use site. Same trust posture as boj-server's `Boj.SafetyLemmas.charEqSym` and four sibling axioms over String / Char primitives. See "Class-J axioms (trusted base)" section below.
+- No other `believe_me`, `sorry`, `postulate`, or `assert_total` in the ABI layer.
 - Zig FFI layer in `src/interface/ffi/`
 
 ## What needs proving
@@ -32,3 +34,27 @@
 
 ## Priority
 - **LOW** — 7 of 8 proof requirements completed. Only extension loading safety remains, blocked on Ephapax module system completion.
+
+## Class-J axioms (trusted base)
+
+This repo has one class-J axiom, sanctioned and documented:
+
+| Axiom | Module | Justification | Soundness oracle |
+|---|---|---|---|
+| `stringNotEqCommut` | `Gossamer.ABI.PanelIsolation` | Commutativity of `prim__eq_String`: the Idris2 backend primitive for `String == String`. Holds on every supported backend (Chez, Racket, Node, JS — all dispatch to native string-equal which is content-symmetric). Cannot be derived inside Idris2 (opaque primitive with no constructors / induction principle). | Per-backend property-test validation (deferred to the backend-assurance harness once ported from boj-server's `project_boj_server_backend_assurance_harness`). |
+
+The axiom is `%unsafe`-marked and the function body is `believe_me ()` — explicit, named, audited; **not unproven debt**. Sites that depend on it: `PanelIsolation.distinctSym`.
+
+**Reduce-the-trusted-base path**: when gossamer adopts the backend-assurance harness, `stringNotEqCommut` can be promoted from class-J axiom to a backend-verified theorem via runtime correspondence tests against the primitive.
+
+## Discharge ledger (2026-05-20, standards#131 close-out)
+
+| Module | Discharged in | State |
+|---|---|---|
+| GrooveTermination | [gossamer#36](https://github.com/hyperpolymath/gossamer/pull/36) | **MERGED** |
+| LayoutStability | [gossamer#40](https://github.com/hyperpolymath/gossamer/pull/40) | **MERGED** |
+| IPCIntegrity | [gossamer#40](https://github.com/hyperpolymath/gossamer/pull/40) | **MERGED** |
+| PanelIsolation (+ class-J axiom) | [gossamer#41](https://github.com/hyperpolymath/gossamer/pull/41) | open, ready, idris2 ✓ 13/13 local |
+| ResourceCleanup | [gossamer#41](https://github.com/hyperpolymath/gossamer/pull/41) | same branch as #41 |
+
+**Lesson memorialised**: the OWED notes carried in the original gossamer#22 deferred-list misdiagnosed the root cause on every one of the four deferred items. The notes named `choose` / theorem restatement / axiom-vs-refactor; the actual fixes were `module-qualify the names` / `reorder + 0-quantity-mark + add accessors` / `import + capitalise the typo` / `class-J axiom` (the last one was right by accident). **Build is the only oracle for proof-bearing code; comment-only notes from never-built modules are hints, not specs.**
diff --git a/gossamer-abi.ipkg b/gossamer-abi.ipkg
index 3098b25..618d101 100644
--- a/gossamer-abi.ipkg
+++ b/gossamer-abi.ipkg
@@ -35,13 +35,18 @@ modules = Gossamer.ABI.Types
         , Gossamer.ABI.GrooveTermination
         , Gossamer.ABI.LayoutStability
         , Gossamer.ABI.IPCIntegrity
-
--- DEFERRED (owner design call — Refs standards#131). Syntactic/structural
--- defects were fixed in-tree, but each module has RESIDUAL proof/design
--- debt that is not a clean discharge. Excluded so the CI gate stays
--- green and the debt stays visible rather than silently bit-rotting:
---   * PanelIsolation / ResourceCleanup — `distinctSym` needs commutativity
---     of primitive String `==`: a sanctioned String-primitive bridge axiom
---     or refactor `Distinct` to carry `Not (a = b)`.
---      , Gossamer.ABI.PanelIsolation
---      , Gossamer.ABI.ResourceCleanup
+        , Gossamer.ABI.PanelIsolation
+        , Gossamer.ABI.ResourceCleanup
+
+-- All formerly-deferred ABI proof modules from gossamer#22's OWED list
+-- are now wired and `idris2 --typecheck` green:
+--   * GrooveTermination  — discharged in gossamer#36 (MERGED)
+--   * LayoutStability    — discharged in gossamer#40 (MERGED)
+--   * IPCIntegrity       — discharged in gossamer#40 (MERGED)
+--   * PanelIsolation     — discharged in this branch via a sanctioned
+--                           class-J axiom (`stringNotEqCommut`) over the
+--                           Idris2 backend primitive `prim__eq_String`.
+--                           First class-J axiom in gossamer; same trust
+--                           posture as boj-server's `Boj.SafetyLemmas.*`.
+--   * ResourceCleanup    — discharged in this branch (missing `Data.DPair`
+--                           import + lowercase `exists` → `Exists`).
diff --git a/src/interface/abi/PanelIsolation.idr b/src/interface/abi/PanelIsolation.idr
index e1367b1..11114fa 100644
--- a/src/interface/abi/PanelIsolation.idr
+++ b/src/interface/abi/PanelIsolation.idr
@@ -15,7 +15,11 @@
 ||| 3. Panel registries track unique panel identifiers with non-collision proof.
 ||| 4. No panel can forge another panel's state token.
 |||
-||| Zero believe_me. All proofs are constructive.
+||| One class-J axiom: `stringNotEqCommut` — commutativity of the
+||| Idris2 backend primitive `prim__eq_String`. Sanctioned principled
+||| assumption over a foreign primitive (same trust posture as
+||| boj-server's `Boj.SafetyLemmas.charEqSym`), not unproven debt. All
+||| other proofs in this module are constructive.
 
 module Gossamer.ABI.PanelIsolation
 
@@ -50,10 +54,47 @@ data Distinct : (a : PanelTag) -> (b : PanelTag) -> Type where
              -> {auto 0 prf : So (not (a == b))}
              -> Distinct a b
 
+--------------------------------------------------------------------------------
+-- Class-J axiom: String `==` commutativity (Refs standards#131 / #124)
+--------------------------------------------------------------------------------
+
+||| AXIOM (class-J): primitive String inequality is commutative.
+|||
+||| The `(==)` operator on `String` is the `Eq String` instance, which
+||| dispatches to Idris2's backend primitive `prim__eq_String`. The
+||| primitive is an opaque foreign function with no constructors and no
+||| in-language induction principle — its commutativity over content
+||| equality (`a == b` ⇔ `b == a`) holds on every supported backend
+||| (Chez, Racket, Node, JS — all dispatch to native string-equal which
+||| is content-symmetric) but cannot be derived inside Idris2 itself.
+|||
+||| Same trust posture as boj-server's `Boj.SafetyLemmas.charEqSym`
+||| (symmetry of `prim__eqChar`) and four sibling axioms over String /
+||| Char primitives. Audited as **class-(J)** — principled assumption
+||| over an Idris2 primitive, not unproven debt. See PROOF-NEEDS.md (in
+||| boj-server) for the per-site convention; this is gossamer's first
+||| class-J axiom and is documented at the use site rather than in a
+||| dedicated `SafetyLemmas` module — that module can be lifted out
+||| later if a second axiom appears.
+|||
+||| Soundness oracle: property-test validation against the runtime,
+||| per the boj-server backend-assurance harness pattern. A reduce-the-
+||| trusted-base PR can replace this axiom with a `prim__eq_String` /
+||| `prim__strEq` symmetry proof once that harness exists for gossamer.
+|||
+||| Refs: standards#131 (PanelIsolation `distinctSym`),
+||| standards#124 (proof-debt epic).
+%unsafe
+export
+stringNotEqCommut : {a, b : String} -> So (not (a == b)) -> So (not (b == a))
+stringNotEqCommut _ = believe_me ()
+
 ||| Distinctness is symmetric: if a /= b then b /= a.
+||| Constructive modulo `stringNotEqCommut` (class-J axiom above).
 public export
 distinctSym : Distinct a b -> Distinct b a
-distinctSym (MkDistinct {a} {b} {prf}) = MkDistinct {a=b} {b=a}
+distinctSym (MkDistinct {a} {b} {prf}) =
+  MkDistinct {a=b} {b=a} {prf = stringNotEqCommut prf}
 
 --------------------------------------------------------------------------------
 -- Panel-Scoped State
diff --git a/src/interface/abi/ResourceCleanup.idr b/src/interface/abi/ResourceCleanup.idr
index fef8680..6dc35af 100644
--- a/src/interface/abi/ResourceCleanup.idr
+++ b/src/interface/abi/ResourceCleanup.idr
@@ -27,6 +27,7 @@ import Data.Bits
 import Data.Nat
 import Data.List
 import Data.List.Elem
+import Data.DPair
 
 %default total
 
@@ -224,7 +225,7 @@ data ShellTeardown : Type where
 ||| Given any number of panel registries and a shell registry,
 ||| we can always produce a complete ShellTeardown.
 public export
-shellTeardownTotal : (panels : List (exists (\rs => Registry rs)))
+shellTeardownTotal : (panels : List (Exists (\rs => Registry rs)))
                    -> (shell : Registry shellRs)
                    -> ShellTeardown
 shellTeardownTotal panels shell =