docs(proof-debt): add canonical AXIOM: annotations to SafetyLemmas.idr (#163)

## Summary

Follow-up to #161 (which seeded `docs/proof-debt.md` per the estate
[Trusted-Base Reduction
Policy](https://github.com/hyperpolymath/standards/blob/main/docs/TRUSTED-BASE-REDUCTION-POLICY.adoc)
— hyperpolymath/standards#203, enforcement hyperpolymath/standards#211).

`docs/proof-debt.md` already enumerates the 5 class-(J) `believe_me`
sites in `src/abi/Boj/SafetyLemmas.idr`, so the `check-trusted-base.sh`
gate passes via the "documented in proof-debt.md" path. This PR closes
the second path: each marker now also has an inline `AXIOM:` leading
comment, the canonical keyword the script greps. The result: boj-server
satisfies **both** halves of the check, making it the fully canonical
reference implementation cited in standards#203 §"Precedent".

## Changes

- `src/abi/Boj/SafetyLemmas.idr` (38 lines, 5 sites + 1 module header):
  - `charEqSound`, `charEqSym`, `unpackLength`, `appendLengthSum`,
    `substrLengthBound` each gain an `AXIOM: <name>; class-(J) — ...`
    header line citing `docs/proof-debt.md §(c)` and the per-primitive
    `docs/backend-assurance/<primitive>.md`.
  - Module-header summary updated from "Five axiomatic believe_me" to
    use the policy vocabulary ("AXIOM-tagged", "disposition-§(c)
    NECESSARY-AXIOM").
- `PROOF-NEEDS.md`: new header note cross-linking `docs/proof-debt.md`
  (strategic-goals doc ↔ schema-conformant per-repo index) — mirrors
  the pattern from standards#213.

## Marker inventory (unchanged)

5 escape hatches, all `believe_me`, all in
`src/abi/Boj/SafetyLemmas.idr`,
all class-(J) NECESSARY AXIOM (§(c)), all externally validated under
`docs/backend-assurance/`:

| Site | Function | Disposition |
|------|----------|-------------|
| `SafetyLemmas.idr:61` | `charEqSound` | §(c) NECESSARY AXIOM |
| `SafetyLemmas.idr:68` | `charEqSym` | §(c) NECESSARY AXIOM |
| `SafetyLemmas.idr:226` | `unpackLength` | §(c) NECESSARY AXIOM |
| `SafetyLemmas.idr:236` | `appendLengthSum` | §(c) NECESSARY AXIOM |
| `SafetyLemmas.idr:246` | `substrLengthBound` | §(c) NECESSARY AXIOM |

§(a) DISCHARGED: 0. §(b) BUDGETED: 0 (the externally-validated harness
under `docs/backend-assurance/` is §(b)-style discipline applied to §(c)
items per standards#203 §"Precedent"). §(d) DEBT: 0.

## Test plan

- [ ] `bash scripts/check-trusted-base.sh .` (when the standards#211
      `trusted-base` job runs against this branch) reports
      `[OK] All 5 escape hatch(es) are documented (inline annotation or
      entry in: docs/proof-debt.md PROOF-NEEDS.md).`
- [ ] CI green on the trusted-base job specifically.
- [ ] No behavioural change in Idris2 build — `believe_me` bodies and
      signatures untouched; only doc-comments edited.

Refs: hyperpolymath/standards#203 (policy), hyperpolymath/standards#211
(enforcement), #161 (proof-debt.md seed).

🤖 Generated with [Claude Code](https://claude.com/claude-code)

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

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

Author: hyperpolymath

PROOF-NEEDS.md

@@ -1,5 +1,15 @@
 # PROOF-NEEDS.md — boj-server
 
+> **See also**: [`docs/proof-debt.md`](docs/proof-debt.md) is the
+> schema-conformant per-repo index under the estate
+> [Trusted-Base Reduction Policy](https://github.com/hyperpolymath/standards/blob/main/docs/TRUSTED-BASE-REDUCTION-POLICY.adoc)
+> (standards#203, enforcement standards#211). PROOF-NEEDS.md is the
+> *strategic-goals* narrative — full audit table, classification
+> rationale, and external-validation pointers. `docs/proof-debt.md` is
+> the *machine-checked* index that `scripts/check-trusted-base.sh`
+> greps. Keep both in sync when the marker count in
+> `src/abi/Boj/SafetyLemmas.idr` changes.
+
 ## Current State (Updated 2026-05-18)
 
 - **src/abi/Boj/**: 16 Idris2 ABI files

src/abi/Boj/SafetyLemmas.idr

@@ -6,12 +6,15 @@
 ||| proofs in SafeHTTP, SafeCORS, SafeWebSocket, SafePromptInjection,
 ||| SafeAPIKey, and Safety modules.
 |||
-||| Five axiomatic believe_me primitives are declared here. Each is
-||| class (J) — genuinely unavoidable in Idris2 0.8.0 because `Char`
-||| and `String` are opaque primitive types whose operations are
+||| Five AXIOM-tagged believe_me primitives are declared here (per the
+||| estate trusted-base reduction policy — hyperpolymath/standards#203).
+||| Each is class (J) — genuinely unavoidable in Idris2 0.8.0 because
+||| `Char` and `String` are opaque primitive types whose operations are
 ||| foreign functions with no constructors and no in-language induction
-||| principle. They are documented as principled assumptions, not
-||| unproven debt; see PROOF-NEEDS.md for the per-site audit.
+||| principle. They are documented as principled disposition-§(c)
+||| NECESSARY-AXIOM assumptions, not unproven debt; see
+||| `docs/proof-debt.md` (schema-conformant index) and `PROOF-NEEDS.md`
+||| (audit narrative) for the per-site disposition.
 |||
 |||   charEqSound       — soundness of prim__eqChar (c1 == c2 = True → c1 = c2)
 |||   charEqSym         — symmetry of prim__eqChar (x == y = y == x)
@@ -54,14 +57,19 @@ notTrueNotTrue : not True = True -> Void
 notTrueNotTrue Refl impossible
 
 ||| Primitive char equality soundness: c1 == c2 = True implies c1 = c2.
-||| Axiomatic: correctness of Idris2's prim__eqChar backend primitive.
+||| AXIOM: charEqSound; class-(J) — correctness of Idris2's prim__eqChar
+||| backend primitive. `Char` is an opaque primitive; no in-language
+||| induction principle exists in Idris2 0.8.0. See docs/proof-debt.md §(c)
+||| and docs/backend-assurance/prim__eqChar.md for external validation.
 %unsafe
 export
 charEqSound : (c1, c2 : Char) -> c1 == c2 = True -> c1 = c2
 charEqSound _ _ _ = believe_me ()
 
 ||| Helper: symmetry of Char equality.
-||| Axiomatic: symmetry of prim__eqChar on the BEAM/Chez backend.
+||| AXIOM: charEqSym; class-(J) — symmetry of prim__eqChar on the BEAM/Chez
+||| backend. Same root cause as charEqSound. See docs/proof-debt.md §(c)
+||| and docs/backend-assurance/prim__eqChar.md.
 %unsafe
 export
 charEqSym : (x, y : Char) -> (x == y) = (y == x)
@@ -212,22 +220,30 @@ allNeqImpliesNotElem {target} {xs = x :: xs'} prf with (x == target) proof xEq
 --------------------------------------------------------------------------------
 
 ||| `unpack s` has the same length as `s`.
-||| Axiomatic: prim__strToCharList preserves length (backend primitive guarantee).
+||| AXIOM: unpackLength; class-(J) — prim__strToCharList preserves length
+||| (backend primitive guarantee). `String` is opaque with no induction
+||| principle. See docs/proof-debt.md §(c) and
+||| docs/backend-assurance/prim__strToCharList.md for external validation.
 %unsafe
 export
 unpackLength : (s : String) -> length (unpack s) = length s
 unpackLength _ = believe_me ()
 
 ||| String concatenation length equals the sum of both argument lengths.
-||| Axiomatic: prim__strAppend is a backend primitive not reducible at the
-||| Idris2 type level. Established by semantics of all supported backends.
+||| AXIOM: appendLengthSum; class-(J) — prim__strAppend is a backend
+||| primitive not reducible at the Idris2 type level. Established by
+||| semantics of all supported backends. See docs/proof-debt.md §(c) and
+||| docs/backend-assurance/prim__strAppend.md for external validation.
 %unsafe
 export
 appendLengthSum : (s, t : String) -> length (s ++ t) = length s + length t
 appendLengthSum _ _ = believe_me ()
 
 ||| Substring of a string has length at most the requested count.
-||| Axiomatic: prim__strSubstr semantics — result is never longer than `len`.
+||| AXIOM: substrLengthBound; class-(J) — prim__strSubstr semantics: result
+||| is never longer than `len`. Backend primitive guarantee with no in-
+||| language proof. See docs/proof-debt.md §(c) and
+||| docs/backend-assurance/prim__strSubstr.md for external validation.
 %unsafe
 export
 substrLengthBound : (s : String) -> (start, len : Nat) -> LTE (length (substr start len s)) len