hyperpolymath · hyperpolymath · Jun 24, 2026 · Jun 24, 2026 · Jun 24, 2026
@@ -47,7 +47,7 @@ cartridges-with-both        = 0     # no cartridge uses both paths
 exunit-tests                = 173   # 10 properties + 163 regular tests across 11 files; Phase 9 auth tests added 2026-04-25
 zig-ffi-chain-verified      = true  # boj-invoke → dlopen → libboj_health.so end-to-end tested 2026-04-25
 js-dispatch-chain-verified  = true  # JsWorkerPool → JsWorker → Deno port → mod.js handleTool
-believe-me-count            = 5     # all in SafetyLemmas.idr — 5 class (J) axioms over Idris2 primitives (charEqSound, charEqSym, unpackLength, appendLengthSum, substrLengthBound); reconciled from stale "4" framing per PROOF-NEEDS.md 2026-05-18 audit + #108 honest-framing PR. Reduced from 31 on 2026-04-12.
+believe-me-count            = 4     # all in SafetyLemmas.idr — 4 class (J) axioms over Idris2 primitives (charEqSound, unpackLength, appendLengthSum, substrLengthBound). charEqSym discharged to a constructive theorem (derived from charEqSound) — first §(a) discharge under standards#203, was 5. (The 2026-05-18 audit + #108 had reconciled a stale "4" up to a true 5; this discharge brings it to a true 4.) Reduced from 31 on 2026-04-12.
 zig-files                = 0     # all .v files removed 2026-04-12
 cartridges-available-real   = 1     # only feedback-mcp is built+verified-real (available:true). ~97 cartridges build a .so that returns {"status":"stub"}; 10 have no FFI — ALL now marked available:false (PR #196, 2026-06-05). Catalogue no longer over-claims; tests/truthfulness_check.sh gate enforces it.
 

diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md
@@ -14,6 +14,23 @@ Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 > greps. Keep both in sync when the marker count in
 > `src/abi/Boj/SafetyLemmas.idr` changes.
 
+## Discharge (2026-06-24) — `charEqSym` axiom → constructive theorem
+
+`charEqSym : (x, y : Char) -> (x == y) = (y == x)` is no longer a
+`believe_me` axiom. It is now **derived constructively from `charEqSound`**
+in `src/abi/Boj/SafetyLemmas.idr`: a `True` result forces propositional
+equality (`charEqSound`), collapsing both sides to the same expression; a
+mixed `True`/`False` split is impossible under soundness. This is the first
+**§(a) DISCHARGED** entry under the trusted-base reduction policy
+(standards#203) and drops the sanctioned class-(J) count **5 → 4**
+(`charEqSound`, `unpackLength`, `appendLengthSum`, `substrLengthBound`
+remain — all genuinely irreducible over opaque `Char`/`String` primitives).
+
+Verified locally: `cd src/abi && idris2 --typecheck boj.ipkg` → 17/17
+modules clean (Idris2 0.8.0, Chez 9.5.8). `scripts/check-trusted-base.sh`
+updated to `EXPECTED_AXIOMS=4` and passes. The dated audits below are
+retained as history; where they say "5", read "4 since 2026-06-24".
+
 ## Build Verification (2026-06-13) — full sweep, freshly built toolchain
 
 Re-verified end-to-end on a clean machine with a from-source toolchain
@@ -76,9 +93,10 @@ fails on anything else (or on axiom-count drift).
 ## Current State (Updated 2026-06-03)
 
 - **src/abi/Boj/**: 17 Idris2 ABI files
-- **Dangerous patterns**: **5** `believe_me` invocations, **all** in
+- **Dangerous patterns**: **4** `believe_me` invocations, **all** in
   `src/abi/Boj/SafetyLemmas.idr`, **all** classified `(J)` genuinely
-  unavoidable (see audit table below). `logSafeBounded` (SafeAPIKey.idr)
+  unavoidable (see audit table below; `charEqSym` was a 5th, discharged to a
+  theorem 2026-06-24). `logSafeBounded` (SafeAPIKey.idr)
   consumes these structurally and contains no direct `believe_me` —
   down from 31 historically.
   - Note: a raw `grep believe_me *.idr` returns **9** hits. 4 of these
@@ -99,12 +117,15 @@ Classification key: **(J)** genuinely unavoidable, documented as an axiom;
 | # | Site | Function | Type | Class | Rationale |
 |---|------|----------|------|-------|-----------|
 | 1 | `SafetyLemmas.idr:60` | `charEqSound` | `(c1,c2:Char) -> c1 == c2 = True -> c1 = c2` | **J ✓** | `Char` is an opaque primitive; `==` is `prim__eqChar` (foreign `Bool`). Idris2 0.8.0 has no in-language soundness principle for primitive equality. Standard, well-understood axiom. **Externally validated** via backend-assurance harness (`docs/backend-assurance/prim__eqChar.md` + BEAM property test). |
-| 2 | `SafetyLemmas.idr:67` | `charEqSym` | `(x,y:Char) -> (x == y) = (y == x)` | **J ✓** | Symmetry of `prim__eqChar`. Same reason as #1 — opaque primitive, no decision procedure to recurse on. **Externally validated** (same harness as #1). |
+| 2 | `SafetyLemmas.idr` | `charEqSym` | `(x,y:Char) -> (x == y) = (y == x)` | **DISCHARGED 2026-06-24** | ~~Symmetry of `prim__eqChar`~~ — superseded. NOT a necessary axiom: derived constructively from `charEqSound` (a `True` result forces `x = y`, collapsing both sides; mixed `True`/`False` impossible under soundness). Now a theorem in `SafetyLemmas.idr`; no longer counts against the trusted base. |
 | 3 | `SafetyLemmas.idr:218` | `unpackLength` | `length (unpack s) = length s` | **J ✓** | `unpack` = `prim__strToCharList` (foreign). `String` is opaque with no induction principle; the relation between primitive `String` length and `List Char` length is not reducible in-language. **Externally validated** via backend-assurance harness (`docs/backend-assurance/prim__strToCharList.md` + BEAM property test). |
 | 4 | `SafetyLemmas.idr:226` | `appendLengthSum` | `length (s ++ t) = length s + length t` | **J ✓** | `++` on `String` = `prim__strAppend` (foreign). Length additivity is a backend-semantics guarantee, not type-level reducible. **Externally validated** via backend-assurance harness (`docs/backend-assurance/prim__strAppend.md` + BEAM property test). |
 | 5 | `SafetyLemmas.idr:233` | `substrLengthBound` | `LTE (length (substr start len s)) len` | **J ✓** | `substr` = `prim__strSubstr` (foreign). The "result no longer than `len`" bound is a primitive-semantics guarantee with no in-language proof. **Externally validated** via backend-assurance harness (`docs/backend-assurance/prim__strSubstr.md` + BEAM property test). |
 
-**Verdict: 5/5 are class (J).** All five reduce to the same root cause:
+**Verdict (revised 2026-06-24): 4 class (J) + 1 discharged.** `charEqSym`
+(row 2) is no longer an axiom — it was found derivable from `charEqSound`
+and is now a constructive theorem (see the Discharge entry at the top of
+this file). The remaining four reduce to the same root cause:
 Idris2 treats `Char` and `String` as opaque primitive types whose
 operations are foreign functions with no constructors and no induction
 principle. There is no constructive in-language proof for any of them; a
@@ -148,19 +169,20 @@ All P1/P2 proof obligations are now closed.
 | BJ2 | Auth/credential handling — full isolation model | ✅ DONE (`CredentialIsolation.idr`) |
 | BJ3 | API contract compliance — protocol/domain coverage | ✅ DONE (`APIContractCoverage.idr`) |
 
-### Remaining axiomatic surface (5 believe_me, all in SafetyLemmas.idr)
+### Remaining axiomatic surface (4 believe_me, all in SafetyLemmas.idr)
 
-All five are class **(J)** — genuinely unavoidable in Idris2 0.8.0
+All four are class **(J)** — genuinely unavoidable in Idris2 0.8.0
 (opaque `Char`/`String` primitives, foreign-backed operations). See the
-**Axiom Audit (2026-05-18)** table above for per-site detail.
+**Axiom Audit** table above for per-site detail. (`charEqSym` was a 5th here
+until 2026-06-24, now discharged to a theorem — see the Discharge entry at
+the top of this file.)
 
 | Axiom | Site | Justification | Backend-assurance evidence |
 |-------|------|---------------|----------------------------|
-| `charEqSound` | `SafetyLemmas.idr:60` | Soundness of `prim__eqChar` — backend primitive correctness, externally validated | `docs/backend-assurance/prim__eqChar.md` + `elixir/test/backend_assurance/prim_eq_char_test.exs` |
-| `charEqSym` | `SafetyLemmas.idr:67` | Symmetry of `prim__eqChar` — backend primitive correctness, externally validated | `docs/backend-assurance/prim__eqChar.md` + `elixir/test/backend_assurance/prim_eq_char_test.exs` |
-| `unpackLength` | `SafetyLemmas.idr:218` | `prim__strToCharList` preserves length — backend primitive correctness, externally validated | `docs/backend-assurance/prim__strToCharList.md` + `elixir/test/backend_assurance/prim_str_to_char_list_test.exs` |
-| `appendLengthSum` | `SafetyLemmas.idr:226` | `prim__strAppend` length semantics — not reducible at type level, externally validated | `docs/backend-assurance/prim__strAppend.md` + `elixir/test/backend_assurance/prim_str_append_test.exs` |
-| `substrLengthBound` | `SafetyLemmas.idr:233` | `prim__strSubstr` length bound — not reducible at type level, externally validated | `docs/backend-assurance/prim__strSubstr.md` + `elixir/test/backend_assurance/prim_str_substr_test.exs` |
+| `charEqSound` | `SafetyLemmas.idr` | Soundness of `prim__eqChar` — backend primitive correctness, externally validated | `docs/backend-assurance/prim__eqChar.md` + `elixir/test/backend_assurance/prim_eq_char_test.exs` |
+| `unpackLength` | `SafetyLemmas.idr` | `prim__strToCharList` preserves length — backend primitive correctness, externally validated | `docs/backend-assurance/prim__strToCharList.md` + `elixir/test/backend_assurance/prim_str_to_char_list_test.exs` |
+| `appendLengthSum` | `SafetyLemmas.idr` | `prim__strAppend` length semantics — not reducible at type level, externally validated | `docs/backend-assurance/prim__strAppend.md` + `elixir/test/backend_assurance/prim_str_append_test.exs` |
+| `substrLengthBound` | `SafetyLemmas.idr` | `prim__strSubstr` length bound — not reducible at type level, externally validated | `docs/backend-assurance/prim__strSubstr.md` + `elixir/test/backend_assurance/prim_str_substr_test.exs` |
 
 Note: `logSafeBounded` in SafeAPIKey.idr no longer uses `believe_me` directly;
 it calls the documented SafetyLemmas axioms via structural proof.
@@ -187,8 +209,9 @@ sites stay in `SafetyLemmas.idr`. The harness shrinks the trusted base
 from "we trust the backend" to "we read the lowering and randomly
 tested the operation".
 
-Primitives validated so far: `prim__eqChar` (covering `charEqSound`
-and `charEqSym`), `prim__strToCharList` (covering `unpackLength`),
+Primitives validated so far: `prim__eqChar` (covering `charEqSound`;
+formerly also `charEqSym`, now a derived theorem), `prim__strToCharList`
+(covering `unpackLength`),
 `prim__strAppend` (covering `appendLengthSum`), and `prim__strSubstr`
 (covering `substrLengthBound`). Tracked under epic #87 Tier C
 backend-assurance campaign.
@@ -198,7 +221,7 @@ backend-assurance campaign.
 **LOW** — All named proof obligations closed. Future work:
 - Proofs for Dap/Bsp/CodeIntel domains when those cartridges reach Ready status
 - Proof that `dispatch` is surjective onto all BJ3-covered (domain, protocol) pairs
-- The 5 string/char-primitive axioms are **irreducible within Idris2**
+- The 4 string/char-primitive axioms are **irreducible within Idris2**
   (opaque primitive types). They cannot be "proved away" in-language;
   the only reduction path is to shrink the trusted base by validating
   `prim__eqChar` / `prim__strToCharList` / `prim__strAppend` /

diff --git a/docs/backend-assurance/prim__eqChar.md b/docs/backend-assurance/prim__eqChar.md
@@ -6,18 +6,24 @@ Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
 # Backend-Assurance: `prim__eqChar`
 
-Trusted-extraction validation for the two class-(J) axioms over
-Idris2's `prim__eqChar` primitive:
+Trusted-extraction validation for the class-(J) axiom over Idris2's
+`prim__eqChar` primitive:
 
 - `charEqSound : (c1, c2 : Char) -> c1 == c2 = True -> c1 = c2`
-  (`src/abi/Boj/SafetyLemmas.idr:53`)
-- `charEqSym : (x, y : Char) -> (x == y) = (y == x)`
-  (`src/abi/Boj/SafetyLemmas.idr:60`)
+  (`src/abi/Boj/SafetyLemmas.idr`)
 
-Both are `%unsafe` `believe_me` declarations in Idris2 0.8.0 because
-`Char` is an opaque primitive type with no in-language induction
+`charEqSound` is a `%unsafe` `believe_me` declaration in Idris2 0.8.0
+because `Char` is an opaque primitive type with no in-language induction
 principle. This document argues — by inspecting the backend lowerings
-that BoJ actually ships against — that the believed properties hold.
+that BoJ actually ships against — that the believed property holds.
+
+> **Note (2026-06-24):** `charEqSym : (x, y : Char) -> (x == y) = (y == x)`
+> was previously a second axiom validated here. It is now a **constructive
+> theorem** derived from `charEqSound` (see `SafetyLemmas.idr`), so it no
+> longer needs independent backend validation — its correctness rides on
+> `charEqSound` plus an in-language proof. The symmetry analysis in the
+> backend sections below is retained as corroborating context (and as the
+> validation basis should `charEqSym` ever be re-axiomatised).
 
 The companion property test
 (`elixir/test/backend_assurance/prim_eq_char_test.exs`) exercises the
@@ -124,4 +130,5 @@ matching property test.
 - R6RS §11.11 "Characters" — `char=?` specification.
 - OTP `erlang(3)` — `=:=`/`=/=` specification.
 - `PROOF-NEEDS.md` — axiom audit (2026-05-18).
-- `src/abi/Boj/SafetyLemmas.idr` — axiom declarations (lines 53, 60).
+- `src/abi/Boj/SafetyLemmas.idr` — `charEqSound` axiom declaration
+  (`charEqSym` is now a derived theorem, not an axiom).
diff --git a/docs/proof-debt.md b/docs/proof-debt.md
@@ -7,11 +7,13 @@ Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 **Schema**: [hyperpolymath/standards `TRUSTED-BASE-REDUCTION-POLICY.adoc`](https://github.com/hyperpolymath/standards/blob/main/docs/TRUSTED-BASE-REDUCTION-POLICY.adoc) (standards#203).
 
 boj-server is the **reference implementation** for the estate trusted-base
-reduction policy (cited as such in standards#203). The 5 class-J axioms
+reduction policy (cited as such in standards#203). The 4 class-J axioms
 this repo isolates in `src/abi/Boj/SafetyLemmas.idr` are the canonical
 example of disposition §(c) NECESSARY AXIOM, and the
 `docs/backend-assurance/` per-axiom files are the canonical example of
-external validation under §(b)-style discipline.
+external validation under §(b)-style discipline. (A 5th former axiom,
+`charEqSym`, was discharged to a constructive theorem on 2026-06-24 — the
+first §(a) entry below.)
 
 This `docs/proof-debt.md` is a thin schema-aligned index. The substantive
 content lives in:
@@ -26,13 +28,22 @@ content lives in:
 
 ## (a) DISCHARGED in this repo
 
-*(None — the 5 class-J axioms are genuinely unavoidable in Idris2 0.8.0.
-Items would move here if a future Idris2 version exposes in-language
-soundness principles for `Char` / `String` primitives.)*
+- **`charEqSym`** : `(x, y : Char) -> (x == y) = (y == x)` — *discharged
+  2026-06-24*. Formerly a class-J axiom; now **derived constructively from
+  `charEqSound`** in `src/abi/Boj/SafetyLemmas.idr`. Intuition: a `True`
+  result forces propositional equality via `charEqSound`, collapsing both
+  sides to the same expression; a mixed `True`/`False` split is impossible
+  under soundness. Verified by `idris2 --typecheck boj.ipkg` (Idris2 0.8.0,
+  17/17 modules clean). This is the first §(a) discharge and the reason the
+  sanctioned count dropped **5 → 4**.
+
+The remaining 4 class-J axioms are genuinely unavoidable in Idris2 0.8.0;
+they would move here only if a future Idris2 exposes in-language soundness
+principles for `Char` / `String` primitives.
 
 ## (b) BUDGETED — tested with a refutation budget
 
-The 5 axioms below are documented under §(c) (NECESSARY) rather than §(b)
+The 4 axioms below are documented under §(c) (NECESSARY) rather than §(b)
 (BUDGETED) because they cannot be discharged in-language. **However**,
 each one is *externally validated* via the
 [backend-assurance harness](./backend-assurance/) — property tests
@@ -45,34 +56,36 @@ extraction-boundary code.
 
 ## (c) NECESSARY AXIOM
 
-All 5 are class-J ("genuinely unavoidable") per
-[PROOF-NEEDS.md §Axiom Audit](../PROOF-NEEDS.md) (2026-05-18). Each
-reduces to the same root cause: Idris2 0.8.0 treats `Char` and `String`
-as opaque primitive types whose operations are foreign functions with no
-constructors and no induction principle.
+All 4 are class-J ("genuinely unavoidable") per
+[PROOF-NEEDS.md §Axiom Audit](../PROOF-NEEDS.md). Each reduces to the same
+root cause: Idris2 0.8.0 treats `Char` and `String` as opaque primitive
+types whose operations are foreign functions with no constructors and no
+induction principle. (`charEqSym` was a 5th entry here until 2026-06-24,
+now discharged — see §(a).)
 
-| # | Site | Signature | External validation |
+| # | Site (`SafetyLemmas.idr`) | Signature | External validation |
 |---|------|-----------|---------------------|
-| 1 | `src/abi/Boj/SafetyLemmas.idr:60` | `charEqSound : (c1,c2 : Char) -> c1 == c2 = True -> c1 = c2` | [`docs/backend-assurance/prim__eqChar.md`](./backend-assurance/prim__eqChar.md) |
-| 2 | `src/abi/Boj/SafetyLemmas.idr:67` | `charEqSym : (x,y : Char) -> (x == y) = (y == x)` | [`docs/backend-assurance/prim__eqChar.md`](./backend-assurance/prim__eqChar.md) |
-| 3 | `src/abi/Boj/SafetyLemmas.idr:218` | `unpackLength : length (unpack s) = length s` | [`docs/backend-assurance/prim__strToCharList.md`](./backend-assurance/prim__strToCharList.md) |
-| 4 | `src/abi/Boj/SafetyLemmas.idr:226` | `appendLengthSum : length (s ++ t) = length s + length t` | [`docs/backend-assurance/prim__strAppend.md`](./backend-assurance/prim__strAppend.md) |
-| 5 | `src/abi/Boj/SafetyLemmas.idr:233` | `substrLengthBound : LTE (length (substr start len s)) len` | [`docs/backend-assurance/prim__strSubstr.md`](./backend-assurance/prim__strSubstr.md) |
+| 1 | `charEqSound` | `(c1,c2 : Char) -> c1 == c2 = True -> c1 = c2` | [`docs/backend-assurance/prim__eqChar.md`](./backend-assurance/prim__eqChar.md) |
+| 2 | `unpackLength` | `length (unpack s) = length s` | [`docs/backend-assurance/prim__strToCharList.md`](./backend-assurance/prim__strToCharList.md) |
+| 3 | `appendLengthSum` | `length (s ++ t) = length s + length t` | [`docs/backend-assurance/prim__strAppend.md`](./backend-assurance/prim__strAppend.md) |
+| 4 | `substrLengthBound` | `LTE (length (substr start len s)) len` | [`docs/backend-assurance/prim__strSubstr.md`](./backend-assurance/prim__strSubstr.md) |
 
 Citation: see standards#203 §"Precedent" — boj-server's harness is the
 reference implementation the estate trusted-base policy directs other
 proof-bearing repos to adopt.
 
 ## (d) DEBT — actively to be closed
 
-*(None in the Idris2 ABI layer. The 5 class-J axioms above are §(c),
+*(None in the Idris2 ABI layer. The 4 class-J axioms above are §(c),
 not §(d); they are not "to be closed" — they are load-bearing
-assumptions about the trusted base.)*
+assumptions about the trusted base. `charEqSym` moved §(c) → §(a) on
+2026-06-24, not via Idris2 change but because it was found to be derivable
+from `charEqSound`.)*
 
 Future work that would generate §(d) entries:
 
 - Migration to a future Idris2 version exposing in-language soundness
-  principles for primitive types — would let entries #1–#5 move from
+  principles for primitive types — would let entries #1–#4 move from
   §(c) → §(a) via discharge.
 - New `believe_me` introduced in non-SafetyLemmas.idr files — these
   must be classified as §(a)/§(b)/§(c) before merge or land here as

diff --git a/scripts/check-trusted-base.sh b/scripts/check-trusted-base.sh
@@ -5,7 +5,7 @@
 # check-trusted-base.sh — enforce the estate trusted-base reduction policy
 # (hyperpolymath/standards#203, enforcement #211) for boj-server.
 #
-# The policy sanctions EXACTLY the 5 class-(J) axioms isolated in
+# The policy sanctions EXACTLY the 4 class-(J) axioms isolated in
 # src/abi/Boj/SafetyLemmas.idr — opaque Char/String primitives that have no
 # in-language induction principle in Idris2 0.8.0, externally validated by the
 # backend-assurance harness (docs/backend-assurance/). Every other proof in the
@@ -20,7 +20,9 @@ set -euo pipefail
 cd "$(dirname "$0")/.."
 
 AXIOM_FILE="src/abi/Boj/SafetyLemmas.idr"
-EXPECTED_AXIOMS=5
+# 4 since charEqSym was discharged to a constructive theorem (was 5); the
+# survivors are charEqSound + the three String-primitive length axioms.
+EXPECTED_AXIOMS=4
 
 echo "==> Scanning for unsound constructs outside ${AXIOM_FILE}..."
 FOUND=$(grep -rn 'believe_me\|assert_total\|assert_smaller\|idris_crash' \

diff --git a/specs/elixir-harness/.gitignore b/specs/elixir-harness/.gitignore
@@ -0,0 +1,8 @@
+# TLC model-checker run artifacts (not source)
+states/
+*_TTrace_*.tla
+*_TTrace_*.bin
+*.st
+*.fp
+MC*.tla
+MC*.cfg