docs(soundness): TRUSTED: annotate 5 code_safety scanner fixtures (#352)

## Summary
- Adds inline `TRUSTED:` leading comments to the 5 deliberate scanner
fixtures under `test/soundness/fixtures/code_safety/` (admitted.v,
sorry.lean, agda_postulate.agda, believe_me.idr, unsafe_coerce.hs).
- Satisfies the trusted-base reduction policy
(hyperpolymath/standards#203) inline-annotation path (b) — companion to
docs enumeration in #343 (path d/initial seed).
- Classifies these 5 sites as PROPERTY-TEST (§(b) BUDGETED): each
fixture exists so that `test/soundness_test.exs` can regression-test
that the corresponding `code_safety/*` rule fires. The soundness test
suite IS the refutation budget.
- Step B of the P1 proof-debt cleanup template (one PR per cluster — all
5 are scanner fixtures, one cluster).

## Why this is content-safe
The added comments live *above* the trigger line. The marker pattern
(`Admitted.`, `sorry`, `postulate`, `believe_me`, `unsafeCoerce`) is
preserved verbatim. `test/soundness_test.exs` still fires on every
fixture (verified by the existing test suite).

## Test plan
- [ ] `mix test --only soundness` continues to pass (every fixture still
triggers its rule at the expected severity).
- [ ] `bash /path/to/standards/scripts/check-trusted-base.sh .` reports
the 5 canonical sites as satisfied via inline annotation (no longer
needs docs/proof-debt.md substring match to pass).
- [ ] No other CI regressions.

## Related
- #343 — initial seed of `docs/proof-debt.md` (count-correction revision
pushed in parallel).
- standards#195 — estate proof-debt audit.
- standards#203 — trusted-base reduction policy.
- standards#211 — `check-trusted-base.sh` CI enforcement.

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

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

Author: hyperpolymath

test/soundness/fixtures/code_safety/admitted.v

@@ -2,6 +2,9 @@
 (* SOUNDNESS FIXTURE — known-bad sample for code_safety/admitted. *)
 (* DO NOT FIX. *)
 
+(* TRUSTED: this `Admitted.` is a deliberate scanner fixture covered  *)
+(* by test/soundness_test.exs (rule `code_safety/admitted` must fire   *)
+(* on this file). Refutation budget = the soundness test suite.       *)
 Theorem bad : 1 + 1 = 3.
 Proof.
   Admitted.

test/soundness/fixtures/code_safety/agda_postulate.agda

@@ -2,5 +2,8 @@
 -- SOUNDNESS FIXTURE — known-bad sample for code_safety/agda_postulate.
 -- DO NOT FIX.
 
+-- TRUSTED: this `postulate` is a deliberate scanner fixture covered by
+-- test/soundness_test.exs (rule `code_safety/agda_postulate` must fire
+-- on this file). Refutation budget = the soundness test suite.
 postulate
   bad : Set

test/soundness/fixtures/code_safety/believe_me.idr

@@ -4,5 +4,8 @@
 
 module Soundness.BelieveMe
 
+-- TRUSTED: this `believe_me` is a deliberate scanner fixture covered
+-- by test/soundness_test.exs (rule `code_safety/believe_me` must fire
+-- on this file). Refutation budget = the soundness test suite.
 bad : Nat
 bad = believe_me Z

test/soundness/fixtures/code_safety/sorry.lean

@@ -2,4 +2,7 @@
 -- SOUNDNESS FIXTURE — known-bad sample for code_safety/sorry.
 -- DO NOT FIX.
 
+-- TRUSTED: this `sorry` is a deliberate scanner fixture covered by
+-- test/soundness_test.exs (rule `code_safety/sorry` must fire on this
+-- file). Refutation budget = the soundness test suite.
 theorem bad : 1 + 1 = 3 := by sorry

test/soundness/fixtures/code_safety/unsafe_coerce.hs

@@ -6,5 +6,8 @@ module Soundness.UnsafeCoerce where
 
 import Unsafe.Coerce
 
+-- TRUSTED: this `unsafeCoerce` is a deliberate scanner fixture covered
+-- by test/soundness_test.exs (rule `code_safety/unsafe_coerce` must
+-- fire on this file). Refutation budget = the soundness test suite.
 bad :: Int -> String
 bad n = unsafeCoerce n