diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md
index 654b26c2..a081d4d6 100644
--- a/.claude/CLAUDE.md
+++ b/.claude/CLAUDE.md
@@ -43,7 +43,7 @@ Hypatia                       # 133 Elixir modules total
 
 ## Key Commands
 
-`just` is the primary entry point (39 recipes; `CONTRIBUTING.md` treats it as canonical):
+`just` is the primary entry point (43 recipes, `just --summary | wc -w`; `CONTRIBUTING.md` treats it as canonical):
 
 ```bash
 just --list           # every recipe
@@ -172,6 +172,7 @@ Training pipeline reads outcomes/*.jsonl for ESN (confidence time series) and pa
 | `REST.idr` | REST endpoint definitions (18 endpoints, 6 groups) |
 | `FFI.idr` | GADT constructors for all C ABI functions + ffiReturnsApiResponse proof |
 | `RuleEngine.idr` | Rule-evaluation types |
+| `Verdict.idr` | Verdict records (HYP-01): support = Pattern / Observed n / Mechanical re-check; `Sound` only from a confirming re-check. Gate: `scripts/check-verdicts.sh` (+ `tests/reject/`, `tests/accept/`) |
 
 **Build system:** `src/abi/hypatia-abi.ipkg` (compile), `verify/hypatia-verify.ipkg` (proofs), `pack.toml` (Pack package manager).
 The ipkg sets `sourcedir = ".."`, so **`src/Hypatia/ABI/` is what compiles** — that is the
diff --git a/.github/workflows/verify-proofs.yml b/.github/workflows/verify-proofs.yml
index 1a29bfec..3e65c070 100644
--- a/.github/workflows/verify-proofs.yml
+++ b/.github/workflows/verify-proofs.yml
@@ -22,6 +22,12 @@ on:
     - src/abi/**
     - src/Hypatia/ABI/**
     - verify/**
+    - tests/accept/**
+    - tests/reject/**
+    - scripts/check-verdicts.sh
+    - scripts/recheck-lean-hole.sh
+    - scripts/fetch-siblings.sh
+    - scripts/check-sibling-citations.sh
     branches:
     - main
   pull_request:
@@ -40,6 +46,12 @@ on:
     - src/abi/**
     - src/Hypatia/ABI/**
     - verify/**
+    - tests/accept/**
+    - tests/reject/**
+    - scripts/check-verdicts.sh
+    - scripts/recheck-lean-hole.sh
+    - scripts/fetch-siblings.sh
+    - scripts/check-sibling-citations.sh
     branches:
     - main
   schedule:
@@ -168,6 +180,13 @@ jobs:
       - name: Build the verify package (PipelineState, Verify.Fuel)
         run: idris2 --build verify/hypatia-verify.ipkg
 
+      # HYP-01: Verdict.idr claims a `Sound` verdict is constructible only
+      # from a confirming prover re-check. The typechecker is the falsifier:
+      # tests/accept/ must be accepted, and every tests/reject/ module must be
+      # refused at `invalid` with the diagnostic its `-- EXPECT:` line names.
+      - name: Verdict accept/reject fixtures (HYP-01)
+        run: bash scripts/check-verdicts.sh
+
       - name: Summary
         if: always()
         run: |
@@ -228,6 +247,13 @@ jobs:
           lake --version
           lake build
 
+      # HYP-01 positive control: the SoundVerdict in
+      # tests/accept/LeanHoleRecheckSound.idr records digests of a Lean run.
+      # Re-run Lean on the fixture from the repository root (where the
+      # control's paths are relative to) and require both digests to match.
+      - name: Re-check the Lean proof-hole fixture against the HYP-01 control
+        run: bash scripts/recheck-lean-hole.sh
+
       - name: Summary
         if: always()
         run: |
@@ -331,3 +357,23 @@ jobs:
 
       - name: No un-annotated trusted-base markers
         run: bash scripts/check-trusted-base.sh
+
+  # Sibling proof repos are consumed by pinned commit, never re-declared. The
+  # Idris2 records that follow them are transcriptions (correspondence
+  # ASSUMED); this job keeps the citation itself honest: the pin fetches,
+  # the cited definitions exist at it, and the citing header names it.
+  sibling-citations:
+    name: sibling citations at pin
+    runs-on: ubuntu-latest
+    timeout-minutes: 5
+    permissions:
+      contents: read
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v7.0.1
+
+      - name: Fetch pinned siblings
+        run: bash scripts/fetch-siblings.sh
+
+      - name: Every citation resolves at its pin
+        run: bash scripts/check-sibling-citations.sh
diff --git a/Justfile b/Justfile
index ed36cf96..2c97e280 100644
--- a/Justfile
+++ b/Justfile
@@ -75,6 +75,19 @@ abi-gen:
 compile-verify:
     cd verify && idris2 --build hypatia-verify.ipkg
 
+# HYP-01 verdict gate: ABI builds, tests/accept accepted, tests/reject refused for the stated reason
+check-verdicts:
+    bash scripts/check-verdicts.sh
+
+# Re-run Lean on the proof-hole fixture; digests must match the HYP-01 positive control
+recheck-lean-hole:
+    bash scripts/recheck-lean-hole.sh
+
+# Fetch pinned sibling proof repos, then check every citation resolves at its pin
+check-siblings:
+    bash scripts/fetch-siblings.sh
+    bash scripts/check-sibling-citations.sh
+
 # Model-check TLA+ specifications (e.g. H8 Kin-gate atomicity)
 verify-tlaplus:
     #!/usr/bin/env bash
diff --git a/scripts/check-proof-status.sh b/scripts/check-proof-status.sh
index 2f511e63..c7098404 100755
--- a/scripts/check-proof-status.sh
+++ b/scripts/check-proof-status.sh
@@ -58,9 +58,12 @@ extract() {
   awk '
     function emit_row(b,   spans, n, i, span, file, first) {
       if (b ~ /line-through/ || b ~ /RETIRED/) return
+      # split() on the OPENING delimiter leaves exactly one span per piece, so
+      # every piece is visited. Until 2026-10-14 this loop stepped by 2 and
+      # silently checked every second identifier only (7 of 16 on main).
       n = split(b, spans, /`\+/)
       file = ""
-      for (i = 2; i <= n; i += 2) {
+      for (i = 2; i <= n; i++) {
         span = spans[i]
         sub(/\+`.*/, "", span)   # cut at the closing +`
         first = span
@@ -90,7 +93,7 @@ extract() {
       body = s
       sub(/^[^\n]*\n/, "", body)
       n = split(body, spans, /`\+/)
-      for (i = 2; i <= n; i += 2) {
+      for (i = 2; i <= n; i++) {
         span = spans[i]
         sub(/\+`.*/, "", span)   # cut at the closing +`
         first = span
diff --git a/scripts/check-sibling-citations.sh b/scripts/check-sibling-citations.sh
new file mode 100755
index 00000000..aabaf4f4
--- /dev/null
+++ b/scripts/check-sibling-citations.sh
@@ -0,0 +1,75 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# check-sibling-citations.sh — keep hypatia's citations of sibling proofs
+# honest.  Run scripts/fetch-siblings.sh first.
+#
+# A module that transcribes a sibling's definitions names the sibling, the
+# commit, the file and the definitions in its header.  This script checks,
+# for every row of the table below:
+#
+#   1. the citing module names the commit that scripts/fetch-siblings.sh
+#      fetched (prose and pin agree);
+#   2. the cited file exists in the sibling at that commit;
+#   3. the cited definition is declared in that file (a declaration, not
+#      merely a mention: `record N`, `data N`, or `N :` at the start of a
+#      line, after indentation);
+#   4. the citing module's header mentions the definition by name.
+#
+# What this does NOT check: that the transcription corresponds to the Agda
+# definition.  That correspondence stays ASSUMED until a checked one exists.
+#
+# Usage: scripts/check-sibling-citations.sh
+# Exit:  0 = every citation resolves at its pin; 1 = a citation is stale;
+#        2 = a sibling has not been fetched.
+
+set -uo pipefail
+cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.." || exit 2
+deps=_build/dependencies
+
+# citing module | sibling | file in sibling | definition
+citations=(
+  "src/Hypatia/ABI/Verdict.idr|epistemic-types|src/EpistemicTypes/Warrant.agda|Warrant"
+  "src/Hypatia/ABI/Verdict.idr|epistemic-types|src/EpistemicTypes/Warrant.agda|Epi"
+  "src/Hypatia/ABI/Verdict.idr|epistemic-types|src/EpistemicTypes/Warrant.agda|SoundWarrant"
+  "src/Hypatia/ABI/Verdict.idr|epistemic-types|src/EpistemicTypes/Warrant.agda|sound-epi"
+  "src/Hypatia/ABI/Verdict.idr|epistemic-types|src/EpistemicTypes/Applications/RapidNJSkip.agda|no-receipt-reflection"
+)
+
+failures=0
+checked=0
+for row in "${citations[@]}"; do
+  IFS='|' read -r citer sibling file def <<<"$row"
+  dir="$deps/$sibling"
+  if [[ ! -d "$dir/.git" ]]; then
+    echo "::error::$sibling not fetched; run scripts/fetch-siblings.sh"
+    exit 2
+  fi
+  pin="$(git -C "$dir" rev-parse HEAD)"
+  checked=$((checked + 1))
+  before=$failures
+
+  if ! grep -qF "hyperpolymath/$sibling @ $pin" "$citer"; then
+    echo "::error::$citer does not name hyperpolymath/$sibling @ $pin (the fetched pin)"
+    failures=$((failures + 1))
+  fi
+  if [[ ! -f "$dir/$file" ]]; then
+    echo "::error::$sibling @ ${pin:0:7} has no $file (cited by $citer)"
+    failures=$((failures + 1))
+    continue
+  fi
+  re="^[[:space:]]*((record|data)[[:space:]]+)?${def}([[:space:]]|$)"
+  if ! grep -Eq "$re" "$dir/$file"; then
+    echo "::error::$sibling @ ${pin:0:7}: $file declares no '$def' (cited by $citer)"
+    failures=$((failures + 1))
+  fi
+  if ! grep -qw -- "$def" "$citer"; then
+    echo "::error::$citer cites $sibling but never names '$def'"
+    failures=$((failures + 1))
+  fi
+  [[ "$failures" -eq "$before" ]] && echo "ok  $citer -> $sibling @ ${pin:0:7} $file :: $def"
+done
+
+echo "sibling citations: checked ${checked}, stale ${failures}"
+[[ "$failures" -eq 0 ]] || exit 1
diff --git a/scripts/check-verdicts.sh b/scripts/check-verdicts.sh
new file mode 100755
index 00000000..4c925f26
--- /dev/null
+++ b/scripts/check-verdicts.sh
@@ -0,0 +1,107 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# check-verdicts.sh — the mechanical falsifier for HYP-01's verdict record.
+#
+# src/Hypatia/ABI/Verdict.idr claims that a `Sound` verdict can be built only
+# from a `Mechanical` support whose prover re-check `Confirms`.  A claim about
+# what does NOT typecheck is tested by asking the typechecker:
+#
+#   1. the ABI package builds (the positive set, first: a broken toolchain or
+#      a missing import must never turn into a "successful" rejection);
+#   2. src/Hypatia/ABI/Verdict.idr contains no escape-hatch marker at all;
+#   3. every module under tests/accept/ is ACCEPTED (positive controls);
+#   4. every module under tests/reject/ is REFUSED, and refused only at its
+#      declaration `invalid`, with the diagnostic its `-- EXPECT:` line
+#      names — an error anywhere else, a different diagnostic (an arity
+#      slip is also "refused at invalid"), or a refusal for a missing name,
+#      import or parse, is a broken fixture, not a pass.
+#
+# An empty tests/accept/ or tests/reject/ is a broken checkout, not a pass.
+# The Lean half of the positive control (re-running the prover and comparing
+# digests) is scripts/recheck-lean-hole.sh.
+#
+# Usage: scripts/check-verdicts.sh
+# Env:   IDRIS2 (default: idris2)
+# Exit:  0 = all controls behave; 1 = a control misbehaved.
+
+set -euo pipefail
+cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.."
+
+idris2="${IDRIS2:-idris2}"
+logs=_build/check-verdicts
+mkdir -p "$logs"
+
+"$idris2" --version
+
+# 1. Positive set: the ABI package, Verdict included.
+"$idris2" --build src/abi/hypatia-abi.ipkg
+export IDRIS2_PATH="$PWD/build/abi/ttc${IDRIS2_PATH:+:$IDRIS2_PATH}"
+
+# 2. No escape hatch in the module the rejections are about.
+if grep -nE 'believe_me|assert_total|assert_smaller|idris_crash|postulate|sorry|admit|native_decide|Admitted|unsafeCoerce|Obj\.magic' \
+     src/Hypatia/ABI/Verdict.idr; then
+  echo "ERROR: escape-hatch marker in src/Hypatia/ABI/Verdict.idr" >&2
+  exit 1
+fi
+echo "PASS: no escape-hatch marker in src/Hypatia/ABI/Verdict.idr"
+
+shopt -s nullglob
+accepts=(tests/accept/*.idr)
+rejects=(tests/reject/*.idr)
+shopt -u nullglob
+if (( ${#accepts[@]} == 0 )); then
+  echo 'ERROR: no positive controls found under tests/accept' >&2
+  exit 1
+fi
+if (( ${#rejects[@]} == 0 )); then
+  echo 'ERROR: no expected-rejection modules found under tests/reject' >&2
+  exit 1
+fi
+
+# 3. Positive controls must typecheck.
+for file in "${accepts[@]}"; do
+  name="$(basename -- "$file" .idr)"
+  log="$logs/accept-$name.log"
+  if ! "$idris2" --source-dir tests/accept --build-dir "$logs/build" --check "$file" >"$log" 2>&1; then
+    cat "$log"
+    echo "ERROR: positive control refused: $name" >&2
+    exit 1
+  fi
+  if grep -q '^Error' "$log"; then
+    cat "$log"
+    echo "ERROR: positive control reported an error: $name" >&2
+    exit 1
+  fi
+  echo "PASS: accepted positive control $name"
+done
+
+# 4. Expected rejections must be refused, at `invalid`, for a typing reason.
+for file in "${rejects[@]}"; do
+  name="$(basename -- "$file" .idr)"
+  log="$logs/reject-$name.log"
+  if "$idris2" --source-dir tests/reject --build-dir "$logs/build" --check "$file" >"$log" 2>&1; then
+    cat "$log"
+    echo "ERROR: invalid verdict accepted: $name" >&2
+    exit 1
+  fi
+  expect="$(sed -n 's/^-- EXPECT: //p' "$file" | head -1)"
+  if [[ -z "$expect" ]]; then
+    echo "ERROR: $file declares no '-- EXPECT: <diagnostic>' line" >&2
+    exit 1
+  fi
+  errors="$(grep -c '^Error' "$log" || true)"
+  if [[ "$errors" -ne 1 ]] ||
+     ! grep -qF -- "$expect" "$log" ||
+     ! grep -q '^Error: While processing right hand side of invalid\.' "$log" ||
+     ! grep -Eq "^${name}:[0-9]+:[0-9]+--[0-9]+:[0-9]+" "$log" ||
+     grep -Eq 'Undefined name|Possible cause|Can.t find import|not in the source directory|Couldn.t parse|Parse error|is not a valid' "$log"; then
+    cat "$log"
+    echo "ERROR: unexpected failure while checking $name (want exactly one typing error, at invalid: $expect)" >&2
+    exit 1
+  fi
+  echo "PASS: rejected $name at invalid: $expect"
+done
+
+echo "PASS: ABI package, ${#accepts[@]} positive control(s), ${#rejects[@]} expected rejection(s)"
diff --git a/scripts/fetch-siblings.sh b/scripts/fetch-siblings.sh
new file mode 100755
index 00000000..7130b330
--- /dev/null
+++ b/scripts/fetch-siblings.sh
@@ -0,0 +1,35 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# Fetch the sibling proof repositories hypatia cites into _build/dependencies,
+# each at a recorded commit, with plain git (the residual-evidence-types
+# pattern).  A checkout that does not resolve to the pinned commit is a
+# failure, never a fallback to whatever the remote currently serves.
+#
+# Hypatia does not import these sources: Idris2 cannot consume Agda, so the
+# ABI records that follow them are transcriptions (ASSUMED correspondence).
+# The pins make the citation checkable — scripts/check-sibling-citations.sh
+# fails if a cited name is absent at the pin, or if a module header names a
+# different commit from the one fetched here.  Re-pin deliberately, one
+# commit per pin.
+set -euo pipefail
+cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.."
+deps=_build/dependencies
+
+fetch() {
+  local name=$1 repo=$2 sha=$3 dir
+  dir=$deps/$name
+  if [[ ! -d "$dir/.git" ]]; then
+    git init -q "$dir"
+    git -C "$dir" remote add origin "https://github.com/$repo.git"
+  fi
+  git -C "$dir" fetch -q --depth 1 origin "$sha"
+  git -C "$dir" checkout -q --detach FETCH_HEAD
+  test "$(git -C "$dir" rev-parse HEAD)" = "$sha"
+  echo "$name @ $sha"
+}
+
+mkdir -p "$deps"
+# HYP-01 verdict record (src/Hypatia/ABI/Verdict.idr): Warrant / Epi / SoundWarrant.
+fetch epistemic-types hyperpolymath/epistemic-types 6a68de3141a981d766fd006b312f0919ade334bf
diff --git a/scripts/recheck-lean-hole.sh b/scripts/recheck-lean-hole.sh
new file mode 100755
index 00000000..42810ba9
--- /dev/null
+++ b/scripts/recheck-lean-hole.sh
@@ -0,0 +1,118 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# recheck-lean-hole.sh — tie HYP-01's positive control to a prover run.
+#
+# tests/accept/LeanHoleRecheckSound.idr builds a `SoundVerdict` for the
+# code_safety Lean proof-hole detector from a Lean 4 re-check of the
+# detector's soundness fixture.  Idris2 only checks that record's shape; the
+# digests in it are claims about a run.  This script makes them falsifiable:
+#
+#   1. read fixturePath, proverVersion, targetHash, artefactHash and the span
+#      line from the control (the control is the single source; nothing is
+#      restated here);
+#   2. the fixture's SHA-256 must equal targetHash;
+#   3. `lean --version` must report proverVersion;
+#   4. run `lean <fixturePath>` from the repository root; the combined output
+#      must carry Lean's own "declaration uses" diagnostic at the span line,
+#      and its SHA-256 must equal artefactHash.
+#
+# Negative controls, run every time, so a pass is never vacuous:
+#   N1. Lean on a hole-free module prints no such diagnostic (the diagnostic
+#       is evidence, not boilerplate);
+#   N2. the same fixture under another path yields a different artefact
+#       digest (the digest is sensitive to the run it records).
+#
+# Usage: scripts/recheck-lean-hole.sh
+# Env:   LEAN (default: lean)
+# Exit:  0 = control agrees with a fresh run; 1 = disagreement; 2 = usage/IO.
+
+set -euo pipefail
+cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.."
+
+lean="${LEAN:-lean}"
+control=tests/accept/LeanHoleRecheckSound.idr
+work=_build/recheck-lean-hole
+mkdir -p "$work"
+
+[[ -f "$control" ]] || { echo "ERROR: $control not found" >&2; exit 2; }
+
+field() {
+  # $1 = extended regex with one capture group, applied to the control.
+  sed -nE "s/$1/\\1/p" "$control" | head -1
+}
+
+target="$(field '^fixturePath = "([^"]+)".*')"
+version="$(field '^  "([0-9]+\.[0-9]+\.[0-9]+)"$')"
+target_hash="$(field '^  \(MkSha256 "([0-9a-f]{64})"\) -- targetHash$')"
+artefact_hash="$(field '^  \(MkSha256 "([0-9a-f]{64})"\) -- artefactHash$')"
+span_line="$(field '^ +\(MkSpan fixturePath ([0-9]+) [0-9]+\) [0-9]+$')"
+
+for v in target version target_hash artefact_hash span_line; do
+  if [[ -z "${!v}" ]]; then
+    echo "ERROR: could not read $v from $control" >&2
+    exit 2
+  fi
+done
+echo "control: target=$target lean=$version span=$span_line"
+
+sha() { sha256sum "$1" | cut -d' ' -f1; }
+
+# 2. The bytes Lean reads are the bytes the control names.
+actual="$(sha "$target")"
+if [[ "$actual" != "$target_hash" ]]; then
+  echo "ERROR: $target digest $actual != targetHash $target_hash" >&2
+  echo "       The fixture changed. If that was deliberate, re-run Lean on it and" >&2
+  echo "       re-measure both digests in $control (see its header)." >&2
+  exit 1
+fi
+echo "PASS: targetHash matches $target"
+
+# 3. The prover is the one the control names.
+lean_version="$("$lean" --version)"
+echo "$lean_version"
+if [[ "$lean_version" != *"version $version,"* ]]; then
+  echo "ERROR: control names Lean $version, toolchain is: $lean_version" >&2
+  exit 1
+fi
+
+# 4. A fresh re-check reproduces the artefact.
+artefact="$work/artefact.log"
+"$lean" "$target" >"$artefact" 2>&1 || true
+cat "$artefact"
+if ! grep -Eq "^${target}:${span_line}:[0-9]+: warning: declaration uses \`sorry\`$" "$artefact"; then
+  echo "ERROR: Lean did not report the proof hole at ${target}:${span_line}" >&2
+  exit 1
+fi
+actual="$(sha "$artefact")"
+if [[ "$actual" != "$artefact_hash" ]]; then
+  echo "ERROR: artefact digest $actual != artefactHash $artefact_hash" >&2
+  exit 1
+fi
+echo "PASS: Lean re-check confirms the hole at ${target}:${span_line}; artefactHash matches"
+
+# N1. No hole, no diagnostic.
+printf '%s\n' 'theorem ok : 1 + 1 = 2 := rfl' >"$work/NoHole.lean"
+if ! "$lean" "$work/NoHole.lean" >"$work/nohole.log" 2>&1; then
+  cat "$work/nohole.log"
+  echo "ERROR: negative control N1 did not typecheck" >&2
+  exit 1
+fi
+if grep -q 'declaration uses' "$work/nohole.log"; then
+  cat "$work/nohole.log"
+  echo "ERROR: negative control N1: diagnostic printed for a hole-free module" >&2
+  exit 1
+fi
+echo "PASS: N1 hole-free module prints no proof-hole diagnostic"
+
+# N2. Another run, another digest.
+cp "$target" "$work/Moved.lean"
+"$lean" "$work/Moved.lean" >"$work/moved.log" 2>&1 || true
+if [[ "$(sha "$work/moved.log")" == "$artefact_hash" ]]; then
+  echo "ERROR: negative control N2: a different run produced the recorded digest" >&2
+  exit 1
+fi
+echo "PASS: N2 a different run yields a different artefact digest"
+
+echo "PASS: positive control agrees with a fresh Lean $version re-check"
diff --git a/src/Hypatia/ABI/Verdict.idr b/src/Hypatia/ABI/Verdict.idr
new file mode 100644
index 00000000..a82bdf4f
--- /dev/null
+++ b/src/Hypatia/ABI/Verdict.idr
@@ -0,0 +1,318 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- Hypatia ABI — Verdict records (HYP-01)
+--
+-- Every gate verdict names its support.  A verdict is an Epi: a claim, the
+-- evidence tokens it was issued on (rule id and version, matched span, fleet
+-- observation count), and the support those tokens give.  It is sound only
+-- when the support carries a soundness map from evidence to the claim, and
+-- the only such map hypatia has today is a mechanical falsifier: a prover
+-- re-checking the file a proof-bypass detector flagged.  A pattern match is
+-- evidence that the pattern matched; an observation count is belief
+-- formation (rules.a2ml proposes a rule at 5 observations); neither is a
+-- proof that the property holds.
+--
+-- What is proved here (Idris2, %default total, no proof-bypass primitives):
+--   * `Sound` has exactly one constructor, indexed by `Mechanical`, and it
+--     demands a re-check whose result `Confirms` the claim
+--     (`patternNotSound`, `observedNotSound`, `refutedNotSound`);
+--   * `decSound` decides soundness of any support;
+--   * the derived `level` says "sound" only when a `Sound` witness exists
+--     (`soundLevelHasWitness`, `patternNeverSoundLevel`,
+--     `observedNeverSoundLevel`), and a `SoundVerdict` always derives "sound"
+--     (`soundVerdictLevel`);
+--   * a `Sha256` literal that is not 64 lower-case hex digits does not
+--     typecheck, so a `Sound` witness always names a well-formed digest of
+--     its re-check artefact (`soundArtefact`).
+--
+-- What is NOT proved here:
+--   * that a `Confirms` result is what the prover actually printed: that is
+--     the job of scripts/recheck-lean-hole.sh, which re-runs the prover and
+--     compares digests with the positive control in tests/accept/;
+--   * that this record corresponds to the Agda definitions it transcribes.
+--
+-- Transcription source (read for the shape only, never imported):
+--   hyperpolymath/epistemic-types @ 6a68de3141a981d766fd006b312f0919ade334bf
+--   src/EpistemicTypes/Warrant.agda — Warrant, Epi, SoundWarrant, sound-epi
+--   src/EpistemicTypes/Applications/RapidNJSkip.agda — no-receipt-reflection
+-- Correspondence (Warrant ~ the rule at a version; Epi ~ `Verdict`;
+-- SoundWarrant ~ `SoundVerdict`; sound-epi ~ `Rechecked`) is ASSUMED, not
+-- checked.  scripts/fetch-siblings.sh fetches the pin and
+-- scripts/check-sibling-citations.sh fails if a name cited above is absent
+-- there; neither checks the correspondence itself.
+
+module Hypatia.ABI.Verdict
+
+import public Data.So
+
+%default total
+
+------------------------------------------------------------------------
+-- Section 1: Digests
+------------------------------------------------------------------------
+
+||| A lower-case hexadecimal digit.
+public export
+isLowerHexDigit : Char -> Bool
+isLowerHexDigit c = isDigit c || (c >= 'a' && c <= 'f')
+
+||| Exactly 64 lower-case hex digits: the shape of a SHA-256 digest.
+public export
+isSha256Hex : String -> Bool
+isSha256Hex s = length s == 64 && all isLowerHexDigit (unpack s)
+
+||| A SHA-256 digest.  The well-formedness proof is found by evaluation, so a
+||| literal of the wrong shape is refused at compile time.
+public export
+record Sha256 where
+  constructor MkSha256
+  hex : String
+  {auto 0 wellFormed : So (isSha256Hex hex)}
+
+------------------------------------------------------------------------
+-- Section 2: Evidence tokens
+------------------------------------------------------------------------
+
+||| A matched region of a file, 1-based and inclusive.
+public export
+record Span where
+  constructor MkSpan
+  file      : String
+  startLine : Nat
+  endLine   : Nat
+
+||| One piece of evidence a rule offered for a verdict: which rule, at which
+||| version, matched where, and how many times the fleet has observed it.
+||| A token is evidence that the rule fired.  It is not the claim.
+public export
+record EvidenceToken where
+  constructor MkEvidenceToken
+  ruleModule   : String
+  ruleId       : String
+  ruleVersion  : String
+  span         : Span
+  observations : Nat
+
+------------------------------------------------------------------------
+-- Section 3: Prover re-checks
+------------------------------------------------------------------------
+
+||| The provers whose bypass detectors hypatia ships
+||| (lib/rules/code_safety.ex; fixtures in test/soundness/fixtures/code_safety/).
+public export
+data Prover = Lean4 | Idris2 | Agda | Coq
+
+||| What a prover reported when it re-checked a flagged file.
+|||   Confirms — the prover's own diagnostic states the bypass the detector
+|||              claimed (Lean 4: "declaration uses `...`" at the flagged line).
+|||   Refutes  — the prover re-checked the file and reported no bypass: the
+|||              detector's match was not a proof hole.
+public export
+data RecheckResult = Confirms | Refutes
+
+public export
+Uninhabited (Refutes = Confirms) where
+  uninhabited Refl impossible
+
+public export
+Uninhabited (Confirms = Refutes) where
+  uninhabited Refl impossible
+
+||| Decide whether a result confirms.
+public export
+decConfirms : (r : RecheckResult) -> Dec (r = Confirms)
+decConfirms Confirms = Yes Refl
+decConfirms Refutes  = No absurd
+
+||| A prover re-check of one file.  `targetHash` is the digest of the bytes
+||| the prover read; `artefactHash` is the digest of everything the prover
+||| printed.  Both are what scripts/recheck-lean-hole.sh recomputes.
+public export
+record ProverRecheck where
+  constructor MkProverRecheck
+  prover        : Prover
+  proverVersion : String
+  target        : String
+  targetHash    : Sha256
+  artefactHash  : Sha256
+  result        : RecheckResult
+
+------------------------------------------------------------------------
+-- Section 4: Support
+------------------------------------------------------------------------
+
+||| What a verdict's evidence supports.
+public export
+data Support : Type where
+  ||| A pattern matched.  Evidence that the pattern matched, and nothing more.
+  Pattern    : Support
+  ||| The finding has been observed `n` times across the fleet.  A count is
+  ||| belief formation; rules.a2ml's proposal threshold of 5 is a policy, not
+  ||| a soundness proof.
+  Observed   : (n : Nat) -> Support
+  ||| A prover re-checked the flagged file.
+  Mechanical : (recheck : ProverRecheck) -> Support
+
+||| `Sound s`: the support `s` carries a soundness map from its evidence to
+||| the claim.  The only constructor is indexed by `Mechanical` and demands a
+||| re-check that `Confirms`.  This is SoundWarrant's `sound` field read at
+||| the ABI layer: the prover's own report is the map.
+public export
+data Sound : Support -> Type where
+  Rechecked : (recheck : ProverRecheck)
+           -> (confirmed : result recheck = Confirms)
+           -> Sound (Mechanical recheck)
+
+||| The digest of the re-check artefact a `Sound` witness rests on.
+public export
+soundArtefact : Sound s -> Sha256
+soundArtefact (Rechecked recheck _) = artefactHash recheck
+
+||| A `Sound` witness names exactly its re-check's artefact.
+public export
+soundArtefactIsRecheck : (w : Sound (Mechanical recheck))
+                      -> soundArtefact w = artefactHash recheck
+soundArtefactIsRecheck (Rechecked recheck _) = Refl
+
+||| A pattern match is never sound.
+public export
+patternNotSound : Sound Pattern -> Void
+patternNotSound (Rechecked _ _) impossible
+
+||| No observation count is sound, however large.
+public export
+observedNotSound : Sound (Observed n) -> Void
+observedNotSound (Rechecked _ _) impossible
+
+||| A re-check that refutes the detector is not soundness either.
+public export
+refutedNotSound : (recheck : ProverRecheck)
+               -> result recheck = Refutes
+               -> Sound (Mechanical recheck) -> Void
+refutedNotSound recheck refuted (Rechecked recheck confirmed) =
+  absurd (trans (sym refuted) confirmed)
+
+||| Soundness of a support is decidable.
+public export
+decSound : (s : Support) -> Dec (Sound s)
+decSound Pattern = No patternNotSound
+decSound (Observed n) = No observedNotSound
+decSound (Mechanical recheck) with (decConfirms (result recheck))
+  decSound (Mechanical recheck) | Yes confirmed = Yes (Rechecked recheck confirmed)
+  decSound (Mechanical recheck) | No notConfirmed =
+    No (\(Rechecked recheck confirmed) => notConfirmed confirmed)
+
+------------------------------------------------------------------------
+-- Section 5: Verdicts and their level
+------------------------------------------------------------------------
+
+||| A gate verdict: the claim, the evidence tokens it was issued on, and the
+||| support they give.  Pass/fail is derived from this record, never stored
+||| beside it.  This is Epi read at the ABI layer: holding a `Verdict` does
+||| not by itself give its claim.
+public export
+record Verdict where
+  constructor MkVerdict
+  claim    : String
+  evidence : List EvidenceToken
+  support  : Support
+
+||| A verdict with a soundness witness for its support: SoundWarrant read at
+||| the ABI layer.
+public export
+record SoundVerdict where
+  constructor MkSoundVerdict
+  verdict : Verdict
+  sound   : Sound (support verdict)
+
+||| The epistemic level a verdict is reported at.  These are the only three
+||| values the findings schema accepts for `level`.
+|||   LvSound  — the support carries a soundness witness;
+|||   LvEpi    — evidence tokens, no soundness witness;
+|||   LvBelief — no evidence token at all (a Bayesian posterior alone).
+public export
+data Level = LvSound | LvEpi | LvBelief
+
+public export
+Uninhabited (LvEpi = LvSound) where
+  uninhabited Refl impossible
+
+public export
+Uninhabited (LvBelief = LvSound) where
+  uninhabited Refl impossible
+
+||| Wire spelling of a level (schema/findings.ncl `Level`).
+public export
+levelName : Level -> String
+levelName LvSound  = "sound"
+levelName LvEpi    = "epi"
+levelName LvBelief = "belief"
+
+||| The level without a soundness witness: tokens make it epi, none make it
+||| belief.
+public export
+unsoundLevel : List EvidenceToken -> Level
+unsoundLevel []       = LvBelief
+unsoundLevel (_ :: _) = LvEpi
+
+||| An unsound level is never "sound".
+public export
+unsoundLevelNotSound : (ts : List EvidenceToken) -> unsoundLevel ts = LvSound -> Void
+unsoundLevelNotSound []       prf = absurd prf
+unsoundLevelNotSound (_ :: _) prf = absurd prf
+
+||| Level from a soundness decision.
+public export
+levelFrom : Dec (Sound s) -> List EvidenceToken -> Level
+levelFrom (Yes _) _  = LvSound
+levelFrom (No _)  ts = unsoundLevel ts
+
+||| The level a verdict is reported at, derived from its support.
+public export
+level : Verdict -> Level
+level v = levelFrom (decSound (support v)) (evidence v)
+
+||| "sound" from `levelFrom` means the decision found a witness.
+public export
+levelFromSoundHasWitness : (d : Dec (Sound s)) -> (ts : List EvidenceToken)
+                        -> levelFrom d ts = LvSound -> Sound s
+levelFromSoundHasWitness (Yes w) _  _   = w
+levelFromSoundHasWitness (No _)  ts prf = absurd (unsoundLevelNotSound ts prf)
+
+||| A verdict reported at level "sound" has a soundness witness.
+public export
+soundLevelHasWitness : (v : Verdict) -> level v = LvSound -> Sound (support v)
+soundLevelHasWitness v = levelFromSoundHasWitness (decSound (support v)) (evidence v)
+
+||| A pattern-supported verdict is never reported "sound".
+public export
+patternNeverSoundLevel : (v : Verdict) -> support v = Pattern
+                      -> level v = LvSound -> Void
+patternNeverSoundLevel v supp prf =
+  patternNotSound (replace {p = Sound} supp (soundLevelHasWitness v prf))
+
+||| An observation-supported verdict is never reported "sound".
+public export
+observedNeverSoundLevel : (v : Verdict) -> support v = Observed n
+                       -> level v = LvSound -> Void
+observedNeverSoundLevel v supp prf =
+  observedNotSound (replace {p = Sound} supp (soundLevelHasWitness v prf))
+
+||| A decision that has a witness in hand reports "sound".
+public export
+levelFromWitness : (w : Sound s) -> (d : Dec (Sound s)) -> (ts : List EvidenceToken)
+                -> levelFrom d ts = LvSound
+levelFromWitness _ (Yes _)      _ = Refl
+levelFromWitness w (No contra)  _ = absurd (contra w)
+
+||| A `SoundVerdict` is always reported "sound".
+public export
+soundVerdictLevel : (sv : SoundVerdict) -> level (verdict sv) = LvSound
+soundVerdictLevel sv =
+  levelFromWitness (sound sv) (decSound (support (verdict sv))) (evidence (verdict sv))
+
+||| Forget the witness: every sound verdict is a verdict.
+public export
+forgetSound : SoundVerdict -> Verdict
+forgetSound = verdict
diff --git a/src/abi/README.adoc b/src/abi/README.adoc
index 407bacd9..49e4c87e 100644
--- a/src/abi/README.adoc
+++ b/src/abi/README.adoc
@@ -34,6 +34,7 @@ been undetectable, so the dead copy was deleted (issue #815, DEBT-REGISTER C-4).
 |`src/Hypatia/ABI/REST.idr` |REST endpoint definitions (18 endpoints, 6 groups)
 |`src/Hypatia/ABI/FFI.idr` |GADT constructors for all 7 C ABI functions + `ffiReturnsApiResponse` proof
 |`src/Hypatia/ABI/RuleEngine.idr` |Rule engine type definitions and proof obligations
+|`src/Hypatia/ABI/Verdict.idr` |Verdict records (HYP-01): every verdict names its support; `Sound` only from a confirming prover re-check. Gate: `just check-verdicts`
 |`src/Hypatia/ABI/Gen.idr` |The generator: evaluates the ABI and emits the generated mirrors
 |===
 
diff --git a/src/abi/hypatia-abi.ipkg b/src/abi/hypatia-abi.ipkg
index c1eb82d4..2ef9b51c 100644
--- a/src/abi/hypatia-abi.ipkg
+++ b/src/abi/hypatia-abi.ipkg
@@ -22,6 +22,7 @@ modules = Hypatia.ABI.Types
         , Hypatia.ABI.REST
         , Hypatia.ABI.FFI
         , Hypatia.ABI.RuleEngine
+        , Hypatia.ABI.Verdict
 
 builddir = "../../build/abi"
 
diff --git a/test/soundness/README.adoc b/test/soundness/README.adoc
index fa5e37f1..6b5dccfa 100644
--- a/test/soundness/README.adoc
+++ b/test/soundness/README.adoc
@@ -61,6 +61,16 @@ another rule. The commit message MUST justify the removal — the default
 assumption is the entry stays. A bare manifest entry deletion in a PR
 that doesn't also remove the rule should fail review.
 
+== The Lean proof-hole fixture is digest-pinned
+
+`fixtures/code_safety/sorry.lean` is also the target of HYP-01's positive
+control, `tests/accept/LeanHoleRecheckSound.idr`: a sound verdict built
+from a Lean 4 re-check of this file. The control records the file's SHA-256
+and the SHA-256 of Lean's output, and `scripts/recheck-lean-hole.sh`
+(CI: the `lake build` job in `verify-proofs.yml`) re-runs Lean and compares
+them. Any edit to the fixture, a comment included, turns that check red
+until the two digests in the control are re-measured from a fresh run.
+
 == Running
 
   mix test --only soundness            # just the soundness suite
diff --git a/tests/accept/LeanHoleRecheckSound.idr b/tests/accept/LeanHoleRecheckSound.idr
new file mode 100644
index 00000000..15c9edc6
--- /dev/null
+++ b/tests/accept/LeanHoleRecheckSound.idr
@@ -0,0 +1,86 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- POSITIVE CONTROL (HYP-01).  A `SoundVerdict` for the code_safety Lean
+-- proof-hole detector, built from a Lean 4 re-check of that detector's
+-- soundness fixture.  scripts/check-verdicts.sh requires Idris2 to ACCEPT
+-- this module; the expected rejections in tests/reject/ are the other half.
+--
+-- The digests below are not trusted by being written here.
+-- scripts/recheck-lean-hole.sh reads `fixturePath`, `proverVersion`,
+-- `targetHash`, `artefactHash` and the span line out of this file, re-runs
+-- Lean on the fixture, recomputes both digests, requires Lean's own
+-- "declaration uses" diagnostic at the span line, and fails if any of them
+-- disagrees with this file.  This module proves only that the record is
+-- well-typed and is reported at level "sound"; the script ties it to a run.
+--
+-- Measured 2026-10-14 with Lean (version 4.30.0, x86_64-unknown-linux-gnu,
+-- commit d024af099ca4bf2c86f649261ebf59565dc8c622, Release), run from the
+-- repository root as `lean <fixturePath>`; the artefact is Lean's combined
+-- stdout and stderr, exactly as printed.
+
+module LeanHoleRecheckSound
+
+import Hypatia.ABI.Verdict
+
+%default total
+%unbound_implicits off
+
+-- The fixture the detector must flag and Lean must re-check.
+fixturePath : String
+fixturePath = "test/soundness/fixtures/code_safety/sorry.lean" -- hypatia: allow code_safety/sorry -- fixture path as data, not a proof hole
+
+-- The detector's rule id (lib/rules/code_safety.ex, @lean_banned).
+detectorRuleId : String
+detectorRuleId = "sorry" -- hypatia: allow code_safety/sorry -- rule id as data, not a proof hole
+
+||| The Lean 4 re-check of the fixture.
+public export
+recheck : ProverRecheck
+recheck = MkProverRecheck
+  Lean4
+  "4.30.0"
+  fixturePath
+  (MkSha256 "5465a2710136d470469e3bc4351c27dd0a6d8a14f520fd7009f5f196351c72e7") -- targetHash
+  (MkSha256 "f5d4cf9e8b96dd98cbf47d432fb83411dad3aa92dd37de1f21d30bebf1f03a31") -- artefactHash
+  Confirms
+
+||| The detector's evidence: rule, version, the flagged line, one observation
+||| (this fixture).  `ruleVersion` is the hypatia version in mix.exs.
+public export
+holeToken : EvidenceToken
+holeToken = MkEvidenceToken "code_safety" detectorRuleId "0.1.0"
+          (MkSpan fixturePath 8 8) 1
+
+||| The claim the verdict makes.
+public export
+holeClaim : String
+holeClaim = fixturePath ++ ":8: theorem `bad` rests on a Lean proof hole"
+
+||| The control: the detector's token, supported by the Lean re-check.
+public export
+soundControl : SoundVerdict
+soundControl = MkSoundVerdict (MkVerdict holeClaim [holeToken] (Mechanical recheck))
+                         (Rechecked recheck Refl)
+
+||| The control is reported at level "sound", by evaluation.
+public export
+controlIsSound : levelName (level (verdict soundControl)) = "sound"
+controlIsSound = Refl
+
+||| The control's soundness witness names the measured artefact.
+public export
+controlArtefact : hex (soundArtefact (sound soundControl))
+                = "f5d4cf9e8b96dd98cbf47d432fb83411dad3aa92dd37de1f21d30bebf1f03a31"
+controlArtefact = Refl
+
+||| The same token held without the re-check is epi, not sound: the match
+||| alone is evidence that the pattern matched.
+public export
+patternOnlyIsEpi : levelName (level (MkVerdict holeClaim [holeToken] Pattern)) = "epi"
+patternOnlyIsEpi = Refl
+
+||| The same claim with no evidence token is belief.
+public export
+noTokenIsBelief : levelName (level (MkVerdict holeClaim [] (Observed 5))) = "belief"
+noTokenIsBelief = Refl
diff --git a/tests/reject/MalformedDigest.idr b/tests/reject/MalformedDigest.idr
new file mode 100644
index 00000000..976e26ac
--- /dev/null
+++ b/tests/reject/MalformedDigest.idr
@@ -0,0 +1,37 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- EXPECTED REJECTION (HYP-01).  scripts/check-verdicts.sh passes only if
+-- Idris2 refuses this module, and only at the declaration `invalid`.  Every
+-- other declaration must typecheck, so that the refusal is for the stated
+-- reason and not for a missing import or a typo.
+--
+-- Must fail: a `Sound` witness must name a well-formed SHA-256 digest of
+-- its artefact.  `MkSha256` finds its well-formedness proof by evaluation, so a
+-- digest that is not 64 lower-case hex digits does not typecheck.
+--
+-- EXPECT: Can't find an implementation for So False.
+
+module MalformedDigest
+
+import Hypatia.ABI.Verdict
+
+%default total
+
+-- Placeholder digests: well-formed, and deliberately not the digest of
+-- anything.  They are scaffolding, not evidence.
+zero : Sha256
+zero = MkSha256 "0000000000000000000000000000000000000000000000000000000000000000"
+
+recheck : ProverRecheck
+recheck = MkProverRecheck Lean4 "4.30.0" "Example.lean" zero zero Confirms
+
+refuted : ProverRecheck
+refuted = MkProverRecheck Lean4 "4.30.0" "Example.lean" zero zero Refutes
+
+token : EvidenceToken
+token = MkEvidenceToken "code_safety" "example_rule" "0.1.0"
+          (MkSpan "Example.lean" 1 1) 1
+
+invalid : Sha256
+invalid = MkSha256 "F5D4CF9E"
diff --git a/tests/reject/ObservedIsNotSound.idr b/tests/reject/ObservedIsNotSound.idr
new file mode 100644
index 00000000..eccd6006
--- /dev/null
+++ b/tests/reject/ObservedIsNotSound.idr
@@ -0,0 +1,37 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- EXPECTED REJECTION (HYP-01).  scripts/check-verdicts.sh passes only if
+-- Idris2 refuses this module, and only at the declaration `invalid`.  Every
+-- other declaration must typecheck, so that the refusal is for the stated
+-- reason and not for a missing import or a typo.
+--
+-- Must fail: an observation count is belief formation.  rules.a2ml
+-- proposes a rule at 5 observations; that threshold is a policy, and no count,
+-- however large, makes `Observed n` sound.
+--
+-- EXPECT: Mismatch between: Mechanical recheck and Observed 5.
+
+module ObservedIsNotSound
+
+import Hypatia.ABI.Verdict
+
+%default total
+
+-- Placeholder digests: well-formed, and deliberately not the digest of
+-- anything.  They are scaffolding, not evidence.
+zero : Sha256
+zero = MkSha256 "0000000000000000000000000000000000000000000000000000000000000000"
+
+recheck : ProverRecheck
+recheck = MkProverRecheck Lean4 "4.30.0" "Example.lean" zero zero Confirms
+
+refuted : ProverRecheck
+refuted = MkProverRecheck Lean4 "4.30.0" "Example.lean" zero zero Refutes
+
+token : EvidenceToken
+token = MkEvidenceToken "code_safety" "example_rule" "0.1.0"
+          (MkSpan "Example.lean" 1 1) 1
+
+invalid : SoundVerdict
+invalid = MkSoundVerdict (MkVerdict "claim" [token] (Observed 5)) (Rechecked recheck Refl)
diff --git a/tests/reject/PatternIsNotSound.idr b/tests/reject/PatternIsNotSound.idr
new file mode 100644
index 00000000..b90d2a2f
--- /dev/null
+++ b/tests/reject/PatternIsNotSound.idr
@@ -0,0 +1,37 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- EXPECTED REJECTION (HYP-01).  scripts/check-verdicts.sh passes only if
+-- Idris2 refuses this module, and only at the declaration `invalid`.  Every
+-- other declaration must typecheck, so that the refusal is for the stated
+-- reason and not for a missing import or a typo.
+--
+-- Must fail: a pattern match is evidence that the pattern matched, not a
+-- soundness map: `Sound` is indexed only by `Mechanical`, so a `Sound` witness
+-- for a `Pattern` support does not unify.
+--
+-- EXPECT: Mismatch between: Mechanical recheck and Pattern.
+
+module PatternIsNotSound
+
+import Hypatia.ABI.Verdict
+
+%default total
+
+-- Placeholder digests: well-formed, and deliberately not the digest of
+-- anything.  They are scaffolding, not evidence.
+zero : Sha256
+zero = MkSha256 "0000000000000000000000000000000000000000000000000000000000000000"
+
+recheck : ProverRecheck
+recheck = MkProverRecheck Lean4 "4.30.0" "Example.lean" zero zero Confirms
+
+refuted : ProverRecheck
+refuted = MkProverRecheck Lean4 "4.30.0" "Example.lean" zero zero Refutes
+
+token : EvidenceToken
+token = MkEvidenceToken "code_safety" "example_rule" "0.1.0"
+          (MkSpan "Example.lean" 1 1) 1
+
+invalid : SoundVerdict
+invalid = MkSoundVerdict (MkVerdict "claim" [token] Pattern) (Rechecked recheck Refl)
diff --git a/tests/reject/RefutedRecheckIsNotSound.idr b/tests/reject/RefutedRecheckIsNotSound.idr
new file mode 100644
index 00000000..1eb4f8de
--- /dev/null
+++ b/tests/reject/RefutedRecheckIsNotSound.idr
@@ -0,0 +1,37 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- EXPECTED REJECTION (HYP-01).  scripts/check-verdicts.sh passes only if
+-- Idris2 refuses this module, and only at the declaration `invalid`.  Every
+-- other declaration must typecheck, so that the refusal is for the stated
+-- reason and not for a missing import or a typo.
+--
+-- Must fail: a re-check whose result is `Refutes` is not a soundness
+-- map.  `Rechecked` demands `result recheck = Confirms`, and `Refl` cannot
+-- prove `Refutes = Confirms`.
+--
+-- EXPECT: Mismatch between: Confirms and Refutes.
+
+module RefutedRecheckIsNotSound
+
+import Hypatia.ABI.Verdict
+
+%default total
+
+-- Placeholder digests: well-formed, and deliberately not the digest of
+-- anything.  They are scaffolding, not evidence.
+zero : Sha256
+zero = MkSha256 "0000000000000000000000000000000000000000000000000000000000000000"
+
+recheck : ProverRecheck
+recheck = MkProverRecheck Lean4 "4.30.0" "Example.lean" zero zero Confirms
+
+refuted : ProverRecheck
+refuted = MkProverRecheck Lean4 "4.30.0" "Example.lean" zero zero Refutes
+
+token : EvidenceToken
+token = MkEvidenceToken "code_safety" "example_rule" "0.1.0"
+          (MkSpan "Example.lean" 1 1) 1
+
+invalid : SoundVerdict
+invalid = MkSoundVerdict (MkVerdict "claim" [token] (Mechanical refuted)) (Rechecked refuted Refl)
diff --git a/verification/PROOF-STATUS.adoc b/verification/PROOF-STATUS.adoc
index 53c8a4a2..5a62f461 100644
--- a/verification/PROOF-STATUS.adoc
+++ b/verification/PROOF-STATUS.adoc
@@ -127,6 +127,62 @@ downgraded to a runtime assertion in
 JSONL for violations. See commit history.
 |===
 
+==== Verdict support (2026-10-14, HYP-01)
+
+A gate verdict names its support: a pattern match, an observation count, or
+a prover re-check. Only the last can be sound. The statuses here use the
+estate vocabulary (PROVEN / TESTED / ASSUMED / OPEN), and every row names
+the artefact that justifies it. `+scripts/check-verdicts.sh+` (CI: `+idris2
+--check+` job) and `+scripts/recheck-lean-hole.sh+` (CI: `+lake build+` job)
+are the gates.
+
+[width="100%",cols="28%,14%,42%,16%",options="header",]
+|===
+|File |Language |Claim |Status
+|`+src/Hypatia/ABI/Verdict.idr+` |Idris2 |`+Sound+` has one
+constructor, indexed by `+Mechanical+`, demanding a re-check that
+`+Confirms+`: `+patternNotSound+`, `+observedNotSound+`,
+`+refutedNotSound+`; soundness is decidable (`+decSound+`); the derived
+level is "sound" only with a witness (`+soundLevelHasWitness+`,
+`+patternNeverSoundLevel+`, `+observedNeverSoundLevel+`) and a
+`+SoundVerdict+` always derives it (`+soundVerdictLevel+`); a `+Sha256+`
+literal of the wrong shape does not typecheck |PROVEN
+
+|`+tests/reject/PatternIsNotSound.idr+` |Idris2 |Expected rejection: a
+`+Sound+` witness for a `+Pattern+` support is refused at `+invalid+`
+|TESTED
+
+|`+tests/reject/ObservedIsNotSound.idr+` |Idris2 |Expected rejection:
+`+Observed+` 5 (the rules.a2ml proposal threshold) is refused as sound at
+`+invalid+` |TESTED
+
+|`+tests/reject/RefutedRecheckIsNotSound.idr+` |Idris2 |Expected
+rejection: a re-check that `+Refutes+` is refused as sound at `+invalid+`
+|TESTED
+
+|`+tests/reject/MalformedDigest.idr+` |Idris2 |Expected rejection: a
+digest that is not 64 lower-case hex digits is refused at `+invalid+`
+|TESTED
+
+|`+tests/accept/LeanHoleRecheckSound.idr+` |Idris2 + Lean 4 |Positive
+control: `+soundControl+`, a `+SoundVerdict+` for the code_safety Lean
+proof-hole detector, is accepted and derives "sound" by evaluation
+(`+controlIsSound+`); its `+targetHash+` and `+artefactHash+` are
+re-derived from a fresh Lean 4.30.0 run of the fixture, with two negative
+controls (a hole-free module prints no diagnostic; another run yields
+another digest) |TESTED
+
+|`+src/Hypatia/ABI/Verdict.idr+` |Idris2 |Correspondence of
+`+Verdict+` / `+SoundVerdict+` to Epi / SoundWarrant in
+hyperpolymath/epistemic-types @ 6a68de3 (Warrant.agda). The pin and the
+cited names are checked (`+sibling-citations+` CI job); the
+correspondence is a transcription, not a checked proof |ASSUMED
+
+|`+src/Hypatia/ABI/Verdict.idr+` |Idris2 |Elixir rules carry a proof of
+their support tag. They carry the tag only (HYP-01, PR B); no Elixir rule
+is proved sound |OPEN
+|===
+
 === Properties Proven
 
 ==== 1. Confidence Bounds (`+ConfidenceBounds.idr+`)