chore(governance): clear 12 trusted-base false-positive escape hatches

The estate's check-trusted-base.sh (standards#203) flagged 12 markers on
main since #112 (2026-05-28) — all 12 are detector-pattern false
positives, structurally identical to the believe_me FP audit recorded
in docs/PROOF-NEEDS.md §"believe_me audit (2026-05-18)" (21 hits, zero
real escapes).

Resolution:

* 10 Rust hits across 4 files are pattern-detector tables. Each holds a
  `Vec<DangerousPattern>` (or equivalent) that *enumerates* the very
  `unsafePerformIO` / `unsafeCoerce` / `Obj.magic` strings the scanner
  is hunting. The scanner's naive substring grep can't tell "uses the
  pattern" from "names the pattern in a detector table". Added a new
  `.trusted-base-ignore` (whole-path exemption, format mirrors the
  scanner's documented spec) covering the four files:
    - src/rust/verification/axiom_tracker.rs
    - crates/echidna-core-spark/src/axiom_tracker.rs
    - src/rust/corpus/agda.rs
    - src/rust/corpus/idris2.rs

* 2 Agda postulates are real well-justified axioms:
    - `funext` (function extensionality) in proofs/agda/Basic.agda
    - `Conflicts` (abstract parameter) in proofs/agda/SoundnessPreservation.agda
  Both already had INTENTIONAL AXIOM / INTENTIONAL PARAMETER prose
  documentation, but outside the script's 5-line preceding-marker
  window. Added an `-- AXIOM:` / `-- TRUSTED:` magic-word line
  immediately before each `postulate` so the scanner sees it.

Effect: `governance / Trusted-base reduction policy` should now report
[OK] (12 markers exempted via .trusted-base-ignore + inline magic), up
from the 12/12 undocumented failure on main.

Refs: #92 (broader baseline failures, this PR addresses the
trusted-base slice only).

Author: hyperpolymath

.trusted-base-ignore

@@ -0,0 +1,36 @@
+# .trusted-base-ignore — whole-path exemptions for the trusted-base scanner
+# (hyperpolymath/standards check-trusted-base.sh).
+#
+# Format: each non-comment, non-blank line is a path-fragment substring that
+# exempts every marker whose file path contains the fragment.
+#
+# Use sparingly. Per-site `TRUSTED:`/`AXIOM:` comments remain the preferred
+# mechanism for one-off documented escapes; this file is for whole-path
+# exemptions where the file's *entire purpose* is to talk about the patterns
+# the scanner detects (so every occurrence is a string literal, not a use).
+
+# ─────────────────────────────────────────────────────────────────────────────
+# Pattern-detector tables (NOT uses of the patterns themselves)
+# ─────────────────────────────────────────────────────────────────────────────
+# Each of the files below holds a `Vec<DangerousPattern>` (or equivalent)
+# that enumerates the very `unsafePerformIO`/`unsafeCoerce`/`believe_me`
+# string literals the scanner is hunting for. The scanner's naive
+# substring grep cannot distinguish "uses the pattern" from "names the
+# pattern in a detector table", so every entry shows up as a false
+# positive. Same FP class as the `\bbelieve_me\b` Idris2 audit recorded
+# in docs/PROOF-NEEDS.md §"believe_me audit (2026-05-18)".
+#
+# These files are the *implementation* of the trust-pipeline's
+# axiom-tracker — they're proof infrastructure, not proof escapes.
+src/rust/verification/axiom_tracker.rs
+crates/echidna-core-spark/src/axiom_tracker.rs
+
+# ─────────────────────────────────────────────────────────────────────────────
+# Hazard-classification helpers in the corpus extractor (NOT uses)
+# ─────────────────────────────────────────────────────────────────────────────
+# `corpus/agda.rs::collect_hazards` and `corpus/idris2.rs::collect_hazards`
+# each run a single-line `if text.contains("unsafePerformIO" / "unsafeCoerce"
+# / "Obj.magic")` to flag corpus entries that *contain* those patterns.
+# Same FP class — the substring is a hazard sentinel, not an escape hatch.
+src/rust/corpus/agda.rs
+src/rust/corpus/idris2.rs

proofs/agda/Basic.agda

@@ -174,6 +174,7 @@ module CurryUncurryLaws where
   -- major proof assistants (Coq's Functional Extensionality, Lean's
   -- funext, HoTT axiom). It does NOT compromise soundness.
   -- See: HoTT Book, Section 2.9; nLab "function extensionality"
+  -- AXIOM: funext (see justification above; recognised by check-trusted-base.sh)
   postulate
     funext : {A B : Set} {f g : A → B}
            → ((x : A) → f x ≡ g x)

proofs/agda/SoundnessPreservation.agda

@@ -48,6 +48,8 @@ record Proof : Set where
 -- In practice ECHIDNA computes this via the danger-level tracker
 -- (verification/axioms.rs): two axiom sets conflict when one contains
 -- an axiom that the other marks Reject.
+-- TRUSTED: Conflicts is an abstract parameter (see above), not an unsound
+-- escape — the caller discharges it with a concrete proof.
 postulate
   Conflicts : List Axiom → List Axiom → Set
   -- ^ INTENTIONAL PARAMETER — "Conflicts" is domain knowledge about