diff --git a/.github/workflows/echidna-verify.yml b/.github/workflows/echidna-verify.yml
new file mode 100644
index 0000000..d5376c4
--- /dev/null
+++ b/.github/workflows/echidna-verify.yml
@@ -0,0 +1,191 @@
+# This workflow is managed by gh actions-lock.
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell and Contributors
+#
+# Echidna proof verification — type-checks proofs/theories with Agda and
+# gates the quarantined trust base against proofs/trust-base.json.
+#
+# Provenance (issue #4): ported from hyperpolymath/standards
+# .github/workflows/echidna-verify.yml job "Agda — lol/proofs", with the
+# paths rebased to this repo (proofs/theories, not lol/proofs/theories).
+# That copy there is now a presence-guard no-op because the corpus was
+# evicted here; this workflow is the authoritative gate, so unlike the
+# standards original — which downgraded failures to ::warning:: — a failed
+# type-check is a HARD failure here.
+#
+# Design notes carried from issue #4 deliberately:
+#   1. No workflow-level `paths:` filter on pull_request. If this context is
+#      ever made required, a workflow-level filter means the workflow never
+#      triggers and the required context never reports, deadlocking every
+#      PR. Change-scoping happens in the job-level `detect-proof-changes`
+#      guard, so a proof-irrelevant PR still gets a (skipped) check run.
+#   2. Never exit 0 on a missing corpus: the file count is asserted before
+#      anything is reported, so this repo cannot inherit the fail-open gate
+#      that hid the strand in standards.
+
+name: Echidna Proof Verification
+
+on:
+  push:
+    branches: [main]
+    paths:
+      - 'proofs/**'
+      - 'scripts/audit-trust-base.py'
+      - '.github/workflows/echidna-verify.yml'
+  # NO path filter on pull_request — see design note 1 above.
+  pull_request:
+  schedule:
+    # Weekly re-verification catches toolchain/stdlib drift between changes
+    # to this tree (the failure mode that made the standards copy rot).
+    - cron: '0 6 * * 1'
+  workflow_dispatch:
+
+# Estate guardrail: cancel superseded runs so re-pushes / rebased PR updates
+# do not pile up queued runs against the shared account-wide Actions
+# concurrency pool. This workflow is read-only (check + log artifact), so
+# cancelling a superseded run is always safe.
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+permissions:
+  contents: read
+
+jobs:
+  detect-proof-changes:
+    timeout-minutes: 5
+    name: Detect proof changes
+    runs-on: ubuntu-latest
+    outputs:
+      proofs: ${{ steps.check.outputs.proofs }}
+    steps:
+      - name: Checkout
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+        with:
+          fetch-depth: 0
+      - name: Did this change touch any proof source?
+        id: check
+        shell: bash
+        run: |
+          # Non-PR events (push, schedule, dispatch) always verify.
+          if [ "${{ github.event_name }}" != "pull_request" ]; then
+            echo "proofs=true" >> "$GITHUB_OUTPUT"; exit 0
+          fi
+          base="${{ github.event.pull_request.base.sha }}"
+          head="${{ github.event.pull_request.head.sha }}"
+          if ! changed=$(git diff --name-only "$base" "$head"); then
+            echo "::warning::diff failed; verifying conservatively"
+            echo "proofs=true" >> "$GITHUB_OUTPUT"; exit 0
+          fi
+          if printf '%s\n' "$changed" | grep -qE '^(proofs/|scripts/audit-trust-base\.py$|\.github/workflows/echidna-verify\.yml$)'; then
+            echo "proofs=true" >> "$GITHUB_OUTPUT"
+          else
+            echo "proofs=false" >> "$GITHUB_OUTPUT"
+          fi
+
+  agda:
+    name: Agda — proofs/theories
+    needs: detect-proof-changes
+    if: needs.detect-proof-changes.outputs.proofs == 'true'
+    runs-on: ubuntu-latest
+    timeout-minutes: 20
+    steps:
+      - name: Checkout
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+
+      - name: Install Agda + stdlib
+        run: |
+          set -euo pipefail
+          sudo apt-get update
+          sudo apt-get install -y --no-install-recommends agda agda-stdlib
+          agda --version
+
+      - name: Register stdlib for Agda
+        run: |
+          set -euo pipefail
+          mkdir -p "$HOME/.agda/libraries"
+          touch "$HOME/.agda/libraries/estate-stdlib" "$HOME/.agda/defaults"
+          found=0
+          while IFS= read -r lib; do
+            [ -n "$lib" ] || continue
+            grep -qxF "$lib" "$HOME/.agda/libraries/estate-stdlib" \
+              || echo "$lib" >> "$HOME/.agda/libraries/estate-stdlib"
+            name=$(awk '$1=="name:"{print $2; exit}' "$lib")
+            if [ -n "$name" ] && ! grep -qxF "$name" "$HOME/.agda/defaults"; then
+              echo "$name" >> "$HOME/.agda/defaults"
+            fi
+            found=1
+          done < <(find /usr/share/agda-stdlib -maxdepth 2 -name '*.agda-lib' 2>/dev/null | sort)
+          if [ "$found" != 1 ]; then
+            echo "::error::no *.agda-lib found under /usr/share/agda-stdlib — the agda-stdlib package layout changed; fix this step before trusting the gate"
+            exit 1
+          fi
+          echo "--- registered ---"
+          cat "$HOME/.agda/libraries/estate-stdlib" "$HOME/.agda/defaults"
+
+      - name: Probe stdlib visibility
+        run: |
+          set -euo pipefail
+          probe=$(mktemp -d)
+          cat > "$probe/Probe.agda" <<'EOF'
+          module Probe where
+          open import Data.Nat using (ℕ)
+          open import Data.Vec using (Vec)
+          open import Data.Float using (Float)
+          EOF
+          agda --safe "$probe/Probe.agda" >/dev/null
+          echo "stdlib probe OK (Data.Nat / Data.Vec / Data.Float resolve under --safe)"
+
+      - name: "Corpus presence (fail-closed, issue #4 note 2)"
+        run: |
+          set -euo pipefail
+          mapfile -t FILES < <(find proofs/theories -name '*.agda' | sort)
+          echo "Agda corpus files: ${#FILES[@]}"
+          printf '  %s\n' "${FILES[@]}"
+          if [ "${#FILES[@]}" -lt 1 ]; then
+            echo "::error::proofs/theories contains no .agda files — refusing to report success with an empty corpus"
+            exit 1
+          fi
+
+      - name: Type-check proofs
+        run: |
+          set -eo pipefail
+          failed=""
+          : > agda-verify.log
+          while IFS= read -r f; do
+            if grep -qE '\{-# OPTIONS[^#]*--safe' "$f"; then
+              flags="--safe --without-K"
+            else
+              flags="--without-K"
+              echo "note: $f is the quarantined trust base (compiled without --safe by design)"
+            fi
+            echo "--- checking $f ($flags) ---"
+            if ! agda $flags -i proofs/theories "$f" >> agda-verify.log 2>&1; then
+              echo "::error::agda type-check FAILED for $f"
+              failed="$failed$f"$'\n'
+              tail -n 40 agda-verify.log
+            fi
+          done < <(find proofs/theories -name '*.agda' | sort)
+          if [ -n "$failed" ]; then
+            printf 'Failed files:\n%s' "$failed"
+            exit 1
+          fi
+          echo "All Agda proofs type-checked cleanly under the enforced flags."
+
+      - name: Trust-base audit
+        run: python3 scripts/audit-trust-base.py
+
+      - name: Postulate census (advisory listing for the run log)
+        run: |
+          echo "=== Postulates in proofs/theories ==="
+          grep -rn "^\s*postulate" proofs/theories/ || echo "none"
+          echo "=== Trust tags ==="
+          grep -rn "ECHIDNA:trust" proofs/theories/ || echo "none"
+
+      - name: Upload log
+        if: always()
+        uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1
+        with:
+          name: agda-verify-log
+          path: agda-verify.log
+          if-no-files-found: ignore
diff --git a/.gitignore b/.gitignore
index 67e4698..46d6186 100644
--- a/.gitignore
+++ b/.gitignore
@@ -66,6 +66,12 @@ build/
 *.ttc
 *.ttm
 
+# Agda (interfaces + MAlta/compile artifacts emitted by `agda --safe` checks)
+*.ai
+*.agda-ir/
+/proofs/verification-results.json
+/proofs/reports/
+
 # Chapel
 *.chpl.tmp.*
 
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 3c57a96..1d0973d 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -163,13 +163,51 @@ rsr-audit:
     - if: $CI_COMMIT_BRANCH == $CI_DEFAULT_BRANCH
 
 proof-verification:
-  <<: *nix-template
   stage: verify
+  # Real type-check of the Agda corpus (issue #4 counterpart). Debian's agda +
+  # agda-stdlib match the GitHub Actions gate (apt-based, same versions).
+  # allow_failure stays true BY DESIGN: this job mirrors the gate onto the
+  # GitLab forge, but the authoritative check is
+  # .github/workflows/echidna-verify.yml; a broken mirror pipeline must not
+  # become a fake gate. Do not "fix" by deleting the script — the script is
+  # the point, the softness is the policy.
+  image: debian:bookworm-slim
+  variables:
+    DEBIAN_FRONTEND: "noninteractive"
   script:
-    - echo "Proof verification would run here"
+    - apt-get update -qq
+    - apt-get install -y -qq --no-install-recommends agda agda-stdlib python3 findutils
+    - |
+      set -eu
+      mkdir -p "$HOME/.agda/libraries"
+      touch "$HOME/.agda/libraries/estate-stdlib" "$HOME/.agda/defaults"
+      found=0
+      for lib in $(find /usr/share/agda-stdlib -maxdepth 2 -name '*.agda-lib' | sort); do
+        echo "$lib" >> "$HOME/.agda/libraries/estate-stdlib"
+        name=$(awk '$1=="name:"{print $2; exit}' "$lib")
+        [ -n "$name" ] && echo "$name" >> "$HOME/.agda/defaults"
+        found=1
+      done
+      [ "$found" = 1 ] || { echo "ERROR: no agda-stdlib .agda-lib found"; exit 1; }
+    - |
+      set -eu
+      FILES=$(find proofs/theories -name '*.agda' | sort)
+      [ -n "$FILES" ] || { echo "ERROR: empty Agda corpus under proofs/theories"; exit 1; }
+      failed=""
+      for f in $FILES; do
+        if grep -qE '\{-# OPTIONS[^#]*--safe' "$f"; then flags="--safe --without-K"; else flags="--without-K"; fi
+        echo "--- checking $f ($flags) ---"
+        agda $flags -i proofs/theories "$f" || failed="$failed $f"
+      done
+      [ -z "$failed" ] || { echo "FAILED:$failed"; exit 1; }
+    - python3 scripts/audit-trust-base.py
   allow_failure: true
   rules:
     - if: $CI_COMMIT_BRANCH == $CI_DEFAULT_BRANCH
+      changes:
+        - proofs/**
+        - scripts/audit-trust-base.py
+        - .gitlab-ci.yml
 
 # =============================================================================
 # Security Stage
diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc
index 08c80f6..8ddb168 100644
--- a/CHANGELOG.adoc
+++ b/CHANGELOG.adoc
@@ -9,6 +9,17 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 == [Unreleased]
 
 === Added
+- Agda proof verification CI (`.github/workflows/echidna-verify.yml`,
+  resolving issue #4): hard-failing `agda --safe` type-check over
+  `proofs/theories`, fail-closed corpus assertion, and a trust-base audit
+  gating `proofs/trust-base.json` against the quarantined axioms
+- Trust-quarantine layering for the Agda corpus
+  (`InformationTheory` = theorems, `Foundations` = safe definitions,
+  `Axioms` = sole non-safe `postulate` module, each axiom tagged
+  `ECHIDNA:trust`)
+- Proven theorems `entropy-nonneg` and `js-symmetric` (POSTULATE-AUDIT
+  Phase 2 items), plus `just prove-agda` / `just prove-audit` /
+  `just prove-check-all` recipes and a mirror-grade check in `.gitlab-ci.yml`
 - Complete rewrite from Python to ReScript for type safety
 - RSR Gold compliance infrastructure
 - Echidna integration for mathematical proofs
@@ -21,6 +32,15 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - AsciiDoc documentation
 
 === Changed
+- `Distribution` now carries range and normalisation hypotheses with a
+  computational float order `_≤ᶠ_` (fixes the vacuous where-clause relations
+  identified in POSTULATE-AUDIT; refutable-as-stated versions removed)
+- `proofs/README.adoc` now describes the tree that exists; removed phantom
+  references (`set_theory.agda`, `language_types.agda`, `verified/*.v`,
+  `opencyc_integration.agda`) and labelled `specs/*.spec` as unchecked
+  design sketches
+- `proofs/echidna.toml`: theory/spec lists rebased to real files;
+  `[ci] fail_on_unverified = true`
 - Migrated from Python to ReScript
 - Replaced requirements.txt with package.json
 - Switched from Apache 2.0 to MIT + Palimpsest dual license
diff --git a/Justfile b/Justfile
index 8af58b4..b96cc21 100644
--- a/Justfile
+++ b/Justfile
@@ -154,6 +154,38 @@ prove:
     @echo "Running Echidna proof verification..."
     cd proofs && echidna verify
 
+# Type-check the Agda corpus exactly like CI (.github/workflows/echidna-verify.yml).
+# Needs: apt install agda agda-stdlib  (or nix-shell -p agda agdaPackages.stdlib)
+prove-agda:
+    #!/usr/bin/env bash
+    set -euo pipefail
+    command -v agda >/dev/null 2>&1 || { echo "agda not found — install it (apt install agda agda-stdlib) first"; exit 1; }
+    failed=""
+    while IFS= read -r f; do
+      if grep -qE '\{-# OPTIONS[^#]*--safe' "$f"; then
+        flags="--safe --without-K"
+      else
+        flags="--without-K"
+        echo "note: $f is the quarantined trust base (compiled without --safe by design)"
+      fi
+      echo "--- checking $f ($flags) ---"
+      if ! agda $flags -i proofs/theories "$f"; then
+        failed="$failed$f"$'\n'
+      fi
+    done < <(find proofs/theories -name '*.agda' | sort)
+    if [ -n "$failed" ]; then
+      printf 'FAILED:\n%s' "$failed"
+      exit 1
+    fi
+    echo "All Agda proofs type-checked cleanly."
+
+# Audit the trust base (postulate quarantine vs proofs/trust-base.json)
+prove-audit:
+    python3 scripts/audit-trust-base.py
+
+# Local mirror of the CI gate: type-check + trust-base audit
+prove-check-all: prove-agda prove-audit
+
 # Check specific proof
 prove-check PROOF:
     cd proofs && echidna check {{PROOF}}
diff --git a/proofs/POSTULATE-AUDIT.adoc b/proofs/POSTULATE-AUDIT.adoc
index d2f7471..58abeaf 100644
--- a/proofs/POSTULATE-AUDIT.adoc
+++ b/proofs/POSTULATE-AUDIT.adoc
@@ -1,101 +1,128 @@
 // SPDX-License-Identifier: CC-BY-SA-4.0
 = LOL Information-Theory Postulate Audit
 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-:updated: 2026-04-05
-:target: lol/proofs/theories/information_theory.agda
+:updated: 2026-10-04
+:target: lol/proofs/theories/InformationTheory.agda (+ Foundations/Axioms)
+:manifest: lol/proofs/trust-base.json
 
-== Summary
+== Current state (2026-10-04)
 
-`information_theory.agda` contains **9 postulates**. Audit verdict:
+The corpus was rebuilt around a quarantined trust base. All postulates now
+live in exactly one module — `InformationTheory/Axioms.agda`, compiled without
+`--safe` because Agda's `--safe` rejects `postulate` (Agda test
+`SafeFlagPostulate`) — and every one of them is tagged, named, classified,
+and budget-enforced against `{manifest}` by `scripts/audit-trust-base.py` in
+CI (`.github/workflows/echidna-verify.yml`, issue #4).
 
-- **4 are legitimate FFI axioms** (float arithmetic bridged to runtime)
-- **4 are theorems that SHOULD be proven** (currently postulated)
-- **1 is a relation declaration** that should move to imports
+The audit now contains **6 postulates**:
 
-== Per-postulate verdict
+- **4 legitimate IEEE-754 `ffi-fact` axioms** (true facts about
+  correctly-rounded float ops that Agda cannot derive from opaque primitives)
+- **2 `conjecture` axioms** (Gibbs' inequality and Lin's JSD bound lifted to
+  floats — honest open debt, never used by the proven theorems)
+- **0 uninterpreted where-clause relations** — the 2026-04 correctness bug is
+  structurally impossible now (see below)
 
-[cols="3,2,3,3",options="header"]
+[cols="3,2,3,2",options="header"]
 |===
-| Postulate | Line | Verdict | Action
-
-| `log₂ : Float → Float`
-| 47
-| ✓ FFI axiom
-| Keep. Foreign float operation.
-
-| `_*f_ : Float → Float → Float`
-| 48
-| ✓ FFI axiom
-| Keep. Foreign float multiply.
-
-| `_+f_ : Float → Float → Float`
-| 49
-| ✓ FFI axiom
-| Keep. Foreign float add.
-
-| `negateF : Float → Float`
-| 50
-| ✓ FFI axiom
-| Keep. Foreign float negate.
-
-| `_/f_ : Float → Float → Float`
-| 67
-| ✓ FFI axiom
-| Keep. Foreign float divide.
-
-| `entropy-nonnegative`
-| 103
-| ✗ Provable
-| Replace with constructive proof. Each `plogp p` is either 0 or `-p·log₂(p)` where p∈[0,1] means log₂(p)≤0, so `-p·log₂(p)≥0`. Sum of non-negatives is non-negative. Requires float lemmas about `log₂` on [0,1]; add those as auxiliary postulates (honest FFI layer) but the top-level theorem should be proven.
-
-| `kl-nonnegative`
-| 109
-| ✗ Provable
-| Gibbs' inequality is a classical theorem. Proof uses Jensen's inequality on the convex function `-log`. Standard proof strategy: log-sum inequality, or expand via `x log(x/y) ≥ x - y`. Should be proven from standard real-analysis lemmas.
-
-| `js-symmetric`
-| 115
-| ✗ Trivially provable
-| By construction, JSD(P,Q) = (D(P‖M) + D(Q‖M))/2 where M = (P+Q)/2. Swap P↔Q gives the same M, so JSD(Q,P) = (D(Q‖M) + D(P‖M))/2 = JSD(P,Q). Proof is 2-3 lines in Agda.
-
-| `js-bounded`
-| 120
-| ✗ Provable (with effort)
-| Upper bound JSD ≤ log(2) requires the information-theoretic log-sum inequality. Non-trivial but classical. Should be proven or imported from an existing Agda library.
+| Axiom | Class | Statement (roughly) | Why axiom
+
+| `log₂-nonpos` | ffi-fact | 0 ≤ v ≤ 1 → log₂ v ≤ 0 (IEEE, incl. v = 0 → −∞)
+| Float `log` is a runtime primitive; no real-analysis model in scope
+| `mul-sign` | ffi-fact | a ≥ 0 ∧ b ≤ 0 → −(a·b) ≥ 0 (correctly-rounded ×)
+| Sign/rounding law of IEEE multiplication
+| `add-nonneg` | ffi-fact | a ≥ 0 ∧ b ≥ 0 → a + b ≥ 0
+| Same, for addition (no associativity is ever claimed)
+| `add-comm` | ffi-fact | a + b ≡ b + a (bitwise)
+| IEEE addition is commutative even under rounding; NaN payload propagation
+  is symmetric
+| `kl-nonneg` | conjecture | Σ p·log₂(p/q) ≥ 0 for [0,1] entries summing to 1
+| Gibbs over reals; float rounding bridge is real proof work (Phase 2 open)
+| `js-bounded` | conjecture | 0 ≤ JSD ≤ 1 (bits)
+| Lin (1991); same rounding bridge plus log-sum inequality
 |===
 
-== Additional concerns
-
-- **`_≥_` and `_≤_` declared as local where-clauses** (lines 104-105, 110-111, 121-123). These should be imported from `Data.Float.Properties` or defined module-wide, not per-postulate. Current structure means each postulate's `_≥_` is a distinct, empty relation — any value satisfies it vacuously. This is a **correctness bug**: the postulates are trivially satisfiable because the order relation is unconstrained.
-
-- **License header**: MIT AND LicenseRef-Palimpsest-0.8 (not the newer PMPL-1.0-or-later). Acceptable given attributed third-party origin (Ehsaneddin Asgari).
-
-== Remediation plan
-
-=== Phase 1 — fix the order relation bug (HIGH priority)
-
-Replace the where-clause declarations of `_≥_`/`_≤_` with a module-level import
-from a float-comparison library. Without this, the theorem statements are
-vacuous.
-
-=== Phase 2 — prove the 4 theorems
-
-Proposed order (easiest first):
-
-1. `js-symmetric` — algebraic, 2-3 lines
-2. `entropy-nonnegative` — requires auxiliary `log₂-nonpos-on-01` lemma (postulated as FFI fact)
-3. `kl-nonnegative` — requires Gibbs/log-sum lemma
-4. `js-bounded` — hardest; may require importing from an Agda analysis library
-
-=== Phase 3 — convert FFI postulates to trust-tagged axioms
-
-Add `@trust(level=axiom, prover=ffi, since=...)` inline annotations above each
-of the 5 float postulates so the innervation layer records their trust level.
+**Discharged since the 2026-04 audit** (were postulates, now theorems proven
+in `InformationTheory` using only the four `ffi-fact` axioms):
+
+* `entropy-nonneg` — per-entry guard `plogpB` + `sumF` induction +
+  `lookup-map` transport.
+* `js-symmetric` — `zipWith-comm` on the midpoint construction +
+  `add-comm`; the swap never needs associativity.
+* The five float-arithmetic postulates from the 2024 baseline
+  (`log₂`, `_*f_`, `_+f_`, `negateF`, `_/f_`) are gone entirely: those ops are
+  *defined* by re-exporting `Agda.Builtin.Float` primitives through
+  `Data.Float`, which is not postulation and was correctly never in the trust
+  base after the rebuild.
+
+== Historical: 2026-04-05 audit (pre-remediation state)
+
+`information_theory.agda` (the pre-split file) contained **9 postulates**.
+Verdicts, preserved for provenance:
+
+* 4-5 were "legitimate FFI axioms" for float ops bridged to runtime — later
+  recognised as definable via `Agda.Builtin.Float` re-exports.
+* 4 (`entropy-nonnegative`, `kl-nonnegative`, `js-symmetric`, `js-bounded`)
+  were theorems postulated rather than proven.
+* 1 was a relation *declaration* smuggled into a `where` clause.
+
+=== The correctness bug (now regression-gated)
+
+The old corpus declared `_≥_` and `_≤_` as **per-postulate `where`-clause
+relations** (`where _≥_ : Float → Float → Set`). Uninterpreted relations are
+satisfied vacuously by every pair of floats, so `entropy d ≥ 0.0` quantified
+over an empty proposition: *trivially provable, meaningfully false*. Two
+layers of gate now prevent this class:
+
+1. Agda itself: `where` clauses on `postulate` signatures don't parse, and
+   even when abused via module-level declarations, the statements over
+   unconstrained `Probability` records are **refutable** (e.g. `p = 2.0`
+   gives `−p·log₂ p < 0`, and unnormalised pairs break Gibbs). The rebuild
+   replaces the records with a `Distribution` carrying `lower`, `upper` and
+   `normalised` hypotheses expressed through the *computational* order
+   `_≤ᶠ_ := T (… ≤ᵇ …)`, so each claim evaluates against the real IEEE
+   comparison.
+2. `scripts/audit-trust-base.py` fails on any `where _≥_/_≤_ :` shape inside
+   the trust base, and on any untagged or off-manifest postulate.
+
+== License note (unchanged)
+
+The Agda corpus files carry `MIT AND LicenseRef-Palimpsest-0.8` (not the
+newer PMPL-1.0-or-later), reflecting attributed third-party origin
+(Ehsaneddin Asgari, 2024). Acceptable as-is.
+
+== Remediation ledger
+
+*Phase 1 — fix the order relation bug*: **DONE 2026-10-04.** Computational
+`_≤ᶠ_`/`_<ᶠ_`/`_≥ᶠ_` module-wide in `Foundations`; where-clause relations
+eliminated and regression-gated.
+
+*Phase 2 — prove the 4 theorems*: **PARTIAL 2026-10-04.** `js-symmetric` and
+`entropy-nonneg` are proven. `kl-nonneg` and `js-bounded` remain tagged
+`conjecture` axioms — each requires real-analysis lemmas (log-sum/Jensen)
+over a reals model plus a rounding bridge; `Probability`-style range +
+normalisation hypotheses now make their statements *true-as-stated modulo
+rounding* rather than vacuous.
+
+*Phase 3 — convert FFI postulates to trust-tagged axioms*: **DONE.** The
+audit asked for `@trust(level=axiom, prover=ffi, since=...)` annotations;
+Agda has no annotation syntax, so the mechanism is the `ECHIDNA:trust
+<class> :: <name>` line tag consumed by the audit script and enforced by
+manifest equality (`{manifest}`), which is strictly stronger than comments:
+the tag set and the source are checked for exact bi-directional match.
+
+*Phase 4 (new, from issue #4) — CI that type-checks this tree*: **DONE.**
+Workflow ported from the stranded `standards` job with its two structural
+notes applied (no workflow-level `paths:` filter on `pull_request`;
+fail-closed corpus assertion), and with the type-check made a hard failure
+rather than the advisory `::warning::` the standards copy used.
 
 == Recorded as VeriSimDB octads (once deployed)
 
-Each postulate should produce a `proof-status` octad with:
+Each postulate produces a `proof-status` octad with:
 
-- `trust_level`: `axiom` (for FFI) or `postulate` (for provable theorems)
-- `axioms_used`: list of float primitives
-- Temporal: `verified_at` = null for postulates, set for any that get proven
+- `trust_level`: `axiom` for `ffi-fact`, `postulate` for `conjecture`
+- `axioms_used`: the four `ffi-fact` names for any proven theorem
+- Temporal: `verified_at` = null while `verified` = true for proven theorems
+  (`entropy-nonneg`, `js-symmetric`); `conjecture` entries remain
+  `verified_at: null` by design.
diff --git a/proofs/README.adoc b/proofs/README.adoc
index 4c25724..63cbc93 100644
--- a/proofs/README.adoc
+++ b/proofs/README.adoc
@@ -1,91 +1,78 @@
 // SPDX-License-Identifier: CC-BY-SA-4.0
-// SPDX-FileCopyrightText: 2024-2025 Ehsaneddin Asgari and Contributors
+// SPDX-FileCopyrightText: 2024-2026 Ehsaneddin Asgari and Contributors
 = Mathematical Proofs for 1000Langs
 :toc:
 :toclevels: 3
 
 This directory contains formal mathematical proofs and specifications for the
-1000Langs corpus crawler, verified using https://github.com/hyperpolymath/echidna[Echidna].
+1000Langs corpus crawler. The Agda tree is verified with
+https://github.com/hyperpolymath/echidna[Echidna] tooling conventions and is
+type-checked in CI by
+`.github/workflows/echidna-verify.yml` (port of the job formerly stranded in
+`hyperpolymath/standards`; see issue #4).
 
-== Proof Categories
+== Verified Tree and Trust Layering
 
-=== 1. Data Integrity Proofs
-
-Proofs that ensure the integrity of crawled and stored data:
-
-* *Checksums*: Cryptographic verification of data consistency
-* *Encoding*: UTF-8 validity and normalization guarantees
-* *Idempotency*: Re-crawling produces identical results
-
-=== 2. Alignment Correctness
-
-Proofs about parallel text alignment:
-
-* *Bijection*: One-to-one mapping between verse references
-* *Transitivity*: If A aligns with B and B with C, then A aligns with C
-* *Completeness*: All verses in source appear in alignment
-
-=== 3. Statistical Properties
-
-Proofs about statistical computations:
-
-* *KL-Divergence*: Non-negativity, asymmetry properties
-* *Jensen-Shannon*: Symmetry, boundedness (0 ≤ JSD ≤ 1)
-* *Entropy*: Maximized by uniform distribution
-
-=== 4. Type Safety Guarantees
-
-Proofs derived from the ReScript type system:
-
-* *ISO 639 Codes*: Valid language code formats
-* *Verse References*: Well-formed reference structures
-* *Configuration*: Type-safe Nickel schemas
-
-== Directory Structure
+The corpus is split so that everything load-bearing checks under Agda's
+`--safe` flag, and the irreducible trust base is quarantined and audited:
 
 [source]
 ----
 proofs/
-├── theories/       # Background mathematical theories
-│   ├── information_theory.agda
-│   ├── set_theory.agda
-│   └── language_types.agda
-├── specs/          # Formal specifications
+├── theories/
+│   ├── InformationTheory.agda            # public module: theorems (agda --safe)
+│   ├── InformationTheory/
+│   │   ├── Foundations.agda              # total, postulate-free definitions (agda --safe)
+│   │   └── Axioms.agda                   # THE ONLY quarantine holding `postulate`
+├── specs/                                # design sketches (NOT yet machine-checked)
 │   ├── alignment.spec
-│   ├── crawler.spec
+│   ├── iso639.spec
 │   └── statistics.spec
-└── verified/       # Verified implementations
-    ├── kl_divergence.v
-    ├── alignment.v
-    └── iso639.v
+├── trust-base.json                       # machine-readable axiom manifest (enforced by CI)
+├── POSTULATE-AUDIT.adoc                  # human-readable audit of every axiom
+└── echidna.toml                          # multi-prover pipeline config
 ----
 
-== Using Echidna
+Rules enforced by CI (`scripts/audit-trust-base.py`, one of the workflow steps):
 
-=== Running Proofs
+* `postulate` may only appear in `InformationTheory/Axioms.agda`;
+* every axiom carries an `ECHIDNA:trust <class> :: <name>` tag and must match
+  `trust-base.json` exactly — adding, removing, renaming, or reclassifying an
+  axiom without updating the manifest and this audit fails the build;
+* every safe module must keep `{-# OPTIONS --safe ... #-}`;
+* the corpus must be non-empty (a gate with nothing to check is no gate).
 
-[source,bash]
-----
-# Verify all proofs
-just prove
+`--safe` is not decoration: since Agda 2.6.1 it rejects `postulate` outright,
+which is why the trust base is a separate non-safe module rather than
+where-clauses scattered through the theorems (the pre-2026 corpus did the
+latter, and the relations declared that way were vacuously satisfiable —
+see POSTULATE-AUDIT.adoc).
 
-# Check specific proof
-just prove-check alignment_correctness
+== What Is Proven vs. What Is Axiomatic
 
-# Generate proof obligations
-just prove-gen
-----
+*Proven in `InformationTheory`* (from IEEE-754 `ffi-fact` axioms only):
 
-=== Adding New Proofs
+* `entropy-nonneg` — H ≥ 0 for entries in [0, 1], via per-entry
+  `0·log 0 = 0` guarding and a `sumF` induction.
+* `js-symmetric` — JSD(P,Q) ≡ JSD(Q,P), from commutativity of float addition
+  and the symmetric midpoint construction.
+* Vector plumbing (`lookup-map`, `sumF-nonneg`, `zipWith-cong₂`,
+  `zipWith-comm`) and definitional sanity lemmas.
 
-1. Create specification in `specs/`
-2. Implement proof in appropriate prover syntax
-3. Add to verification pipeline in `echidna.toml`
-4. Run `just prove` to verify
+`Axioms.agda` (class `conjecture`, kept open deliberately):
 
-== Proof Obligations
+* `kl-nonneg` — Gibbs' inequality; proof over reals needs the log-sum
+  inequality plus a rounding bridge.
+* `js-bounded` — Lin (1991) bounds; same.
 
-=== Alignment Module
+== Proof Obligations (specs/ — design sketches, not checked)
+
+The `.spec` files under `specs/` are *specification sketches* written in
+Agda-like pseudo-syntax (they use a `theorem` keyword that Agda does not
+have). They are inputs to future proof work, not verified artifacts, and CI
+does not type-check them. Their intended obligations:
+
+=== Alignment Module (`specs/alignment.spec`)
 
 [cols="1,2,1"]
 |===
@@ -93,18 +80,18 @@ just prove-gen
 
 |`align_bijective`
 |Alignment creates bijective mapping
-|Pending
+|Draft spec
 
 |`align_transitive`
 |Alignment is transitive across languages
-|Pending
+|Draft spec
 
 |`coverage_monotonic`
 |Adding translations increases coverage
-|Pending
+|Draft spec
 |===
 
-=== Statistics Module
+=== Statistics Module (`specs/statistics.spec`)
 
 [cols="1,2,1"]
 |===
@@ -112,26 +99,30 @@ just prove-gen
 
 |`kl_nonnegative`
 |KL-divergence ≥ 0
-|Pending
+|Axiom (`kl-nonneg`) — provable over reals, open over Float
 
 |`kl_zero_identical`
-|KL(P\|\|P) = 0
-|Pending
+|KL(P‖P) = 0
+|Not formalised yet
 
 |`js_symmetric`
-|JSD(P\|\|Q) = JSD(Q\|\|P)
-|Pending
+|JSD(P‖Q) = JSD(Q‖P)
+|*Proven* (`js-symmetric`)
 
 |`js_bounded`
 |0 ≤ JSD ≤ 1
-|Pending
+|Axiom (`js-bounded`)
 
 |`entropy_maximum`
 |H(uniform) = log(n)
-|Pending
+|Not formalised yet
+
+|`entropy_nonnegative`
+|H ≥ 0
+|*Proven* (`entropy-nonneg`)
 |===
 
-=== ISO 639 Module
+=== ISO 639 Module (`specs/iso639.spec`)
 
 [cols="1,2,1"]
 |===
@@ -139,23 +130,53 @@ just prove-gen
 
 |`code_format_valid`
 |All codes match regex patterns
-|Pending
+|Draft spec
 
 |`conversion_injective`
 |ISO 639-1 → 639-3 is injective
-|Pending
+|Draft spec
 
 |`special_codes_disjoint`
 |Special codes don't overlap regular codes
-|Pending
+|Draft spec
 |===
 
-== Integration with OpenCyc
+== Running the Checks Locally
 
-Proofs can leverage OpenCyc's common-sense reasoning for:
+[source,bash]
+----
+# Install the toolchain (matches the apt pin used by CI):
+sudo apt-get install -y agda agda-stdlib
+
+# Type-check the corpus exactly like CI + run the trust-base audit:
+just prove-check-all
 
-* Language family relationships
-* Geographic constraints on language distribution
-* Script compatibility with language features
+# Individual steps:
+just prove-agda     # agda --safe / --without-K over proofs/theories
+just prove-audit    # trust-base.json ⇄ source manifest gate
+
+# Echidna pipeline (requires the echidna tool; CI does not depend on it):
+just prove          # echidna verify
+just prove-gen      # generate proof obligations
+----
 
-See `theories/opencyc_integration.agda` for details.
+== Adding New Proofs
+
+1. Put total definitions in `InformationTheory/Foundations.agda` (or a new
+   `*/Foundations`-style safe module).
+2. If — and only if — a fact is genuinely unprovable in Agda over its
+   primitives, add it to `InformationTheory/Axioms.agda` with an
+   `ECHIDNA:trust ffi-fact :: <name>` (IEEE-754 true fact) or
+   `ECHIDNA:trust conjecture :: <name>` tag, update `trust-base.json` and
+   `POSTULATE-AUDIT.adoc` in the same PR, and add the file to
+   `theories`/`safe_modules` lists as appropriate.
+3. Register the module in `proofs/trust-base.json` (CI fails on any unlisted
+   `.agda` file).
+4. Run `just prove-check-all`.
+
+== Integration with OpenCyc (planned, not present)
+
+Earlier revisions of this README promised `theories/opencyc_integration.agda`
+and a `verified/` directory of Coq proofs; those files never landed and the
+references are removed. OpenCyc-based common-sense grounding remains a
+planned feature — see `../FUTURE.adoc` — with no formal artifacts to claim.
diff --git a/proofs/echidna.toml b/proofs/echidna.toml
index fe9b41b..30ff4c6 100644
--- a/proofs/echidna.toml
+++ b/proofs/echidna.toml
@@ -16,8 +16,15 @@ primary = ["agda", "coq"]
 fallback = ["lean", "z3"]
 
 [provers.agda]
+# Matches the apt-pinned toolchain used by .github/workflows/echidna-verify.yml
+# (ubuntu-latest: Agda 2.6.4.3 + stdlib 1.7.2). Bump deliberately, in lockstep
+# with the workflow if the runner image moves.
 version = "2.6.4"
 stdlib = true
+# `--safe` applies to every module EXCEPT the quarantined trust base
+# (theories/InformationTheory/Axioms.agda, which holds the ECHIDNA:trust
+# postulates and is checked with --without-K only). The split is enforced by
+# scripts/audit-trust-base.py; see proofs/README.adoc.
 flags = ["--safe", "--without-K"]
 
 [provers.coq]
@@ -44,20 +51,21 @@ cache = true
 cache_dir = ".echidna-cache"
 
 [specifications]
-# Specification files to verify
+# Specification sketches — design inputs, NOT yet machine-checked
+# (they use Agda-like pseudo-syntax, e.g. a `theorem` keyword Agda lacks).
 files = [
   "specs/alignment.spec",
-  "specs/crawler.spec",
   "specs/statistics.spec",
   "specs/iso639.spec",
 ]
 
 [theories]
-# Background theories to load
+# Background theories to load (files that exist; see proofs/README.adoc for
+# the Foundations/Axioms quarantine layout and the trust-base manifest)
 files = [
-  "theories/information_theory.agda",
-  "theories/set_theory.agda",
-  "theories/language_types.agda",
+  "theories/InformationTheory.agda",
+  "theories/InformationTheory/Foundations.agda",
+  "theories/InformationTheory/Axioms.agda",
 ]
 
 [output]
@@ -92,7 +100,8 @@ concepts = [
 ]
 
 [ci]
-# CI/CD integration
-fail_on_unverified = false
+# CI/CD integration. fail_on_unverified must stay true — the standards-era
+# gate fail-opened precisely because unverified was tolerated (issue #4).
+fail_on_unverified = true
 min_coverage = 0.8
 report_format = "junit"
diff --git a/proofs/theories/InformationTheory.agda b/proofs/theories/InformationTheory.agda
new file mode 100644
index 0000000..b4b0cdb
--- /dev/null
+++ b/proofs/theories/InformationTheory.agda
@@ -0,0 +1,132 @@
+-- SPDX-License-Identifier: MIT AND LicenseRef-Palimpsest-0.8
+-- SPDX-FileCopyrightText: 2024-2026 Ehsaneddin Asgari and Contributors
+--
+-- Information Theory — theorems
+-- =============================
+-- The public module of the LOL information-theory formalisation
+-- (1000Langs/ReScript side keeps its own property tests; this tree is the
+-- machine-checked companion).
+--
+-- Layering (enforced by .github/workflows/echidna-verify.yml, issue #4):
+--
+--   InformationTheory.Foundations   --safe   total, postulate-free definitions
+--   InformationTheory.Axioms        not safe  the only quarantine holding `postulate`
+--   InformationTheory (this module) --safe   theorems + public surface
+--
+-- The two theorems POSTULATE-AUDIT classified as "provable" (`entropy-nonneg`,
+-- `js-symmetric`) are proven here — from the four IEEE-754 `ffi-fact` axioms,
+-- never from the `conjecture` class. `kl-nonneg` and `js-bounded` remain
+-- tagged conjectures (Phase 2 open), re-exported so dependents see the
+-- trust level.
+{-# OPTIONS --safe --without-K #-}
+
+module InformationTheory where
+
+open import Data.Bool.Base using (Bool; true; false; T)
+open import Data.Float using (Float; _+_; _÷_; _≤ᵇ_; _≡ᵇ_)
+open import Data.Fin using (Fin; zero; suc)
+open import Data.Nat using (ℕ)
+open import Data.Product using (_×_; _,_)
+open import Data.Vec using (Vec; []; _∷_; map; zipWith; lookup)
+open import Data.Unit.Base using (tt)
+open import Relation.Binary.PropositionalEquality
+  using (_≡_; refl; sym; trans; cong; cong₂; subst)
+
+open import InformationTheory.Foundations public
+open import InformationTheory.Axioms
+  using (log₂-nonpos; mul-sign; add-nonneg; add-comm; kl-nonneg; js-bounded)
+  public
+
+-- ============================================================================
+-- Vector plumbing
+-- ============================================================================
+
+lookup-map : ∀ {n} (f : Float → Float) (xs : Vec Float n) (i : Fin n) →
+             lookup (map f xs) i ≡ f (lookup xs i)
+lookup-map f []       ()
+lookup-map f (x ∷ xs) zero    = refl
+lookup-map f (x ∷ xs) (suc i) = lookup-map f xs i
+
+-- The float sum of a vector is non-negative when all entries are.
+sumF-nonneg : ∀ {n} (xs : Vec Float n) →
+              (∀ {i : Fin n} → 0.0 ≤ᶠ lookup xs i) → 0.0 ≤ᶠ sumF xs
+sumF-nonneg []       h = tt
+sumF-nonneg (x ∷ xs) h =
+  add-nonneg x (sumF xs) (h {zero}) (sumF-nonneg xs λ { {i} → h {suc i} })
+
+-- Pointwise equality transports through zipWith, and a commutative pointwise
+-- function makes zipWith itself symmetric in its arguments.
+zipWith-cong₂ : ∀ {n} (f g : Float → Float → Float) →
+                (∀ x y → f x y ≡ g x y) →
+                (xs ys : Vec Float n) →
+                zipWith f xs ys ≡ zipWith g xs ys
+zipWith-cong₂ f g h []       []       = refl
+zipWith-cong₂ f g h (x ∷ xs) (y ∷ ys) = cong₂ _∷_ (h x y) (zipWith-cong₂ f g h xs ys)
+
+zipWith-comm : (f : Float → Float → Float) →
+               (∀ x y → f x y ≡ f y x) →
+               ∀ {n} (xs ys : Vec Float n) →
+               zipWith f xs ys ≡ zipWith f ys xs
+zipWith-comm f h []       []       = refl
+zipWith-comm f h (x ∷ xs) (y ∷ ys) = cong₂ _∷_ (h x y) (zipWith-comm f h xs ys)
+
+-- ============================================================================
+-- Entropy is non-negative (H ≥ 0 for p ∈ [0,1], per-entry 0·log 0 = 0)
+-- ============================================================================
+
+-- Per-entry fact: the guarded −v·log₂ v is non-negative on [0,1].
+plogpB-nonneg : (v : Float) → 0.0 ≤ᶠ v → v ≤ᶠ 1.0 →
+                (b : Bool) → 0.0 ≤ᶠ plogpB v b
+plogpB-nonneg v lv lu true  = tt
+plogpB-nonneg v lv lu false = mul-sign v (log₂ v) lv (log₂-nonpos v lv lu)
+
+plogp-nonneg : (v : Float) → 0.0 ≤ᶠ v → v ≤ᶠ 1.0 → 0.0 ≤ᶠ plogp v
+plogp-nonneg v lv lu = plogpB-nonneg v lv lu (v ≡ᵇ 0.0)
+
+entropy-nonneg : ∀ {n} (d : Distribution n) → 0.0 ≤ᶠ entropy d
+entropy-nonneg {n} d =
+  sumF-nonneg (map plogp (values d)) λ { {i} →
+    subst (0.0 ≤ᶠ_) (sym (lookup-map plogp (values d) i))
+      (plogp-nonneg (lookup (values d) i) (lower d {i}) (upper d {i})) }
+
+-- ============================================================================
+-- Jensen-Shannon divergence is symmetric
+-- ============================================================================
+
+midpointF-comm : ∀ x y → midpointF x y ≡ midpointF y x
+midpointF-comm x y = cong (λ w → w ÷ 2.0) (add-comm x y)
+
+-- JSD(P,Q) = (D(P‖M) + D(Q‖M))/2 with M = (P+Q)/2. Swapping P and Q leaves M
+-- fixed up to commutativity of float addition, then the two KL terms swap.
+js-symmetric : ∀ {n} (p q : Distribution n) →
+               jensen-shannon p q ≡ jensen-shannon q p
+js-symmetric {n} p q = cong (λ w → w ÷ 2.0) (trans swapKL rezip)
+  where
+    pv qv : Vec Float n
+    pv = values p
+    qv = values q
+
+    mm : zipWith midpointF pv qv ≡ zipWith midpointF qv pv
+    mm = zipWith-comm midpointF midpointF-comm pv qv
+
+    swapKL : kl-divergenceF pv (zipWith midpointF pv qv)
+               + kl-divergenceF qv (zipWith midpointF pv qv)
+             ≡ kl-divergenceF qv (zipWith midpointF pv qv)
+               + kl-divergenceF pv (zipWith midpointF pv qv)
+    swapKL = add-comm _ _
+
+    rezip : kl-divergenceF qv (zipWith midpointF pv qv)
+              + kl-divergenceF pv (zipWith midpointF pv qv)
+            ≡ kl-divergenceF qv (zipWith midpointF qv pv)
+              + kl-divergenceF pv (zipWith midpointF qv pv)
+    rezip = cong₂ _+_ (cong (kl-divergenceF qv) mm) (cong (kl-divergenceF pv) mm)
+
+-- ============================================================================
+-- Sanity of the definitions themselves (no axioms used)
+-- ============================================================================
+
+-- The zero-guard on the KL term agrees with the 0·log convention at p = 0:
+-- `0.0 ≡ᵇ 0.0` computes to true, so the term reduces.
+klTerm-zero-left : ∀ q → klTerm 0.0 q ≡ 0.0
+klTerm-zero-left q = refl
+
diff --git a/proofs/theories/InformationTheory/Axioms.agda b/proofs/theories/InformationTheory/Axioms.agda
new file mode 100644
index 0000000..68bf3ee
--- /dev/null
+++ b/proofs/theories/InformationTheory/Axioms.agda
@@ -0,0 +1,71 @@
+-- SPDX-License-Identifier: MIT AND LicenseRef-Palimpsest-0.8
+-- SPDX-FileCopyrightText: 2024-2026 Ehsaneddin Asgari and Contributors
+--
+-- Information Theory — quarantined trust base
+-- ============================================
+-- This is the ONLY module in the corpus allowed to contain `postulate`.
+-- It is deliberately compiled WITHOUT `--safe` (Agda's --safe rejects
+-- postulates outright — test/Fail/SafeFlagPostulate in the Agda tree), so
+-- the quarantine is enforced mechanically by
+-- .github/workflows/echidna-verify.yml (issue #4):
+--
+--   * `grep postulate` outside this file is a hard CI failure;
+--   * every postulate declaration carries an `ECHIDNA:trust <class> :: <name>`
+--     tag on the line above it;
+--   * names, classes and counts must match proofs/trust-base.json exactly
+--     (see scripts/audit-trust-base.py and proofs/POSTULATE-AUDIT.adoc).
+--
+-- Classes:
+--   ffi-fact     — a true property of correctly-rounded IEEE-754 operations
+--                  that Agda cannot derive from its opaque Float primitives.
+--                  Removing this file's --safe flag is what admits them; the
+--                  theorems that consume them are still fully checked.
+--   conjecture   — a classical theorem over the reals (Gibbs' inequality,
+--                  Lin's JSD bound) whose float-lifted form is trusted modulo
+--                  rounding; never discharged, only referenced.
+--
+-- The vacuous per-postulate `where _≥_/_≤_` relations of the original corpus
+-- (POSTULATE-AUDIT "Additional concerns") are gone: all statements below use
+-- the computational `InformationTheory.Foundations` order `_≤ᶠ_`.
+{-# OPTIONS --without-K #-}
+
+module InformationTheory.Axioms where
+
+open import Data.Bool.Base using (T)
+open import Data.Float using (Float; _+_; _*_; _÷_; -_; _≤ᵇ_; _≡ᵇ_; _<ᵇ_)
+open import Data.Product using (_×_)
+open import Relation.Binary.PropositionalEquality using (_≡_)
+
+open import InformationTheory.Foundations
+
+postulate
+  -- log₂ is non-positive on [0,1]: 0 ≤ v ≤ 1 → log₂ v ≤ 0. True including
+  -- v = 0 (log 0 = −∞ ≤ 0) and v = NaN (hypothesis is `T false`, i.e. ⊥).
+  -- ECHIDNA:trust ffi-fact :: log₂-nonpos
+  log₂-nonpos : (v : Float) → 0.0 ≤ᶠ v → v ≤ᶠ 1.0 → log₂ v ≤ᶠ 0.0
+
+  -- Sign law of correctly-rounded multiplication: a ≥ 0 ∧ b ≤ 0 → −(a·b) ≥ 0.
+  -- ECHIDNA:trust ffi-fact :: mul-sign
+  -- a > 0 excludes 0·(−∞) = NaN.
+  mul-sign : (a b : Float) → 0.0 <ᶠ a → b ≤ᶠ 0.0 → 0.0 ≤ᶠ - (a * b)
+
+  -- Non-negative floats are closed under correctly-rounded addition.
+  -- ECHIDNA:trust ffi-fact :: add-nonneg
+  add-nonneg : (a b : Float) → 0.0 ≤ᶠ a → 0.0 ≤ᶠ b → 0.0 ≤ᶠ a + b
+
+  -- Correctly-rounded addition is commutative as a bitwise operation (only
+  -- associativity fails IEEE-754). Consumed by js-symmetric.
+  -- ECHIDNA:trust ffi-fact :: add-comm
+  add-comm : (a b : Float) → a + b ≡ b + a
+
+  -- Gibbs' inequality lifted to float sums. Kept a conjecture on purpose:
+  -- the real-analysis proof (log-sum inequality over reals) plus a rounding
+  -- bridge is out of scope; see POSTULATE-AUDIT remediation Phase 2.
+  -- ECHIDNA:trust conjecture :: kl-nonneg
+  kl-nonneg : ∀ {n} (p q : Distribution n) → 0.0 ≤ᶠ kl-divergence p q
+
+  -- Lin (1991): 0 ≤ JSD ≤ 1 in bits, lifted to float arithmetic. Same
+  -- rationale as kl-nonneg.
+  -- ECHIDNA:trust conjecture :: js-bounded
+  js-bounded : ∀ {n} (p q : Distribution n) →
+    0.0 ≤ᶠ jensen-shannon p q × jensen-shannon p q ≤ᶠ 1.0
diff --git a/proofs/theories/InformationTheory/Foundations.agda b/proofs/theories/InformationTheory/Foundations.agda
new file mode 100644
index 0000000..a17fb64
--- /dev/null
+++ b/proofs/theories/InformationTheory/Foundations.agda
@@ -0,0 +1,129 @@
+-- SPDX-License-Identifier: MIT AND LicenseRef-Palimpsest-0.8
+-- SPDX-FileCopyrightText: 2024-2026 Ehsaneddin Asgari and Contributors
+--
+-- Information Theory — computational foundations
+-- ==============================================
+-- Every definition the `InformationTheory` theorems quantify over, as
+-- total postulate-free Agda. Trusted facts (IEEE-754 float properties and
+-- the two open information-theoretic conjectures) live in
+-- `InformationTheory.Axioms`, the single quarantined trust base.
+--
+-- This module is checked with `--safe` by
+-- .github/workflows/echidna-verify.yml (issue #4); adding a `postulate`
+-- here is rejected by Agda itself.
+{-# OPTIONS --safe --without-K #-}
+
+module InformationTheory.Foundations where
+
+open import Data.Bool.Base using (Bool; true; false; T; if_then_else_)
+open import Data.Float public
+  using (Float; _+_; _*_; _÷_; -_; log; _≤ᵇ_; _≡ᵇ_; _<ᵇ_)
+open import Data.Fin using (Fin)
+open import Data.Nat using (ℕ)
+open import Data.Vec using (Vec; []; _∷_; map; zipWith; lookup)
+open import Relation.Binary.PropositionalEquality using (_≡_)
+
+-- ============================================================================
+-- Order relations on Float — honest and non-vacuous
+-- ============================================================================
+-- Each proposition is `T` applied to the runtime comparison primitive, so it
+-- computes to a decidable claim about IEEE-754 values (`T true = ⊤`,
+-- `T false = ⊥`). This replaces the pre-2026 corpus's per-postulate
+-- `where _≥_ : Float → Float → Set` declarations, which were uninterpreted
+-- relations satisfied vacuously by every pair of floats. See
+-- proofs/POSTULATE-AUDIT.adoc ("Additional concerns").
+
+infix 4 _≤ᶠ_ _≥ᶠ_ _<ᶠ_
+
+_≤ᶠ_ : Float → Float → Set
+x ≤ᶠ y = T (x ≤ᵇ y)
+
+_<ᶠ_ : Float → Float → Set
+x <ᶠ y = T (x <ᵇ y)
+
+_≥ᶠ_ : Float → Float → Set
+x ≥ᶠ y = y ≤ᶠ x
+
+-- ============================================================================
+-- Logarithms and per-entry terms
+-- ============================================================================
+
+-- log base 2, via the float primitives (ln x / ln 2).
+log₂ : Float → Float
+log₂ v = log v ÷ log 2.0
+
+-- −p·log₂ p with the usual 0·log 0 = 0 convention. The zero-test result is
+-- an explicit Boolean argument so downstream theorems can case-analyse it
+-- without stuck with-abstraction on a Float primitive; `plogp` is the entry
+-- point used in definitions.
+plogpB : Float → Bool → Float
+plogpB v b = if b then 0.0 else - (v * log₂ v)
+
+plogp : Float → Float
+plogp v = plogpB v (v ≡ᵇ 0.0)
+
+-- p·log₂(p/q) for KL terms, guarding p = 0 (the q = 0 case legitimately
+-- yields +∞ rather than a special value).
+klTermB : Float → Float → Bool → Float
+klTermB p q b = if b then 0.0 else p * log₂ (p ÷ q)
+
+klTerm : Float → Float → Float
+klTerm p q = klTermB p q (p ≡ᵇ 0.0)
+
+-- Pointwise (P + Q)/2, the JSD midpoint construction.
+midpointF : Float → Float → Float
+midpointF x y = (x + y) ÷ 2.0
+
+-- ============================================================================
+-- Sums and distributions
+-- ============================================================================
+
+-- Right-associated fold over a vector of floats; observationally equal to
+-- `Data.Vec.foldr (λ _ → Float) _+_ 0.0` but shaped for induction.
+sumF : ∀ {n} → Vec Float n → Float
+sumF []       = 0.0
+sumF (x ∷ xs) = x + sumF xs
+
+-- A distribution over n outcomes: every entry lies in [0, 1] as decided by
+-- the float comparison primitives (which exclude NaN, since NaN fails every
+-- comparison), and the float sum is exactly 1.0. These hypotheses make the
+-- theorems in `InformationTheory` true statements — the pre-2026 corpus had
+-- unconstrained `Probability` records and was refutable (e.g. p = 2.0 makes
+-- −p·log₂ p < 0, and unnormalised p/q trivially breaks Gibbs).
+record Distribution (n : ℕ) : Set where
+  constructor mkDist
+  field
+    values     : Vec Float n
+    lower      : ∀ {i : Fin n} → 0.0 ≤ᶠ lookup values i
+    upper      : ∀ {i : Fin n} → lookup values i ≤ᶠ 1.0
+    normalised : sumF values ≡ 1.0
+
+-- Projections (and `mkDist`) into scope for the definitions below and for
+-- consumers that re-export this module.
+open Distribution public
+
+-- ============================================================================
+-- Divergences
+-- ============================================================================
+
+-- Shannon entropy: H(X) = −Σ p(x) log₂ p(x), bits.
+entropy : ∀ {n} → Distribution n → Float
+entropy {n} d = sumF (map plogp (values d))
+
+-- KL-divergence on raw vectors: D(P‖Q) = Σ p·log₂(p/q).
+kl-divergenceF : ∀ {n} → Vec Float n → Vec Float n → Float
+kl-divergenceF ps qs = sumF (zipWith klTerm ps qs)
+
+-- KL-divergence on distributions.
+kl-divergence : ∀ {n} → Distribution n → Distribution n → Float
+kl-divergence p q = kl-divergenceF (values p) (values q)
+
+-- Jensen-Shannon divergence on raw vectors: with M = (P + Q)/2,
+-- JSD = (D(P‖M) + D(Q‖M))/2.
+jsdF : ∀ {n} → Vec Float n → Vec Float n → Float
+jsdF ps qs = ((kl-divergenceF ps m) + (kl-divergenceF qs m)) ÷ 2.0
+  where m = zipWith midpointF ps qs
+
+-- Jensen-Shannon divergence on distributions.
+jensen-shannon : ∀ {n} → Distribution n → Distribution n → Float
+jensen-shannon p q = jsdF (values p) (values q)
diff --git a/proofs/theories/information_theory.agda b/proofs/theories/information_theory.agda
deleted file mode 100644
index 54c1281..0000000
--- a/proofs/theories/information_theory.agda
+++ /dev/null
@@ -1,140 +0,0 @@
--- SPDX-License-Identifier: MIT AND LicenseRef-Palimpsest-0.8
--- SPDX-FileCopyrightText: 2024-2025 Ehsaneddin Asgari and Contributors
---
--- Information Theory Foundations
--- ==============================
--- Agda formalization of information-theoretic concepts
-
-{-# OPTIONS --safe --without-K #-}
-
-module InformationTheory where
-
-open import Data.Nat using (ℕ; zero; suc)
-open import Data.Float using (Float)
-open import Agda.Builtin.Float
-  using (primFloatLog; primFloatTimes; primFloatPlus; primFloatNegate; primFloatDiv)
-open import Data.Vec using (Vec; []; _∷_; map; zipWith; foldr)
-open import Data.Product using (_×_; _,_)
-open import Relation.Binary.PropositionalEquality using (_≡_; refl)
-
--- ============================================================================
--- Basic Definitions
--- ============================================================================
-
--- Non-negative real (approximated as Float for computation)
-ℝ⁺ : Set
-ℝ⁺ = Float
-
--- Probability value [0, 1]
-record Probability : Set where
-  constructor mkProb
-  field
-    value : Float
-    -- Invariants would be proven separately
-
--- Probability distribution over n outcomes
-record Distribution (n : ℕ) : Set where
-  constructor mkDist
-  field
-    probabilities : Vec Probability n
-
--- ============================================================================
--- Entropy
--- ============================================================================
-
--- Shannon entropy: H(X) = -Σ p(x) log₂ p(x)
--- Uses convention that 0 log 0 = 0
-
--- Float arithmetic: defined via Agda.Builtin.Float primitives.
-log₂ : Float → Float
-log₂ x = primFloatDiv (primFloatLog x) (primFloatLog 2.0)
-
-_*f_ : Float → Float → Float
-_*f_ = primFloatTimes
-
-_+f_ : Float → Float → Float
-_+f_ = primFloatPlus
-
-negateF : Float → Float
-negateF = primFloatNegate
-
-plogp : Probability → Float
-plogp p = let v = Probability.value p in
-  if v == 0.0 then 0.0
-  else negateF (v *f log₂ v)
-
-entropy : ∀ {n} → Distribution n → Float
-entropy (mkDist ps) = foldr (λ _ → Float) _+f_ 0.0 (map plogp ps)
-
--- ============================================================================
--- KL-Divergence
--- ============================================================================
-
--- KL-Divergence: D_KL(P||Q) = Σ P(i) log(P(i)/Q(i))
-
-_/f_ : Float → Float → Float
-_/f_ = primFloatDiv
-
-kl-term : Probability → Probability → Float
-kl-term p q =
-  let pv = Probability.value p
-      qv = Probability.value q
-  in if pv == 0.0 then 0.0
-     else pv *f log₂ (pv /f qv)
-
-kl-divergence : ∀ {n} → Distribution n → Distribution n → Float
-kl-divergence (mkDist ps) (mkDist qs) =
-  foldr (λ _ → Float) _+f_ 0.0 (zipWith kl-term ps qs)
-
--- ============================================================================
--- Jensen-Shannon Divergence
--- ============================================================================
-
--- Midpoint of two distributions
-midpoint-prob : Probability → Probability → Probability
-midpoint-prob p q = mkProb ((Probability.value p +f Probability.value q) /f 2.0)
-
-midpoint : ∀ {n} → Distribution n → Distribution n → Distribution n
-midpoint (mkDist ps) (mkDist qs) = mkDist (zipWith midpoint-prob ps qs)
-
--- JSD: (D_KL(P||M) + D_KL(Q||M)) / 2
-jensen-shannon : ∀ {n} → Distribution n → Distribution n → Float
-jensen-shannon p q =
-  let m = midpoint p q
-  in (kl-divergence p m +f kl-divergence q m) /f 2.0
-
--- ============================================================================
--- Theorems (Postulated — justified mathematical axioms over Float)
--- ============================================================================
--- These are known theorems of information theory (Shannon, Gibbs, Lin 1991).
--- They cannot be proven directly over Agda's Float (IEEE 754 approximation);
--- proofs would require a real-analysis formalisation (e.g. over ℝ).
--- Classified as justified postulates, not proof debt.
-
--- Entropy is non-negative (H ≥ 0 follows from -p·log(p) ≥ 0 for 0 ≤ p ≤ 1)
--- AXIOM: justified theorem over IEEE-754 Float; proof requires a real-analysis model.
-postulate
-  entropy-nonnegative : ∀ {n} (d : Distribution n) → entropy d ≥ 0.0
-    where
-      _≥_ : Float → Float → Set
-
--- KL-divergence is non-negative (Gibbs' inequality / log-sum inequality)
--- AXIOM: justified Gibbs inequality over Float; proof requires a real-analysis model.
-postulate
-  kl-nonnegative : ∀ {n} (p q : Distribution n) → kl-divergence p q ≥ 0.0
-    where
-      _≥_ : Float → Float → Set
-
--- Jensen-Shannon is symmetric (follows from symmetry of KL terms in the midpoint construction)
--- AXIOM: justified by the symmetric midpoint construction and paired KL terms.
-postulate
-  js-symmetric : ∀ {n} (p q : Distribution n) →
-    jensen-shannon p q ≡ jensen-shannon q p
-
--- Jensen-Shannon is bounded [0, 1] (Lin 1991; upper bound via Jensen's inequality)
--- AXIOM: justified Lin bound over Float; proof requires a real-analysis model.
-postulate
-  js-bounded : ∀ {n} (p q : Distribution n) →
-    0.0 ≤ jensen-shannon p q × jensen-shannon p q ≤ 1.0
-    where
-      _≤_ : Float → Float → Set
diff --git a/proofs/trust-base.json b/proofs/trust-base.json
new file mode 100644
index 0000000..002f43e
--- /dev/null
+++ b/proofs/trust-base.json
@@ -0,0 +1,29 @@
+{
+  "comment": [
+    "Machine-readable trust-base manifest for proofs/theories (issue #4).",
+    "Enforced by scripts/audit-trust-base.py, which runs in CI",
+    "(.github/workflows/echidna-verify.yml) and via `just prove-audit`.",
+    "Any change to the Agda corpus postulates, modules, or --safe status",
+    "must land in the same PR as the matching change here and an entry in",
+    "proofs/POSTULATE-AUDIT.adoc."
+  ],
+  "schema": 1,
+  "quarantine": "proofs/theories/InformationTheory/Axioms.agda",
+  "safe_modules": [
+    "proofs/theories/InformationTheory.agda",
+    "proofs/theories/InformationTheory/Foundations.agda"
+  ],
+  "axioms": [
+    { "name": "log₂-nonpos", "class": "ffi-fact" },
+    { "name": "mul-sign", "class": "ffi-fact" },
+    { "name": "add-nonneg", "class": "ffi-fact" },
+    { "name": "add-comm", "class": "ffi-fact" },
+    { "name": "kl-nonneg", "class": "conjecture" },
+    { "name": "js-bounded", "class": "conjecture" }
+  ],
+  "class_budget": {
+    "ffi-fact": 4,
+    "conjecture": 2
+  },
+  "total_budget": 6
+}
diff --git a/scripts/audit-trust-base.py b/scripts/audit-trust-base.py
new file mode 100644
index 0000000..150106c
--- /dev/null
+++ b/scripts/audit-trust-base.py
@@ -0,0 +1,193 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell and Contributors
+"""
+audit-trust-base.py — gate the quarantined Agda trust base (issue #4).
+
+Single implementation shared by .github/workflows/echidna-verify.yml and
+`just prove-audit`. Exits non-zero (with ::error:: annotations for Actions)
+when the corpus and proofs/trust-base.json disagree in ANY direction, so a
+postulate can be neither smuggled in nor silently deleted from the audit.
+
+Checks:
+  1.  Every *.agda under proofs/theories is listed in the manifest as either
+      the quarantine module or a safe module (no unregistered files).
+  2.  `postulate` may only occur in the quarantine file.
+  3.  Safe modules carry `--safe`; the quarantine file must NOT claim it
+      (Agda's --safe rejects postulates, so the claim would be dishonest
+      tooling rather than a sound split).
+  4.  Every postulate declaration is preceded (within one comment line) by an
+      `-- ECHIDNA:trust <class> :: <name>` tag whose name matches the
+      declaration, class is in {ffi-fact, conjecture}, and the whole set
+      (names, per-class counts, total) equals the manifest exactly.
+  5.  Regression guard for the 2026-04 soundness bug: no per-postulate
+      `where _≥_/_≤_ : Float → Float → Set`-style vacuous relation clauses.
+  6.  Non-empty corpus (fail-closed, issue #4 note 2).
+"""
+
+import json
+import re
+import sys
+from pathlib import Path
+
+REPO_ROOT = Path(__file__).resolve().parent.parent
+THEORIES = REPO_ROOT / "proofs" / "theories"
+MANIFEST = REPO_ROOT / "proofs" / "trust-base.json"
+ALLOWED_CLASSES = {"ffi-fact", "conjecture"}
+
+POSTULATE_RE = re.compile(r"^\s*postulate(\s|$)")
+DECL_RE = re.compile(r"^\s+(\S+)\s+:")
+TAG_RE = re.compile(r"^\s*--\s*ECHIDNA:trust\s+(\S+)\s+::\s+(\S+)\s*$")
+VACUOUS_RE = re.compile(r"^\s+_[≥≤]_\s*:")
+
+errors: list[str] = []
+
+
+def err(msg: str) -> None:
+    errors.append(msg)
+    print(f"::error::{msg}")
+
+
+def rel(p: Path) -> str:
+    return p.relative_to(REPO_ROOT).as_posix()
+
+
+def main() -> int:
+    if not MANIFEST.is_file():
+        err(f"missing manifest {rel(MANIFEST)}")
+        return 1
+    manifest = json.loads(MANIFEST.read_text(encoding="utf-8"))
+
+    agda_files = sorted(THEORIES.rglob("*.agda")) if THEORIES.is_dir() else []
+    if not agda_files:
+        err("no .agda corpus under proofs/theories — a gate with nothing to "
+            "check is no gate (fail-closed per issue #4 note 2)")
+        return 1
+
+    quarantine = manifest.get("quarantine")
+    safe_modules = manifest.get("safe_modules", [])
+    expected = manifest.get("axioms", [])
+    class_budget = manifest.get("class_budget", {})
+    total_budget = manifest.get("total_budget")
+
+    listed = set(map(str, [quarantine] + list(safe_modules)))
+    on_disk = {rel(p) for p in agda_files}
+    unlisted = on_disk - listed
+    missing = listed - on_disk
+    if unlisted:
+        err(f".agda file(s) not registered in {rel(MANIFEST)}: "
+            f"{sorted(unlisted)} — add to safe_modules (or extend the "
+            f"quarantine deliberately) in the same PR")
+    if missing:
+        err(f"manifest lists files that do not exist: {sorted(missing)}")
+
+    qpath = REPO_ROOT / quarantine if quarantine else None
+    if qpath and qpath.is_file():
+        qtext = qpath.read_text(encoding="utf-8")
+        if "--safe" in (re.search(r"\{-# OPTIONS[^\n]*", qtext).group(0)
+                        if re.search(r"\{-# OPTIONS[^\n]*", qtext) else ""):
+            err(f"{rel(qpath)}: quarantine must not declare --safe "
+                "(Agda rejects postulates under --safe)")
+
+        # --tag → declaration pairing, and per-declaration postulate-block walk
+        lines = qtext.splitlines()
+        found: dict[str, str] = {}
+        in_postulate = False
+        for i, line in enumerate(lines):
+            if POSTULATE_RE.match(line):
+                in_postulate = True
+                continue
+            if line.strip() == "" or line.lstrip().startswith("--"):
+                continue
+            if in_postulate and (line.startswith((" ", "\t"))):
+                m = DECL_RE.match(line)
+                if m:
+                    name = m.group(1)
+                    # find tag: nearest preceding non-blank comment line pair
+                    j = i - 1
+                    while j >= 0 and lines[j].strip() == "":
+                        j -= 1
+                    tag = TAG_RE.match(lines[j]) if j >= 0 else None
+                    if not tag:
+                        err(f"{rel(qpath)}:{i + 1}: postulate `{name}` is not "
+                            f"tagged — add `-- ECHIDNA:trust <class> :: {name}` "
+                            f"directly above it")
+                    else:
+                        cls, tname = tag.group(1), tag.group(2)
+                        if tname != name:
+                            err(f"{rel(qpath)}:{i + 1}: tag names `{tname}` "
+                                f"but declares `{name}`")
+                        if cls not in ALLOWED_CLASSES:
+                            err(f"{rel(qpath)}:{i + 1}: class `{cls}` not in "
+                                f"{sorted(ALLOWED_CLASSES)}")
+                        if name in found:
+                            err(f"duplicate postulate `{name}`")
+                        found[name] = cls
+                    if VACUOUS_RE.match(lines[i + 1] if i + 1 < len(lines) else ""):
+                        err(f"{rel(qpath)}:{i + 2}: `where _≥_/_≤_ : ...` — "
+                            f"vacuous relation regression (2026-04 audit bug)")
+                continue
+            if in_postulate and not line.startswith((" ", "\t")):
+                in_postulate = False
+        for i, line in enumerate(lines):
+            if VACUOUS_RE.match(line):
+                err(f"{rel(qpath)}:{i + 1}: vacuous where-relation "
+                    f"(2026-04 audit regression)")
+    else:
+        err(f"quarantine file missing: {quarantine}")
+
+    # postulate keyword may not appear outside the quarantine
+    for p in agda_files:
+        if qpath and p == qpath:
+            continue
+        for n, line in enumerate(p.read_text(encoding="utf-8").splitlines(), 1):
+            if re.match(r"^\s*postulate(\s|$)", line):
+                err(f"{rel(p)}:{n}: `postulate` outside the trust-base "
+                    f"quarantine ({quarantine})")
+
+    # safe modules must claim --safe
+    for name in safe_modules:
+        spath = REPO_ROOT / name
+        if not spath.is_file():
+            continue  # already reported via `missing`
+        s = spath.read_text(encoding="utf-8")
+        opts = re.findall(r"\{-#\s*OPTIONS([^#]*)#-\}", s)
+        if not any(re.search(r"(^|\s)--safe(\s|$)", o) for o in opts):
+            err(f"{name}: safe module must carry `--safe` in its OPTIONS pragma")
+
+    # manifest ⇄ source set equality
+    exp = {a["name"]: a["class"] for a in expected}
+    if set(exp) != set(found):
+        only_src = sorted(set(found) - set(exp))
+        only_man = sorted(set(exp) - set(found))
+        if only_src:
+            err(f"postulates not in manifest: {only_src}")
+        if only_man:
+            err(f"manifest entries absent from source: {only_man}")
+    for name in sorted(set(exp) & set(found)):
+        if exp[name] != found[name]:
+            err(f"`{name}`: class `{found[name]}` in source but "
+                f"`{exp[name]}` in manifest")
+    per_class: dict[str, int] = {}
+    for cls in found.values():
+        per_class[cls] = per_class.get(cls, 0) + 1
+    for cls, cap in class_budget.items():
+        if per_class.get(cls, 0) != cap:
+            err(f"class `{cls}`: source has {per_class.get(cls, 0)}, manifest "
+                f"budget is {cap} — adjust proofs/trust-base.json AND "
+                f"POSTULATE-AUDIT.adoc together")
+    if total_budget is not None and len(found) != total_budget:
+        err(f"total postulates: source has {len(found)}, budget is "
+            f"{total_budget}")
+
+    if errors:
+        print(f"trust-base audit: FAILED ({len(errors)} problem(s))")
+        return 1
+    print(f"trust-base audit: OK — {len(found)} postulate(s) in quarantine "
+          f"({', '.join(f'{c}={n}' for c, n in sorted(per_class.items()))}), "
+          f"{len(safe_modules)} safe module(s), {len(agda_files)} .agda file(s) total")
+    return 0
+
+
+if __name__ == "__main__":
+    sys.exit(main())