diff --git a/.github/workflows/mvp-smoke.yml b/.github/workflows/mvp-smoke.yml
index 570f040c..6956ec7b 100644
--- a/.github/workflows/mvp-smoke.yml
+++ b/.github/workflows/mvp-smoke.yml
@@ -32,6 +32,11 @@ jobs:
       - name: Checkout repository
         uses: actions/checkout@v7.0.1
 
+      - name: Gate library and W0 gate self-tests (fixtures, no network)
+        run: |
+          bash scripts/gates/lib.selftest.sh
+          bash scripts/gates/w0.selftest.sh
+
       - name: Setup Rust toolchain
         uses: dtolnay/rust-toolchain@v1
         with:
diff --git a/Justfile b/Justfile
index 3f11a86f..5adaa59a 100644
--- a/Justfile
+++ b/Justfile
@@ -217,6 +217,11 @@ build-release:
 test:
     cargo test --lib
 
+# Self-test the wave gates (scripts/gates/*.selftest.sh): fixtures, no network
+test-gates:
+    bash scripts/gates/lib.selftest.sh
+    bash scripts/gates/w0.selftest.sh
+
 # Run all tests (unit + integration)
 test-all:
     cargo test
diff --git a/scripts/gates/hotspot-goldens.sh b/scripts/gates/hotspot-goldens.sh
new file mode 100755
index 00000000..981356a8
--- /dev/null
+++ b/scripts/gates/hotspot-goldens.sh
@@ -0,0 +1,131 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+#
+# Goldens for NEW:hotspot-split (W0 gate check 5). The split of main.rs into
+# cli/*, server.rs into server/* and the Justfile into just/*.just is a pure
+# move, so these three surfaces must not change:
+#
+#   help/echidna[.<sub>[.<subsub>]].txt   `echidna [<sub> ...] --help`, every
+#                                         subcommand, recursively (depth 3);
+#                                         "." joins the words because clap
+#                                         names never contain one
+#   routes.txt                            every `.route(...)` line under
+#                                         src/rust/, whitespace-trimmed, sorted
+#   router-composition.txt                every Router::new, .merge, .nest,
+#                                         .nest_service, .fallback, .with_state
+#                                         and .layer line under src/rust/, so a
+#                                         route moved into a sub-router that is
+#                                         never mounted shows up as a diff
+#   just-list.txt                         `just --list`
+#
+# Usage:
+#   hotspot-goldens.sh capture [--dir DIR] [--bin PATH]   write the goldens
+#   hotspot-goldens.sh check   [--dir DIR] [--bin PATH]   diff against them
+#
+# Capture on the pre-split tree (origin/main before the split lands), commit
+# the result, and never re-capture to silence a diff after the split.
+# DIR defaults to tests/golden/hotspot. Without --bin the echidna binary is
+# built with `cargo build --locked --bin echidna` into $CARGO_TARGET_DIR
+# (default target/). Run from the repository root.
+#
+# Exit codes: 0 no diff (or captured), 1 diff or missing golden, 2 cannot run.
+
+set -euo pipefail
+export LC_ALL=C
+
+mode="${1:-}"
+[ $# -gt 0 ] && shift
+dir="tests/golden/hotspot"
+bin=""
+while [ $# -gt 0 ]; do
+  case "$1" in
+    --dir) dir="$2"; shift 2 ;;
+    --bin) bin="$2"; shift 2 ;;
+    -h|--help) sed -n '3,31p' "$0"; exit 0 ;;
+    *) echo "unknown argument: $1" >&2; exit 2 ;;
+  esac
+done
+case "$mode" in capture|check) ;; *) sed -n '3,31p' "$0" >&2; exit 2 ;; esac
+
+for tool in just rg; do
+  command -v "$tool" >/dev/null 2>&1 || { echo "cannot run: $tool is not installed" >&2; exit 2; }
+done
+
+if [ -z "$bin" ]; then
+  cargo build --locked --quiet --bin echidna >&2 || { echo "cannot run: cargo build failed" >&2; exit 2; }
+  bin="${CARGO_TARGET_DIR:-target}/debug/echidna"
+fi
+[ -x "$bin" ] || { echo "cannot run: $bin is not executable" >&2; exit 2; }
+
+out=$(mktemp -d)
+trap 'rm -rf "$out"' EXIT
+mkdir -p "$out/help"
+
+# Subcommand names from a clap help text: the indented first words under
+# "Commands:", up to the next blank line. `help` is clap's own and skipped.
+subcommands() {
+  awk '/^Commands:/{on=1; next} on && /^$/{on=0} on && /^  [a-z0-9]/{print $1}' | grep -vx help || true
+}
+
+# help_tree <depth> <args...>
+help_tree() {
+  local depth="$1" name sub text
+  shift
+  name=$(printf '%s' "echidna${*:+ $*}" | tr ' ' '.')
+  local rc=0
+  text=$(NO_COLOR=1 COLUMNS=100 RUST_BACKTRACE=0 "$bin" "$@" --help 2>&1) || rc=$?
+  if [ "$rc" -ne 0 ]; then
+    # A failing --help is behaviour too, and a pure move must keep it. Record
+    # the exit status and the message, without the thread id and the source
+    # path of the panic, which differ between machines.
+    text=$(printf '[exit %d]\n%s' "$rc" "$text" \
+      | sed -E "s/^thread '([^']*)' \\([0-9]+\\) panicked at .*/thread '\\1' panicked:/")
+    echo "note: '$*${*:+ }--help' exits $rc; recorded as behaviour" >&2
+  fi
+  printf '%s\n' "$text" > "$out/help/$name.txt"
+  [ "$depth" -ge 3 ] && return 0
+  for sub in $(printf '%s\n' "$text" | subcommands); do
+    help_tree $((depth + 1)) "$@" "$sub"
+  done
+}
+help_tree 0
+
+# Prefix each matched line with the module that owns it, so moving a
+# `.route(...)` from one router to another changes the golden. The owner is
+# the first path component under src/rust/ with `.rs` removed: server.rs
+# and server/prove.rs are both `server`, groove.rs is `groove`. That keeps
+# the golden invariant under a module split, which is what it guards.
+owned() {
+  awk '{
+    i = index($0, ":"); path = substr($0, 1, i - 1); line = substr($0, i + 1)
+    sub(/^src\/rust\//, "", path); sub(/\/.*$/, "", path); sub(/\.rs$/, "", path)
+    gsub(/^[[:space:]]+|[[:space:]]+$/, "", line)
+    print path ": " line
+  }'
+}
+
+rg --with-filename --no-line-number --glob '*.rs' '^\s*\.route\(' src/rust \
+  | owned | sort > "$out/routes.txt" || true
+[ -s "$out/routes.txt" ] || { echo "cannot run: no .route( lines found under src/rust" >&2; exit 2; }
+
+rg --with-filename --no-line-number --glob '*.rs' \
+   '(^|[^A-Za-z0-9_])Router::new\(|\.(merge|nest|nest_service|fallback|with_state|layer)\(' src/rust \
+  | owned | sort > "$out/router-composition.txt" || true
+[ -s "$out/router-composition.txt" ] || { echo "cannot run: no Router::new( lines found under src/rust" >&2; exit 2; }
+
+just --list > "$out/just-list.txt" 2>&1 || { echo "cannot run: just --list failed" >&2; exit 2; }
+
+if [ "$mode" = capture ]; then
+  mkdir -p "$dir"
+  rm -rf "$dir/help"
+  cp -R "$out/." "$dir/"
+  echo "captured $(find "$dir" -type f | wc -l) golden files into $dir"
+  exit 0
+fi
+
+[ -d "$dir" ] || { echo "golden directory $dir is missing; capture it on the pre-split tree" >&2; exit 1; }
+if diff -ruN "$dir" "$out"; then
+  echo "hotspot goldens: no diff ($(find "$out" -type f | wc -l) files)"
+  exit 0
+fi
+exit 1
diff --git a/scripts/gates/lib.selftest.sh b/scripts/gates/lib.selftest.sh
new file mode 100755
index 00000000..fb22a5a3
--- /dev/null
+++ b/scripts/gates/lib.selftest.sh
@@ -0,0 +1,132 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+#
+# Self-test for scripts/gates/lib.sh. Each case runs a tiny gate in a child
+# bash and checks its exit status (and, where it matters, its output).
+#
+# Usage: scripts/gates/lib.selftest.sh     Exit 0 iff every case behaves.
+
+# SC2001: sed prefixes multi-line output, which ${var//} cannot do per line.
+# shellcheck disable=SC2001
+set -uo pipefail
+
+here=$(cd "$(dirname "$0")" && pwd)
+lib="$here/lib.sh"
+tmp=$(mktemp -d)
+trap 'rm -rf "$tmp"' EXIT
+
+failures=0
+cases=0
+
+# run_gate <body>: run a gate whose checks are <body>; prints its output,
+# returns its exit status.
+run_gate() {
+  bash -c ". '$lib'; gate_init selftest; $1; gate_finish"
+}
+
+# expect <name> <want: zero|nonzero> <body> [grep-pattern]
+expect() {
+  local name="$1" want="$2" body="$3" pattern="${4:-}" out rc ok=1
+  cases=$((cases + 1))
+  out=$(run_gate "$body" 2>&1)
+  rc=$?
+  case "$want" in
+    zero) [ "$rc" -eq 0 ] || ok=0 ;;
+    nonzero) [ "$rc" -ne 0 ] || ok=0 ;;
+  esac
+  if [ -n "$pattern" ] && ! printf '%s\n' "$out" | grep -qE -- "$pattern"; then
+    ok=0
+  fi
+  if [ "$ok" -eq 1 ]; then
+    echo "ok   $name (exit $rc)"
+  else
+    failures=$((failures + 1))
+    echo "FAIL $name: wanted $want exit${pattern:+ and output matching /$pattern/}, got exit $rc"
+    printf '%s\n' "$out" | sed 's/^/     | /'
+  fi
+}
+
+expect "all pass exits 0" zero \
+  'pass a "one"; pass b "two"' \
+  'selftest: 2 pass, 0 fail, 0 deferred'
+
+expect "a FAIL exits non-zero" nonzero \
+  'pass a "one"; fail b "broken"; pass c "three"' \
+  'selftest: 2 pass, 1 fail, 0 deferred'
+
+for reason in ruling:R0 secret:GITHUB_TOKEN hardware:8-core owner-host:P0-6 no-push:proof-burrower; do
+  expect "DEFERRED($reason) exits 0" zero \
+    "pass a one; deferred b '$reason' 'waiting'" \
+    "DEFERRED\\($reason\\)"
+done
+
+for reason in flaky "tool:just" "ruling:" "ruling" "" "secret:two words" "later:soon" "no-push"; do
+  expect "DEFERRED('$reason') is a FAIL" nonzero \
+    "pass a one; deferred b '$reason' 'waiting'" \
+    'not permitted'
+done
+
+expect "an empty gate fails" nonzero ':' 'no checks were recorded'
+
+expect "a duplicated check id fails" nonzero \
+  'pass a one; pass a again' 'recorded twice'
+
+expect "gate_cmd PASS on exit 0" zero 'gate_cmd a "true runs" -- true'
+
+expect "gate_cmd FAIL on non-zero exit" nonzero \
+  'gate_cmd a "false runs" -- sh -c "echo boom; exit 3"' 'exit 3; boom'
+
+# GATE_REPORT writes one JCS object per check.
+cases=$((cases + 1))
+report="$tmp/report.jsonl"
+GATE_REPORT="$report" run_gate 'pass a "x"; deferred b secret:GITHUB_TOKEN "y"; fail c "z \"q\""' >/dev/null 2>&1
+if [ "$(wc -l < "$report")" -eq 3 ] \
+  && [ "$(jq -cS . "$report")" = "$(cat "$report")" ] \
+  && [ "$(jq -r '.result' "$report" | tr '\n' ' ')" = "PASS DEFERRED FAIL " ] \
+  && [ "$(sed -n 2p "$report")" = '{"check":"b","detail":"y","reason":"secret:GITHUB_TOKEN","result":"DEFERRED"}' ]; then
+  echo "ok   GATE_REPORT is JCS JSON Lines"
+else
+  failures=$((failures + 1))
+  echo "FAIL GATE_REPORT is JCS JSON Lines"
+  sed 's/^/     | /' "$report"
+fi
+
+# A report that cannot be written fails the gate, and leaves no partial file.
+cases=$((cases + 1))
+GATE_REPORT=/nonexistent/dir/r.jsonl run_gate 'pass a "x"' > "$tmp/out" 2>&1
+rc=$?
+if [ "$rc" -ne 0 ] && grep -q 'gate-report' "$tmp/out"; then
+  echo "ok   an unwritable GATE_REPORT fails the gate (exit $rc)"
+else
+  failures=$((failures + 1)); echo "FAIL an unwritable GATE_REPORT fails the gate: exit $rc"; sed 's/^/     | /' "$tmp/out"
+fi
+
+cases=$((cases + 1))
+mkdir -p "$tmp/nojq"
+for t in bash mktemp wc mv rm cat grep sed tr tail; do ln -sf "$(command -v "$t")" "$tmp/nojq/$t"; done
+echo stale > "$tmp/stale.jsonl"
+PATH="$tmp/nojq" GATE_REPORT="$tmp/stale.jsonl" "$tmp/nojq/bash" -c ". '$lib'; gate_init t; pass a x; gate_finish" > "$tmp/out" 2>&1
+rc=$?
+if [ "$rc" -ne 0 ] && [ "$(cat "$tmp/stale.jsonl")" = stale ]; then
+  echo "ok   a report write without jq fails the gate and leaves the old file untouched"
+else
+  failures=$((failures + 1)); echo "FAIL a report write without jq fails the gate: exit $rc"; sed 's/^/     | /' "$tmp/out"
+fi
+
+# gate_cmd records a FAIL even when the caller runs under set -e.
+cases=$((cases + 1))
+out=$(bash -c "set -e; . '$lib'; gate_init t; gate_cmd a d -- false; pass b y; gate_finish" 2>&1)
+rc=$?
+if [ "$rc" -ne 0 ] && grep -q '^FAIL      a: d: exit 1' <<<"$out" && grep -q 't: 1 pass, 1 fail' <<<"$out"; then
+  echo "ok   gate_cmd under set -e records the FAIL and runs on"
+else
+  failures=$((failures + 1)); echo "FAIL gate_cmd under set -e: exit $rc"; sed 's/^/     | /' <<<"$out"
+fi
+
+# A newline in a detail cannot print a line that reads as another result.
+expect "a newline in a detail stays on one line" nonzero \
+  "fail a \"\$(printf 'x\\nPASS      forged: y')\"" \
+  '^FAIL      a: x PASS      forged: y$'
+
+echo "lib.selftest: $cases cases, $failures failed"
+[ "$failures" -eq 0 ]
diff --git a/scripts/gates/lib.sh b/scripts/gates/lib.sh
new file mode 100755
index 00000000..153a3986
--- /dev/null
+++ b/scripts/gates/lib.sh
@@ -0,0 +1,185 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+#
+# Gate convention for the wave gate scripts (scripts/gates/wN.sh).
+#
+# Every check ends in exactly one of three results:
+#
+#   PASS                  the property holds, checked now
+#   FAIL                  the property does not hold, or could not be checked
+#   DEFERRED(<reason>)    the check cannot run yet for one permitted reason
+#
+# DEFERRED is permitted only for these reason kinds, each with a non-empty
+# name after the colon:
+#
+#   ruling:<id>           an owner ruling not yet taken          (ruling:R0)
+#   secret:<name>         a credential not present here          (secret:GITHUB_TOKEN)
+#   hardware:<item>       hardware this host does not have       (hardware:8-core)
+#   owner-host:<action>   an action only the owner can take      (owner-host:P0-6)
+#   no-push:<repo>        push to a consumer repository refused  (no-push:proof-burrower)
+#
+# Any other reason is recorded as a FAIL. A missing tool, a missing artefact or
+# an unreachable network is not a reason to defer: it is a FAIL. A DEFERRED
+# check moves to the next wave's gate script and to STATUS (ultraplan
+# convention (a)).
+#
+# Use from a gate script:
+#
+#   . "$(dirname "$0")/lib.sh"
+#   gate_init W0
+#   pass     <id> <detail>
+#   fail     <id> <detail>
+#   deferred <id> <reason> <detail>
+#   gate_finish            # prints the summary, exits 0 iff no FAIL
+#
+# A gate that records no checks fails: an empty gate is not a green gate.
+# A check id recorded twice fails, so a copy-paste slip cannot hide a check.
+#
+# Set GATE_REPORT=<path> to also write one JCS object per check (JSON Lines,
+# keys check/detail/reason/result, all strings) for the STATUS generator.
+#
+# Requires bash 4 and, only when GATE_REPORT is set, jq.
+
+# Not `set -e` here: the sourcing script owns its shell options.
+
+GATE_ALLOWED_DEFER_KINDS="ruling secret hardware owner-host no-push"
+
+gate_init() {
+  GATE_NAME="${1:-gate}"
+  GATE_IDS=()
+  GATE_RESULTS=()
+  GATE_REASONS=()
+  GATE_DETAILS=()
+  GATE_FAILS=0
+  GATE_PASSES=0
+  GATE_DEFERS=0
+}
+
+# _gate_flat <text>: the text on one line. A newline or carriage return in a
+# detail could otherwise print a line that reads like another check's result.
+_gate_flat() {
+  local s="$1"
+  s="${s//$'\r'/ }"
+  printf '%s' "${s//$'\n'/ }"
+}
+
+# _gate_record <id> <result> <reason> <detail>
+_gate_record() {
+  local id result="$2" reason="$3" detail seen
+  id=$(_gate_flat "$1")
+  detail=$(_gate_flat "$4")
+  if [ -z "$id" ]; then
+    id="(unnamed)"
+    result=FAIL
+    reason=""
+    detail="check recorded without an id: $detail"
+  fi
+  for seen in ${GATE_IDS[@]+"${GATE_IDS[@]}"}; do
+    if [ "$seen" = "$id" ]; then
+      result=FAIL
+      reason=""
+      detail="check id recorded twice: $detail"
+      id="$id#dup"
+      break
+    fi
+  done
+  GATE_IDS+=("$id")
+  GATE_RESULTS+=("$result")
+  GATE_REASONS+=("$reason")
+  GATE_DETAILS+=("$detail")
+  case "$result" in
+    PASS) GATE_PASSES=$((GATE_PASSES + 1)); printf 'PASS      %s: %s\n' "$id" "$detail" ;;
+    DEFERRED) GATE_DEFERS=$((GATE_DEFERS + 1)); printf 'DEFERRED  %s (%s): %s\n' "$id" "$reason" "$detail" ;;
+    *) GATE_FAILS=$((GATE_FAILS + 1)); printf 'FAIL      %s: %s\n' "$id" "$detail" ;;
+  esac
+}
+
+# gate_reason_allowed <reason>: 0 iff the reason is one permitted DEFERRED kind
+# with a non-empty, whitespace-free name.
+gate_reason_allowed() {
+  local reason="$1" kind name k
+  case "$reason" in *:*) ;; *) return 1 ;; esac
+  kind="${reason%%:*}"
+  name="${reason#*:}"
+  [[ $name =~ ^[A-Za-z0-9][A-Za-z0-9._#/@+-]*$ ]] || return 1
+  for k in $GATE_ALLOWED_DEFER_KINDS; do
+    [ "$k" = "$kind" ] && return 0
+  done
+  return 1
+}
+
+pass() { _gate_record "${1:-}" PASS "" "${2:-}"; }
+
+fail() { _gate_record "${1:-}" FAIL "" "${2:-}"; }
+
+deferred() {
+  local id="${1:-}" reason="${2:-}" detail="${3:-}"
+  if gate_reason_allowed "$reason"; then
+    _gate_record "$id" DEFERRED "$reason" "$detail"
+  else
+    _gate_record "$id" FAIL "" "DEFERRED reason '$reason' is not permitted (allowed kinds: $GATE_ALLOWED_DEFER_KINDS, as kind:name): $detail"
+  fi
+}
+
+# gate_cmd <id> <detail> -- <command...>: PASS when the command exits 0,
+# otherwise FAIL with its exit status and the last lines of its output.
+gate_cmd() {
+  local id="$1" detail="$2" out rc
+  shift 2
+  [ "${1:-}" = "--" ] && shift
+  # `&& rc=0 || rc=$?` keeps a failing command from aborting a caller that
+  # runs under `set -e` before its FAIL is recorded.
+  out=$("$@" 2>&1) && rc=0 || rc=$?
+  if [ "$rc" -eq 0 ]; then
+    pass "$id" "$detail"
+  else
+    fail "$id" "$detail: exit $rc; $(printf '%s\n' "$out" | tail -n 5 | tr '\n' ' ')"
+  fi
+}
+
+gate_summary() {
+  local i n="${#GATE_IDS[@]}"
+  if [ "$n" -eq 0 ]; then
+    _gate_record "gate-nonempty" FAIL "" "no checks were recorded"
+    n="${#GATE_IDS[@]}"
+  fi
+  printf '\n== %s gate summary ==\n' "$GATE_NAME"
+  for ((i = 0; i < n; i++)); do
+    case "${GATE_RESULTS[$i]}" in
+      DEFERRED) printf '  %-34s DEFERRED(%s)\n' "${GATE_IDS[$i]}" "${GATE_REASONS[$i]}" ;;
+      *) printf '  %-34s %s\n' "${GATE_IDS[$i]}" "${GATE_RESULTS[$i]}" ;;
+    esac
+  done
+  printf '%s: %d pass, %d fail, %d deferred\n' "$GATE_NAME" "$GATE_PASSES" "$GATE_FAILS" "$GATE_DEFERS"
+  if [ -n "${GATE_REPORT:-}" ] && ! _gate_write_report "$n"; then
+    # The STATUS generator reads this file. A missing, empty or stale report
+    # must not sit beside a green exit.
+    printf 'FAIL      gate-report: cannot write GATE_REPORT=%s\n' "$GATE_REPORT"
+    return 1
+  fi
+  [ "$GATE_FAILS" -eq 0 ]
+}
+
+# _gate_write_report <n>: write the report to a temporary file beside the
+# target and move it into place, so a failed write never leaves a partial or
+# stale report under the target name.
+_gate_write_report() {
+  local n="$1" i tmp
+  command -v jq >/dev/null 2>&1 || return 1
+  tmp=$(mktemp "${GATE_REPORT}.XXXXXX" 2>/dev/null) || return 1
+  for ((i = 0; i < n; i++)); do
+    jq -cnS --arg check "${GATE_IDS[$i]}" --arg result "${GATE_RESULTS[$i]}" \
+      --arg reason "${GATE_REASONS[$i]}" --arg detail "${GATE_DETAILS[$i]}" \
+      '{check: $check, detail: $detail, reason: $reason, result: $result}' >> "$tmp" \
+      || { rm -f "$tmp"; return 1; }
+  done
+  [ "$(wc -l < "$tmp")" -eq "$n" ] || { rm -f "$tmp"; return 1; }
+  mv -f "$tmp" "$GATE_REPORT" || { rm -f "$tmp"; return 1; }
+}
+
+gate_finish() {
+  if gate_summary; then
+    exit 0
+  fi
+  exit 1
+}
diff --git a/scripts/gates/w0.selftest.sh b/scripts/gates/w0.selftest.sh
new file mode 100755
index 00000000..c041c17a
--- /dev/null
+++ b/scripts/gates/w0.selftest.sh
@@ -0,0 +1,432 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+#
+# Fixture tests for scripts/gates/w0.sh. Each case builds a scratch git
+# repository holding the gate scripts and one planted artefact, serves the
+# GitHub API from files through a stub curl, runs the gate with W0_CHECKS
+# set to the check under test, and asserts the result line for that check.
+# No network, cargo or GitHub token is used.
+#
+# The planted artefacts include each false green found in review: a commit
+# with more than 100 check runs, governance jobs named "... conformance",
+# empty untracked handover files, blank and glob backend names, nudged
+# fabricated metrics, a one-heading rulings ledger, a "nix flake" claim,
+# legacy statuses and rules past page one, a pinned context met by the
+# wrong app, inline `#` comments, ledger sections inside comment blocks and
+# a claims.json whose root is an array.
+#
+# Usage: scripts/gates/w0.selftest.sh     Exit 0 iff every case behaves.
+
+# SC2001: sed prefixes multi-line output, which ${var//} cannot do per line.
+# SC2016: fixture text holds a literal $pattern on purpose.
+# shellcheck disable=SC2001,SC2016
+set -uo pipefail
+export LC_ALL=C
+
+here=$(cd "$(dirname "$0")" && pwd)
+tmp=$(mktemp -d)
+trap 'rm -rf "$tmp"' EXIT
+failures=0
+cases=0
+
+# ------------------------------------------------------------- scaffolding
+
+mkdir -p "$tmp/bin"
+cat > "$tmp/bin/curl" <<'EOF'
+#!/usr/bin/env bash
+# Serves https://api.github.com/<path> from $STUB_API/<path with /?&= as _>
+# and logs its arguments, one call per line, to $STUB_API.calls.
+url="${*: -1}"
+printf '%s\n' "$*" >> "$STUB_API.calls"
+key=$(printf '%s' "${url#https://api.github.com/}" | tr '/?&=' '____')
+[ -f "$STUB_API/$key" ] || { echo "curl stub: no fixture for $url" >&2; exit 22; }
+cat "$STUB_API/$key"
+EOF
+chmod +x "$tmp/bin/curl"
+
+# new_repo: a fresh scratch repository with the gate scripts committed;
+# sets R (its path) and STUB_API (its API fixture directory).
+new_repo() {
+  R=$(mktemp -d "$tmp/repo.XXXXXX")
+  STUB_API="$R.api"
+  mkdir -p "$R/scripts/gates" "$STUB_API"
+  cp "$here/lib.sh" "$here/w0.sh" "$here/hotspot-goldens.sh" "$R/scripts/gates/"
+  git -C "$R" init -q -b main
+  git -C "$R" -c user.email=t@t -c user.name=t add -A
+  git -C "$R" -c user.email=t@t -c user.name=t commit -qm base
+}
+
+commit_all() {
+  git -C "$R" -c user.email=t@t -c user.name=t add -A
+  git -C "$R" -c user.email=t@t -c user.name=t commit -qm "${1:-fixture}"
+}
+
+# serve <api path> <body>: the stub curl answers <api path> with <body>.
+serve() {
+  printf '%s\n' "$2" > "$STUB_API/$(printf '%s' "$1" | tr '/?&=' '____')"
+}
+
+# serve_status <repo> <sha> <body>: page 1 of the combined commit status.
+# The unpaged path is served the same body, so the cases also run against
+# the gate before it paginated (to show they fail there).
+serve_status() {
+  serve "repos/$1/commits/$2/status?per_page=100&page=1" "$3"
+  serve "repos/$1/commits/$2/status" "$3"
+}
+
+# serve_rules <body>: page 1 of the echidna main rules (and the unpaged path).
+serve_rules() {
+  serve "repos/hyperpolymath/echidna/rules/branches/main?per_page=100&page=1" "$1"
+  serve "repos/hyperpolymath/echidna/rules/branches/main" "$1"
+}
+
+# runs_json <count> <failing name or ""> <name padding>: a check-runs page.
+runs_json() {
+  jq -cn --argjson n "$1" --arg bad "$2" --arg pad "$3" --argjson off "${4:-0}" '
+    {total_count: $n, check_runs: [range($n) as $i
+      | {id: ($i + $off + 1), name: ("job-\($i + $off)-" + $pad), status: "completed",
+         conclusion: (if ("job-\($i + $off)-" + $pad) == $bad then "failure" else "success" end)}]}'
+}
+
+# gate <checks> [VAR=value ...]: run w0.sh in $R; output in $OUT.
+gate() {
+  local checks="$1"
+  shift
+  OUT=$(cd "$R" && env PATH="$tmp/bin:$PATH" STUB_API="$STUB_API" GITHUB_TOKEN= \
+    W0_CHECKS="$checks" "$@" bash scripts/gates/w0.sh 2>&1)
+  RC=$?
+}
+
+# expect <case name> <PASS|FAIL|DEFERRED> <check id> [extra grep pattern]
+expect() {
+  local name="$1" want="$2" id="$3" pattern="${4:-}" ok=1
+  cases=$((cases + 1))
+  grep -qE "^$want +$id( |:)" <<<"$OUT" || ok=0
+  if [ -n "$pattern" ] && ! grep -qE -- "$pattern" <<<"$OUT"; then ok=0; fi
+  # A subset run must never exit 0.
+  [ "$RC" -ne 0 ] || ok=0
+  if [ "$ok" -eq 1 ]; then
+    echo "ok   $name"
+  else
+    failures=$((failures + 1))
+    echo "FAIL $name: wanted $want $id${pattern:+ and /$pattern/}, exit non-zero; got exit $RC"
+    sed 's/^/     | /' <<<"$OUT"
+  fi
+}
+
+# --------------------------------------------- check 2: >100 check runs
+
+new_repo
+base=$(git -C "$R" rev-parse HEAD)
+echo x > "$R/f"; commit_all merge
+head=$(git -C "$R" rev-parse HEAD)
+pad=$(printf 'p%.0s' $(seq 1 1500))
+serve "repos/hyperpolymath/echidna/commits/$head/check-runs?per_page=100&page=1" "$(runs_json 100 "" "$pad")"
+serve "repos/hyperpolymath/echidna/commits/$head/check-runs?per_page=100&page=2" "$(runs_json 50 "job-140-$pad" "$pad" 100)"
+serve_status hyperpolymath/echidna "$head" '{"state":"pending","total_count":0,"statuses":[]}'
+gate 2 W0_BASE="$base" W0_HEAD="$head"
+expect "check 2 sees a failure on page 2 of 150 large runs" FAIL 02-w0-merges-green "job-140-p+=failure"
+
+serve "repos/hyperpolymath/echidna/commits/$head/check-runs?per_page=100&page=2" "$(runs_json 50 "" "$pad" 100)"
+gate 2 W0_BASE="$base" W0_HEAD="$head"
+expect "check 2 passes when all 150 runs succeed" PASS 02-w0-merges-green
+
+serve "repos/hyperpolymath/echidna/commits/$head/check-runs?per_page=100&page=2" 'not json'
+gate 2 W0_BASE="$base" W0_HEAD="$head"
+expect "check 2 fails closed on an unparseable page" FAIL 02-w0-merges-green "unreadable"
+
+rm -f "$STUB_API"/*page_2
+gate 2 W0_BASE="$base" W0_HEAD="$head"
+expect "check 2 fails closed on an unreadable page" FAIL 02-w0-merges-green "unreadable"
+
+# ------------------------------- check 2: legacy statuses beyond page one
+
+# statuses_json <count> <state of the last one> <combined state> <total> [offset]
+statuses_json() {
+  jq -cn --argjson n "$1" --arg last "$2" --arg st "$3" --argjson t "$4" --argjson off "${5:-0}" '
+    {state: $st, total_count: $t, statuses: [range($n) as $i
+      | {context: "legacy-\($i + $off)", state: (if $i == $n - 1 then $last else "success" end)}]}'
+}
+new_repo
+base=$(git -C "$R" rev-parse HEAD)
+echo x > "$R/f"; commit_all merge
+head=$(git -C "$R" rev-parse HEAD)
+serve "repos/hyperpolymath/echidna/commits/$head/check-runs?per_page=100&page=1" "$(runs_json 1 "" x)"
+serve_status hyperpolymath/echidna "$head" "$(statuses_json 100 success failure 101)"
+serve "repos/hyperpolymath/echidna/commits/$head/status?per_page=100&page=2" "$(statuses_json 1 failure failure 101 100)"
+gate 2 W0_BASE="$base" W0_HEAD="$head"
+expect "check 2 reads a red legacy status on page 2 of the statuses" FAIL 02-w0-merges-green "legacy-100=failure"
+
+rm -f "$STUB_API"/*status_per_page_100_page_2
+gate 2 W0_BASE="$base" W0_HEAD="$head"
+expect "check 2 fails closed when a statuses page is missing" FAIL 02-w0-merges-green "unreadable"
+
+serve_status hyperpolymath/echidna "$head" "$(statuses_json 2 success failure 2)"
+gate 2 W0_BASE="$base" W0_HEAD="$head"
+expect "check 2 requires the combined legacy state to be success" FAIL 02-w0-merges-green "combined status=failure"
+
+serve_status hyperpolymath/echidna "$head" "$(statuses_json 100 success success 101)"
+serve "repos/hyperpolymath/echidna/commits/$head/status?per_page=100&page=2" "$(statuses_json 1 success success 101 100)"
+gate 2 W0_BASE="$base" W0_HEAD="$head"
+expect "check 2 passes 101 green legacy statuses over two pages" PASS 02-w0-merges-green
+
+# ----------------------------------------- check 1: probe PR required contexts
+
+new_repo
+psha=0123456789abcdef0123456789abcdef0123abcd
+serve_rules '[{"type":"required_status_checks","parameters":{"required_status_checks":[{"context":"rust-ci / Cargo test"},{"context":"gitleaks"}]}}]'
+serve "repos/hyperpolymath/echidna/pulls/7" "{\"head\":{\"sha\":\"$psha\"}}"
+serve_status hyperpolymath/echidna "$psha" '{"state":"success","total_count":1,"statuses":[{"context":"gitleaks","state":"success"}]}'
+serve "repos/hyperpolymath/echidna/commits/$psha/check-runs?per_page=100&page=1" '{"check_runs":[{"id":1,"name":"rust-ci / Cargo test","status":"completed","conclusion":"failure"}]}'
+gate 1 W0_PROBE_PR=7
+expect "a red required context fails check 1 by name" FAIL 01-probe-pr-required-contexts "not success: rust-ci / Cargo test;"
+serve "repos/hyperpolymath/echidna/commits/$psha/check-runs?per_page=100&page=1" '{"check_runs":[{"id":1,"name":"rust-ci / Cargo test","status":"completed","conclusion":"success"}]}'
+gate 1 W0_PROBE_PR=7
+expect "every required context green passes check 1" PASS 01-probe-pr-required-contexts "all 2 required contexts"
+gate 1
+expect "check 1 needs W0_PROBE_PR" FAIL 01-probe-pr-required-contexts "W0_PROBE_PR is not set"
+serve_rules '[]'
+gate 1 W0_PROBE_PR=7
+expect "a ruleset with no required context fails check 1" FAIL 01-probe-pr-required-contexts "requires no status context"
+
+# Pinned contexts: integration_id names the app whose check run counts.
+pinned='[{"type":"required_status_checks","parameters":{"required_status_checks":[{"context":"rust-ci / Cargo test","integration_id":15368},{"context":"gitleaks"}]}}]'
+serve_rules "$pinned"
+serve "repos/hyperpolymath/echidna/commits/$psha/check-runs?per_page=100&page=1" '{"check_runs":[{"id":1,"name":"rust-ci / Cargo test","status":"completed","conclusion":"success","app":{"id":999}}]}'
+gate 1 W0_PROBE_PR=7
+expect "a run from another app does not satisfy a pinned context" FAIL 01-probe-pr-required-contexts "not success: rust-ci / Cargo test \(app 15368\);"
+serve "repos/hyperpolymath/echidna/commits/$psha/check-runs?per_page=100&page=1" '{"check_runs":[]}'
+serve_status hyperpolymath/echidna "$psha" '{"state":"success","total_count":2,"statuses":[{"context":"gitleaks","state":"success"},{"context":"rust-ci / Cargo test","state":"success"}]}'
+gate 1 W0_PROBE_PR=7
+expect "a legacy status does not satisfy a pinned context" FAIL 01-probe-pr-required-contexts "rust-ci / Cargo test \(app 15368\)"
+serve "repos/hyperpolymath/echidna/commits/$psha/check-runs?per_page=100&page=1" '{"check_runs":[{"id":1,"name":"rust-ci / Cargo test","status":"completed","conclusion":"success","app":{"id":999}},{"id":2,"name":"rust-ci / Cargo test","status":"completed","conclusion":"success","app":{"id":15368}}]}'
+gate 1 W0_PROBE_PR=7
+expect "a green run from the pinned app passes check 1" PASS 01-probe-pr-required-contexts "all 2 required contexts"
+
+# Rules on page 2: page 1 is full (100 rules), the red context is on page 2.
+serve_status hyperpolymath/echidna "$psha" '{"state":"success","total_count":1,"statuses":[{"context":"gitleaks","state":"success"}]}'
+serve_rules "$(jq -cn '[range(99) | {type: "deletion"}] + [{type: "required_status_checks", parameters: {required_status_checks: [{context: "gitleaks"}]}}]')"
+serve "repos/hyperpolymath/echidna/rules/branches/main?per_page=100&page=2" '[{"type":"required_status_checks","parameters":{"required_status_checks":[{"context":"rust-ci / Cargo test"}]}}]'
+serve "repos/hyperpolymath/echidna/commits/$psha/check-runs?per_page=100&page=1" '{"check_runs":[{"id":1,"name":"rust-ci / Cargo test","status":"completed","conclusion":"failure"}]}'
+gate 1 W0_PROBE_PR=7
+expect "a required context in rules page 2 still gates check 1" FAIL 01-probe-pr-required-contexts "not success: rust-ci / Cargo test;"
+rm -f "$STUB_API"/*main_per_page_100_page_2
+gate 1 W0_PROBE_PR=7
+expect "check 1 fails closed when a rules page is missing" FAIL 01-probe-pr-required-contexts "cannot read the live ruleset"
+
+# Every GitHub API request is bounded in time.
+cases=$((cases + 1))
+if [ -s "$STUB_API.calls" ] \
+   && ! grep -vE -- '--connect-timeout [0-9]+ ' "$STUB_API.calls" | grep -q . \
+   && ! grep -vE -- '--max-time [0-9]+ ' "$STUB_API.calls" | grep -q . \
+   && ! grep -vE -- '--retry-max-time [0-9]+ ' "$STUB_API.calls" | grep -q .; then
+  echo "ok   every GitHub API request sets connect, total and retry time limits"
+else
+  failures=$((failures + 1)); echo "FAIL every GitHub API request sets connect, total and retry time limits"
+  sed 's/^/     | /' "$STUB_API.calls" | head -n 3
+fi
+
+# ------------------------------------------- checks 11/12: consumer repos
+
+# consumer <repo> <runs json>: serve the repo, its head and its runs.
+consumer() {
+  serve "repos/hyperpolymath/$1" '{"default_branch":"main"}'
+  serve "repos/hyperpolymath/$1/commits/main" '{"sha":"0123456789abcdef0123456789abcdef01234567"}'
+  serve "repos/hyperpolymath/$1/commits/0123456789abcdef0123456789abcdef01234567/check-runs?per_page=100&page=1" "$2"
+}
+gov='{"check_runs":[{"id":1,"name":"governance / UUID v7 conformance","status":"completed","conclusion":"success"},{"id":2,"name":"KYAML conformance","status":"completed","conclusion":"success"}]}'
+good='{"check_runs":[{"id":3,"name":"ci / prove-result-conformance","status":"completed","conclusion":"success"},{"id":4,"name":"verisim-api-list","status":"completed","conclusion":"success"}]}'
+
+new_repo
+for r in echidnabot proof-burrower panic-attack verisimdb; do consumer "$r" "$gov"; done
+gate 11
+expect "governance '... conformance' jobs do not satisfy check 11" FAIL 11-conformance-panic-attack "no check run named 'prove-result-conformance'"
+
+for r in echidnabot proof-burrower panic-attack verisimdb; do consumer "$r" "$good"; done
+gate 11
+expect "the named conformance job passes check 11" PASS 11-conformance-panic-attack
+expect "the verisim-api-list job passes check 11" PASS 11-conformance-verisimdb
+
+for r in echidnabot proof-burrower panic-attack verisimdb; do consumer "$r" "$gov"; done
+mkdir -p "$R/docs/handover/cross-repo/panic-attack"
+: > "$R/docs/handover/cross-repo/panic-attack/x.patch"
+: > "$R/docs/handover/cross-repo/panic-attack/issue.md"
+: > "$R/docs/handover/cross-repo/panic-attack/PUSH-REFUSED.txt"
+gate 11
+expect "empty untracked handover files do not defer" FAIL 11-conformance-panic-attack "no committed handover"
+
+for f in x.patch issue.md PUSH-REFUSED.txt; do echo content > "$R/docs/handover/cross-repo/panic-attack/$f"; done
+gate 11
+expect "non-empty but uncommitted handover does not defer" FAIL 11-conformance-panic-attack "no committed handover"
+
+rm "$R/docs/handover/cross-repo/panic-attack/PUSH-REFUSED.txt"; commit_all handover
+gate 11
+expect "a handover without PUSH-REFUSED.txt does not defer" FAIL 11-conformance-panic-attack
+
+echo "remote: Permission denied" > "$R/docs/handover/cross-repo/panic-attack/PUSH-REFUSED.txt"; commit_all refused
+gate 11
+expect "a committed handover with the refusal defers" DEFERRED 11-conformance-panic-attack "no-push:panic-attack"
+
+echo edited >> "$R/docs/handover/cross-repo/panic-attack/issue.md"
+gate 11
+expect "a handover with uncommitted edits does not defer" FAIL 11-conformance-panic-attack "no committed handover"
+git -C "$R" checkout -q -- docs/handover
+
+: > "$R/docs/handover/cross-repo/panic-attack/PUSH-REFUSED.txt"; commit_all empty-refusal
+gate 11
+expect "a committed but empty PUSH-REFUSED.txt does not defer" FAIL 11-conformance-panic-attack "no committed handover"
+echo "remote: Permission denied" > "$R/docs/handover/cross-repo/panic-attack/PUSH-REFUSED.txt"; commit_all refused-again
+
+consumer panic-attack "$good"
+gate 11
+expect "a green job passes even when a handover exists" PASS 11-conformance-panic-attack
+
+consumer proof-burrower "$gov"
+mkdir -p "$R/docs/handover/cross-repo/proof-burrower"
+for f in fix.patch issue.md PUSH-REFUSED.txt; do echo c > "$R/docs/handover/cross-repo/proof-burrower/$f"; done
+commit_all pb
+gate 12
+expect "check 12 needs the patch to be the Agda one" FAIL 12-proof-burrower-agda
+git -C "$R" mv docs/handover/cross-repo/proof-burrower/fix.patch docs/handover/cross-repo/proof-burrower/agda-ci.patch; commit_all pb-agda
+gate 12
+expect "check 12 defers with an Agda patch" DEFERRED 12-proof-burrower-agda
+
+# ------------------------------------------------- check 6a: XFAIL ledger
+
+xfail() { mkdir -p "$R/tests/fixtures"; printf '%s\n' "$1" > "$R/tests/fixtures/XFAIL.json"; gate 6; }
+new_repo
+xfail '[{"backend":""},{"backend":" "},{"backend":"","prover":"vampire"}]'
+expect "blank backend names fail 06a" FAIL 06a-xfail-ledger "does not name its backend"
+xfail '{"entries":[{"backend":"\n"}]}'
+expect "a newline backend name fails 06a" FAIL 06a-xfail-ledger
+xfail '[{"backend":"*"}]'
+expect "a glob backend name fails 06a without expanding" FAIL 06a-xfail-ledger "does not name its backend"
+xfail '[{"backend":"agda z3"}]'
+expect "a two-word backend name fails 06a" FAIL 06a-xfail-ledger
+xfail '[{"backend":"vampire"}]'
+expect "an out-of-scope backend fails 06a" FAIL 06a-xfail-ledger "outside V-3 scope: vampire"
+xfail '[{"backend":"z3"},{"prover":"agda"}]'
+expect "in-scope backends pass 06a" PASS 06a-xfail-ledger "2 entries"
+xfail '[]'
+expect "an empty ledger passes 06a" PASS 06a-xfail-ledger "empty"
+
+# ---------------------------------------------- check 9: training metrics
+
+metrics() { mkdir -p "$R/models"; printf '%s\n' "$1" > "$R/models/training_metrics.json"; gate 9; }
+new_repo
+gate 9
+expect "absent metrics pass check 9" PASS 09-no-fabricated-metrics "is gone"
+metrics '{}'
+expect "an empty object fails check 9" FAIL 09-no-fabricated-metrics "no run provenance"
+metrics '{"MRR":0.85,"nDCG":0.85,"training_data_size":10012,"timestamp":"2026-04-25T15:26:45.717Z"}'
+expect "nudged fabricated metrics fail check 9" FAIL 09-no-fabricated-metrics "fabricated"
+metrics '{"MRR":0.41,"nDCG":0.52,"provenance":{"commit":"0123456789abcdef0123456789abcdef01234567","run_id":"run-7"}}'
+expect "metrics with run provenance pass check 9" PASS 09-no-fabricated-metrics "run-7"
+
+# ------------------------------------------------ check 10a: rulings ledger
+
+ids="D-A D-B D-C D-D D-E D-F D-G D-H D-I D-J D-K D-L D-M D-N D2 D3 D5 D6 D7"
+ledger() { mkdir -p "$R/docs/decisions"; printf '%s\n' "$1" > "$R/docs/decisions/ADR-020-rulings-ledger.adoc"; gate 10; }
+new_repo
+ledger "$(printf '= Rulings\n\n== %s\n:status: open\n' "$ids")"
+expect "one heading naming every ruling fails 10a" FAIL 10a-rulings-ledger "names more than one ruling"
+ledger "$(printf '= Rulings %s\n:status: ruled\nhttps://example.invalid\n' "$ids")"
+expect "the document title does not count as sections" FAIL 10a-rulings-ledger "no section of its own"
+good_ledger=$(printf '= Rulings\n'; for r in $ids; do printf '\n== %s\n:status: open\n' "$r"; done)
+ledger "$good_ledger"
+expect "one open section per ruling passes 10a" PASS 10a-rulings-ledger
+ledger "${good_ledger/:status: open/:status: ruled
+https://example.invalid/x}"
+expect "a ruled section with a foreign link fails 10a" FAIL 10a-rulings-ledger "D-A: ruled without a link"
+ledger "${good_ledger/:status: open/:status: ruled
+https://github.com/hyperpolymath/echidna/issues/1#issuecomment-1}"
+expect "a ruled section with the owner's record passes 10a" PASS 10a-rulings-ledger
+ledger "${good_ledger/:status: open/:status: open
+:status: ruled}"
+expect "two status lines in one section fail 10a" FAIL 10a-rulings-ledger "D-A: 2 :status: lines"
+commented_ledger=$(printf '= Rulings\n\n////\n== D-A\n:status: open\n////\n'; for r in ${ids#D-A }; do printf '\n== %s\n:status: open\n' "$r"; done)
+ledger "$commented_ledger"
+expect "a section inside a //// comment block does not count for 10a" FAIL 10a-rulings-ledger "D-A: no section of its own"
+ledger "${good_ledger/:status: open/:status: open
+
+----
+:status: ruled
+== D-A
+----
+
+....
+:status: ruled
+....}"
+expect "status lines and headings in listing blocks do not count for 10a" PASS 10a-rulings-ledger
+
+# ------------------------------------------------- check 13: Lean claims
+
+claims() { mkdir -p "$R/docs/proofs"; jq -cS . <<<"$1" > "$R/docs/proofs/claims.json"; gate 13; }
+new_repo
+claims '{"claims":[{"name":"nix flake check","note":"lean 4.13.0","status":"pass"}]}'
+expect "'flake' is not a lake build" FAIL 13-lean-build-recorded
+claims '{"claims":[{"claim":"lake build","toolchain":"14.13.01","status":"pass"}]}'
+expect "14.13.01 is not version 4.13.0" FAIL 13-lean-build-recorded
+claims '{"claims":[{"claim":"lake build","toolchain":"4.13.0","issue":"x"}]}'
+expect "a bare issue string is not a scheduled repair" FAIL 13-lean-build-recorded
+claims '{"claims":[{"claim":"lake build","toolchain":"4.13.0","repair":{"id":"R-1"}}]}'
+expect "a repair item with no place in the schedule fails 13" FAIL 13-lean-build-recorded
+claims '{"claims":[{"claim":"lake build","toolchain":"4.13.0","repair":{"id":"R-1","before":"F-3"}}]}'
+expect "a repair item before F-3 passes 13" PASS 13-lean-build-recorded
+claims '{"claims":[{"claim":"Lean 4 lake build of verification/proofs/lean4","toolchain":"leanprover/lean4:v4.13.0","result":"green"}]}'
+expect "a green lake build passes 13" PASS 13-lean-build-recorded
+claims '[{"claim":"Lean 4 lake build","toolchain":"4.13.0","result":"green"}]'
+expect "a claims.json whose root is an array fails 13" FAIL 13-lean-build-recorded "not a JSON object at its root"
+
+# ----------------------------------------------- check 7: Idris/Agda hygiene
+
+new_repo
+mkdir -p "$R/.github/workflows" "$R/src/abi/EchidnaABI" "$R/meta-checker/src/Echidna" "$R/scripts/ci"
+printf '# for pattern in postulate; do grep\nrun: echo\n' > "$R/.github/workflows/idris2-abi-ci.yml"
+printf 'package x\nmodules = EchidnaABI.CapnSchemas, CoprocessorForeign\n' > "$R/src/abi/echidnaabi.ipkg"
+touch "$R/src/abi/EchidnaABI/CapnSchemas.idr" "$R/src/abi/CoprocessorForeign.idr"
+printf 'module Echidna.MetaChecker where\n{- import Echidna.AxiomTrackerCompleteness -}\n' > "$R/meta-checker/src/Echidna/MetaChecker.agda"
+printf 'run: bash scripts/ci/check-agda.sh\n' > "$R/.github/workflows/agda-meta-checker.yml"
+printf 'agda --safe src/Echidna/MetaChecker.agda\n' > "$R/scripts/ci/check-agda.sh"
+gate 7
+expect "a postulate grep inside a comment fails 07a" FAIL 07a-idris-postulate-grep
+expect "the one-line modules layout passes 07b" PASS 07b-ipkg-coverage
+expect "an import inside a block comment fails 07c" FAIL 07c-meta-checker-completeness
+printf 'run: |\n  for pattern in believe_me postulate; do grep -rn "$pattern" src/abi; done\n' > "$R/.github/workflows/idris2-abi-ci.yml"
+printf 'package x\nmodules = Main\n     , EchidnaABI.CapnSchemas\ndepends = base\n     , CoprocessorForeign\n' > "$R/src/abi/echidnaabi.ipkg"
+printf 'module Echidna.MetaChecker where\nopen import Echidna.AxiomTrackerCompleteness public\n' > "$R/meta-checker/src/Echidna/MetaChecker.agda"
+gate 7
+expect "a real postulate grep passes 07a" PASS 07a-idris-postulate-grep
+expect "a module listed under depends does not count for 07b" FAIL 07b-ipkg-coverage "CoprocessorForeign"
+expect "a real import checked through check-agda.sh passes 07c" PASS 07c-meta-checker-completeness
+
+# Inline `#` comments: a mention after code on the line does not count.
+printf 'run: echo ok # grep -rn postulate src/abi\n' > "$R/.github/workflows/idris2-abi-ci.yml"
+printf 'module Echidna.MetaChecker where\n' > "$R/meta-checker/src/Echidna/MetaChecker.agda"
+printf 'run: echo ok # agda src/Echidna/AxiomTrackerCompleteness.agda\n' > "$R/.github/workflows/agda-meta-checker.yml"
+gate 7
+expect "a postulate grep in an inline comment fails 07a" FAIL 07a-idris-postulate-grep
+expect "an agda call in an inline comment fails 07c" FAIL 07c-meta-checker-completeness
+printf 'run: grep -rnE "believe_me #|postulate" src/abi\n' > "$R/.github/workflows/idris2-abi-ci.yml"
+printf "run: echo don't # agda src/Echidna/AxiomTrackerCompleteness.agda\n" > "$R/.github/workflows/agda-meta-checker.yml"
+gate 7
+expect "a # inside quotes does not cut the line for 07a" PASS 07a-idris-postulate-grep
+expect "an apostrophe does not hide an inline comment from 07c" FAIL 07c-meta-checker-completeness
+printf 'run: agda --safe src/Echidna/AxiomTrackerCompleteness.agda # completeness\n' > "$R/.github/workflows/agda-meta-checker.yml"
+gate 7
+expect "an agda call before an inline comment passes 07c" PASS 07c-meta-checker-completeness
+
+# ---------------------------------------------------- subset runs and config
+
+new_repo
+gate 9
+cases=$((cases + 1))
+if grep -qE '^FAIL +w0-subset' <<<"$OUT" && grep -q '^W0 config: ' <<<"$OUT" && [ "$RC" -ne 0 ]; then
+  echo "ok   a subset run records w0-subset as FAIL and prints its configuration"
+else
+  failures=$((failures + 1)); echo "FAIL a subset run records w0-subset as FAIL and prints its configuration"
+  sed 's/^/     | /' <<<"$OUT"
+fi
+
+echo "w0.selftest: $cases cases, $failures failed"
+[ "$failures" -eq 0 ]
diff --git a/scripts/gates/w0.sh b/scripts/gates/w0.sh
new file mode 100755
index 00000000..b922d5fc
--- /dev/null
+++ b/scripts/gates/w0.sh
@@ -0,0 +1,651 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+#
+# W0 exit gate (ultraplan, section "W0: unjam the gates ...", checks 1-13).
+# Every check is PASS, FAIL or DEFERRED(reason) under scripts/gates/lib.sh.
+# Exit 0 iff no check FAILs. Run from anywhere inside the repository.
+#
+# Checks whose artefact arrives from another W0 lane FAIL until that lane
+# lands. That is the point of the gate: do not soften a check to get green.
+#
+# Environment:
+#   GITHUB_TOKEN          optional read token for the GitHub API. The
+#                         repositories read here are public, so without it
+#                         the API is read anonymously (60 requests per hour);
+#                         a rate-limited or unreadable API is a FAIL.
+#   W0_PROBE_PR           number of the no-op probe PR (check 1). Required.
+#   W0_REPO               default hyperpolymath/echidna
+#   W0_BASE               last main commit before W0 (check 2). Default
+#                         6dbfea5 (main before #460, the CI-2 merge).
+#   W0_HEAD               ref whose first-parent W0 merges are checked
+#                         (check 2). Default HEAD.
+#   W0_HOTSPOT_GOLDENS    golden directory for check 5, default
+#                         tests/golden/hotspot (see hotspot-goldens.sh).
+#   W0_CONSUMER_OWNER     owner of the consumer repositories, default
+#                         hyperpolymath.
+#   W0_CHECKS             space-separated check numbers to run instead of all
+#                         thirteen. A subset run always exits non-zero: it is
+#                         a diagnostic, never a gate result.
+#   GATE_REPORT           also write the results as JCS JSON Lines (lib.sh).
+#
+# The effective configuration is printed first, so a result always shows
+# what it was computed over.
+#
+# Check 2 counts a check run as green when its conclusion is success,
+# skipped or neutral. The ultraplan says "at success"; every merge on main
+# carries schedule-only and matrix jobs that GitHub records as skipped, so a
+# literal reading could never pass. The PASS detail counts the skipped and
+# neutral runs so the reading stays visible.
+#
+# Contracts this gate reads from other lanes' artefacts. A lane that chooses
+# another shape changes this script in the same PR.
+#
+#   Consumer conformance jobs (checks 11, 12): a check run on the default
+#   branch's head whose name is exactly the job name below, or ends in
+#   " / <name>" (a reusable-workflow prefix):
+#     echidnabot, proof-burrower, panic-attack   prove-result-conformance
+#     verisimdb                                  verisim-api-list
+#     proof-burrower (check 12)                  agda-proofs
+#   A consumer check counts as DEFERRED(no-push:<repo>) only when the job is
+#   not green AND docs/handover/cross-repo/<repo>/ is committed (tracked,
+#   no uncommitted changes) with three non-empty files: a patch (*.patch or
+#   *.diff; for check 12 its name contains "agda"), the issue text (a file
+#   whose name contains "issue"), and PUSH-REFUSED.txt holding the output of
+#   the refused push.
+#   tests/fixtures/XFAIL.json
+#     One JCS value: an array of entries, or an object with "entries". Each
+#     entry names its backend in "backend" (or "prover"), matching
+#     ^[a-z0-9_]+$.
+#   models/training_metrics.json (check 9)
+#     Absent, or a JSON object whose "provenance" object carries "commit"
+#     (40 lower-case hex digits) and "run_id" (a non-empty string), and which
+#     does not repeat the fabricated values.
+#   docs/decisions/ADR-*-rulings-ledger.adoc (check 10)
+#     One section per ruling (D-A, ..., D-N, D2, D3, D5, D6, D7) whose
+#     heading (== or deeper) names exactly one ruling id, with exactly one
+#     attribute line `:status: open` or `:status: ruled`, all outside
+#     comment and verbatim blocks (////, ----, ...., ++++, ```). A ruled
+#     section links the owner's record on https://github.com/hyperpolymath/.
+#   scripts/ci/ruling-cited.sh (check 10b)
+#     Called as `ruling-cited.sh <W0_BASE> <W0_HEAD>`; exits 0 iff every W0
+#     PR in that range cites the rulings it acts on.
+#   docs/proofs/claims.json (check 13)
+#     One JCS value whose root is an object (a root array FAILs), holding
+#     an object whose id, name or claim names the Lean build ("lake build",
+#     "lean build", "lean4 build"), which mentions the version 4.13.0 as a
+#     whole token, and which carries either a green result
+#     (result/status/outcome: green, pass, passed, success) or a "repair"
+#     object with a non-empty "id" and "before": "F-3".
+
+# The checks are called through "check_$c", which shellcheck cannot follow.
+# shellcheck disable=SC2317
+set -uo pipefail
+export LC_ALL=C
+
+here=$(cd "$(dirname "$0")" && pwd)
+# shellcheck source=scripts/gates/lib.sh
+. "$here/lib.sh"
+root=$(git -C "$here" rev-parse --show-toplevel) || { echo "not inside a git checkout" >&2; exit 2; }
+cd "$root" || exit 2
+
+REPO="${W0_REPO:-hyperpolymath/echidna}"
+OWNER="${W0_CONSUMER_OWNER:-hyperpolymath}"
+W0_BASE="${W0_BASE:-6dbfea562beee3c46d754e380dec3dbef95bff24}"
+W0_HEAD="${W0_HEAD:-HEAD}"
+GOLDENS="${W0_HOTSPOT_GOLDENS:-tests/golden/hotspot}"
+
+# ---------------------------------------------------------------- helpers
+
+# gh_get <api path>: GET from the GitHub REST API, body on stdout. The
+# Authorization header is sent only when a token is present. Every request
+# is bounded (connect 10 s, transfer 60 s, retries 120 s in all), so a
+# stalled API is a FAIL, not a gate that never ends.
+gh_get() {
+  local auth=()
+  [ -n "${GITHUB_TOKEN:-}" ] && auth=(-H "Authorization: Bearer $GITHUB_TOKEN")
+  curl -fsS --connect-timeout 10 --max-time 60 --retry 2 --retry-max-time 120 \
+    ${auth[@]+"${auth[@]}"} \
+    -H "Accept: application/vnd.github+json" \
+    -H "X-GitHub-Api-Version: 2022-11-28" \
+    "https://api.github.com/$1"
+}
+
+# gh_pages <out file> <api path> <jq path to the page's array>: GET every
+# page (per_page=100) of a paginated endpoint and write the bodies to the
+# file, one per line. Returns non-zero when any page cannot be read, when a
+# page's items are not an array, or when there are more pages than it will
+# follow: a partial list must never read as a full one. Pages go to a file,
+# not through argv, because a commit with many runs produces arrays larger
+# than the argument limit.
+gh_pages() {
+  local out="$1" path="$2" items="$3" page=1 body n
+  : > "$out" || return 1
+  while :; do
+    if ! body=$(gh_get "$path?per_page=100&page=$page") \
+       || ! n=$(jq -e "$items | if type == \"array\" then length else error(\"not an array\") end" <<<"$body" 2>/dev/null); then
+      return 1
+    fi
+    printf '%s\n' "$body" >> "$out"
+    [ "$n" -lt 100 ] && return 0
+    page=$((page + 1))
+    [ "$page" -gt 20 ] && return 1
+  done
+}
+
+# check_runs <repo> <sha>: every check run on the commit, latest per name
+# and app, as a JSON array of {name, status, conclusion, app_id}. Returns
+# non-zero, with no output, when the runs cannot be read in full.
+check_runs() {
+  local repo="$1" sha="$2" tmp out
+  tmp=$(mktemp) || return 1
+  if ! gh_pages "$tmp" "repos/$repo/commits/$sha/check-runs" '.check_runs' \
+     || ! out=$(jq -cs 'map(.check_runs) | add // []
+                        | map(. + {app_id: (.app.id // null)})
+                        | group_by([.name, .app_id])
+                        | map(max_by(.id) | {name, status, conclusion, app_id})' "$tmp") \
+     || [ -z "$out" ] || ! jq -e 'type == "array"' <<<"$out" >/dev/null 2>&1; then
+    rm -f "$tmp"; return 1
+  fi
+  rm -f "$tmp"
+  printf '%s\n' "$out"
+}
+
+# commit_statuses <repo> <sha>: the combined legacy commit status with the
+# statuses of every page, as {state, total_count, statuses}. Returns
+# non-zero, with no output, when any page cannot be read or the pages do not
+# add up to total_count.
+commit_statuses() {
+  local repo="$1" sha="$2" tmp out
+  tmp=$(mktemp) || return 1
+  if ! gh_pages "$tmp" "repos/$repo/commits/$sha/status" '.statuses' \
+     || ! out=$(jq -cs '{state: .[0].state, total_count: .[0].total_count, statuses: (map(.statuses) | add // [])}
+                        | if (.state | type) == "string" and (.total_count | type) == "number"
+                             and (.statuses | length) == .total_count
+                          then . else error("incomplete combined status") end' "$tmp" 2>/dev/null) \
+     || [ -z "$out" ]; then
+    rm -f "$tmp"; return 1
+  fi
+  rm -f "$tmp"
+  printf '%s\n' "$out"
+}
+
+# is_jcs <file>: one JSON value, serialised as JCS, one final LF.
+# (jq -cS matches JCS for the strings, integers and plain decimals these
+# ledgers hold; it is not a general JCS number serialiser.)
+is_jcs() {
+  local f="$1"
+  [ "$(jq -s 'length' "$f" 2>/dev/null)" = 1 ] || return 1
+  cmp -s <(jq -cS . "$f") "$f"
+}
+
+# strip_hash_comments <file>: the file without shell/YAML `#` comments,
+# whole-line and inline. A `#` starts a comment at the start of a line or
+# after whitespace, outside single and double quotes. A quote opens only
+# where it does not follow a letter or digit, so the apostrophe in "don't"
+# does not hide a comment after it. Quote state does not span lines.
+strip_hash_comments() {
+  awk '
+    { line = $0; out = ""; q = ""; prev = ""
+      for (i = 1; i <= length(line); i++) {
+        c = substr(line, i, 1)
+        if (q == "\"" && c == "\\") { out = out c substr(line, i + 1, 1); prev = substr(line, i + 1, 1); i++; continue }
+        if (q != "") { if (c == q) q = ""; out = out c; prev = c; continue }
+        if (c == "#" && (prev == "" || prev ~ /[[:space:]]/)) break
+        if ((c == "\"" || c == "'\''") && prev !~ /[[:alnum:]]/) q = c
+        out = out c; prev = c
+      }
+      print out }' "$1"
+}
+
+# strip_agda_comments <file>: the file without `--` line comments and
+# (nested) `{- ... -}` block comments.
+strip_agda_comments() {
+  awk '
+    { line = $0; out = ""; i = 1
+      while (i <= length(line)) {
+        two = substr(line, i, 2)
+        if (depth == 0 && two == "--") break
+        if (two == "{-") { depth++; i += 2; continue }
+        if (depth > 0 && two == "-}") { depth--; i += 2; continue }
+        if (depth == 0) out = out substr(line, i, 1)
+        i++
+      }
+      print out }' "$1"
+}
+
+handover_dir() { printf 'docs/handover/cross-repo/%s' "$1"; }
+
+# handover_ok <repo> [patch-name-substring]: the committed handover the
+# contract above describes.
+handover_ok() {
+  local d sub="${2:-}" f base patch="" issue="" refused=""
+  d=$(handover_dir "$1")
+  [ -d "$d" ] || return 1
+  git diff --quiet HEAD -- "$d" 2>/dev/null || return 1
+  [ -z "$(git ls-files --others --exclude-standard -- "$d")" ] || return 1
+  while IFS= read -r -d '' f; do
+    [ -s "$f" ] || continue
+    base="${f##*/}"
+    case "$base" in
+      PUSH-REFUSED.txt) refused=1 ;;
+      *.patch|*.diff) [[ ${base,,} == *"${sub,,}"* ]] && patch=1 ;;
+    esac
+    [[ ${base,,} == *issue* ]] && issue=1
+  done < <(git ls-files -z -- "$d")
+  [ -n "$patch" ] && [ -n "$issue" ] && [ -n "$refused" ]
+}
+
+# --------------------------------------------- (1) probe PR required contexts
+
+check_1() {
+  local id="01-probe-pr-required-contexts" tmp rules req sha runs statuses missing r ctx ok
+  # Every page of rules: a required_status_checks rule on page 2 still gates.
+  tmp=$(mktemp) || { fail "$id" "cannot create a temporary file"; return; }
+  if ! gh_pages "$tmp" "repos/$REPO/rules/branches/main" '.' || ! rules=$(jq -cs 'add // []' "$tmp"); then
+    rm -f "$tmp"; fail "$id" "cannot read the live ruleset for $REPO main"; return
+  fi
+  rm -f "$tmp"
+  # One {context, integration_id} per line; integration_id is null when the
+  # context is not pinned to an app.
+  if ! req=$(jq -ec '[.[] | select(.type == "required_status_checks") | .parameters.required_status_checks[]
+                      | {context, integration_id: (.integration_id // null)}] | unique | .[]' <<<"$rules"); then
+    fail "$id" "the live ruleset requires no status context; nothing would gate a merge"; return
+  fi
+  if ! [[ ${W0_PROBE_PR:-} =~ ^[0-9]+$ ]]; then
+    fail "$id" "W0_PROBE_PR is not set to the no-op probe PR number ($(wc -l <<<"$req") required contexts to check)"; return
+  fi
+  if ! sha=$(gh_get "repos/$REPO/pulls/$W0_PROBE_PR" | jq -er '.head.sha'); then
+    fail "$id" "cannot read probe PR #$W0_PROBE_PR"; return
+  fi
+  if ! runs=$(check_runs "$REPO" "$sha") || ! statuses=$(commit_statuses "$REPO" "$sha"); then
+    fail "$id" "cannot read check runs for probe PR #$W0_PROBE_PR ($sha)"; return
+  fi
+  missing=()
+  while IFS= read -r r; do
+    # A context pinned to an app (integration_id) is satisfied only by a
+    # check run from that app; a legacy status cannot satisfy it. Not jq -e:
+    # a context that is not green evaluates to false, which is an answer,
+    # not an error.
+    ok=$(jq -r --argjson r "$r" --slurpfile s <(printf '%s\n' "$statuses") '
+        ([.[] | select(.name == $r.context and .conclusion == "success"
+                       and ($r.integration_id == null or .app_id == $r.integration_id))] | length > 0)
+        or ($r.integration_id == null
+            and ([$s[0].statuses[] | select(.context == $r.context and .state == "success")] | length > 0))' <<<"$runs")
+    ctx=$(jq -r '.context + (if .integration_id == null then "" else " (app \(.integration_id))" end)' <<<"$r")
+    case "$ok" in
+      true|false) ;;
+      *) fail "$id" "cannot evaluate required context '$ctx'"; return ;;
+    esac
+    [ "$ok" = true ] || missing+=("$ctx")
+  done <<<"$req"
+  if [ ${#missing[@]} -eq 0 ]; then
+    pass "$id" "probe PR #$W0_PROBE_PR (${sha:0:9}): all $(wc -l <<<"$req") required contexts are success"
+  else
+    fail "$id" "probe PR #$W0_PROBE_PR: not success: $(printf '%s; ' "${missing[@]}")"
+  fi
+}
+
+# --------------------------------------- (2) every W0 merge commit is green
+
+check_2() {
+  local id="02-w0-merges-green" commits c runs bad statuses st nr ns soft=0 n=0 problems=()
+  if ! commits=$(git rev-list --first-parent "$W0_BASE..$W0_HEAD" 2>/dev/null); then
+    fail "$id" "cannot list commits $W0_BASE..$W0_HEAD (fetch history?)"; return
+  fi
+  if [ -z "$commits" ]; then
+    fail "$id" "no W0 merge commits in $W0_BASE..$W0_HEAD"; return
+  fi
+  for c in $commits; do
+    n=$((n + 1))
+    # Legacy statuses: every page is read, and GitHub's combined state must
+    # also be success whenever any status exists. The combined state is
+    # computed over every context, so even a page this script failed to
+    # read cannot hide a red status; the pages only name which one.
+    if ! runs=$(check_runs "$REPO" "$c") || ! statuses=$(commit_statuses "$REPO" "$c") \
+       || ! nr=$(jq -e 'length' <<<"$runs") || ! ns=$(jq -e '.total_count' <<<"$statuses"); then
+      problems+=("${c:0:9} unreadable"); continue
+    fi
+    if [ "$nr" -eq 0 ] && [ "$ns" -eq 0 ]; then
+      problems+=("${c:0:9} has no check runs"); continue
+    fi
+    if ! bad=$(jq -er '[.[] | select((.conclusion // "pending") as $k | ["success","skipped","neutral"] | index($k) | not) | "\(.name)=\(.conclusion // .status)"] | join(", ")' <<<"$runs") \
+       || ! st=$(jq -er '[.statuses[] | select(.state != "success") | "\(.context)=\(.state)"]
+                         + (if .total_count > 0 and .state != "success" then ["combined status=\(.state)"] else [] end)
+                         | join(", ")' <<<"$statuses"); then
+      problems+=("${c:0:9} unparseable"); continue
+    fi
+    soft=$((soft + $(jq '[.[] | select(.conclusion == "skipped" or .conclusion == "neutral")] | length' <<<"$runs")))
+    [ -n "$bad$st" ] && problems+=("${c:0:9}: ${bad}${bad:+${st:+, }}${st}")
+  done
+  if [ ${#problems[@]} -eq 0 ]; then
+    pass "$id" "$n first-parent commits in ${W0_BASE:0:9}..$W0_HEAD, every check run success ($soft skipped or neutral; the bypass log stays an owner checkpoint)"
+  else
+    fail "$id" "$(printf '%s; ' "${problems[@]}")"
+  fi
+}
+
+# ------------------------------------------------------- (3) cargo audit
+
+check_3() {
+  local id="03-cargo-audit"
+  if ! cargo audit --version >/dev/null 2>&1; then
+    fail "$id" "cargo-audit is not installed (cargo install cargo-audit --locked)"; return
+  fi
+  gate_cmd "$id" "cargo audit" -- cargo audit
+}
+
+# ---------------------------------------------- (4) the W0 safety-net tests
+
+check_4() {
+  local id="04-w0-net-tests" t missing=()
+  for t in arbiter_props trust_kernel_characterisation prove_output_json; do
+    [ -f "tests/$t.rs" ] || missing+=("tests/$t.rs")
+  done
+  if [ ${#missing[@]} -gt 0 ]; then
+    fail "$id" "missing: ${missing[*]}"; return
+  fi
+  gate_cmd "$id" "cargo test --locked (arbiter_props, trust_kernel_characterisation, prove_output_json)" -- \
+    cargo test --locked --test arbiter_props --test trust_kernel_characterisation --test prove_output_json
+}
+
+# --------------------------------------------- (5) hotspot-split goldens
+
+check_5() {
+  local id="05-hotspot-goldens"
+  if [ ! -d "$GOLDENS" ]; then
+    fail "$id" "$GOLDENS is missing; capture it on the pre-split tree with scripts/gates/hotspot-goldens.sh capture"; return
+  fi
+  gate_cmd "$id" "help, route table and just --list match $GOLDENS" -- \
+    "$here/hotspot-goldens.sh" check --dir "$GOLDENS"
+}
+
+# ---------------------------------------- (6) live fixtures + XFAIL ledger
+
+# Backends V-3 is scoped to (P1, P2 and P3 lanes of W1a), whose vacuous
+# Ok(true) or IR fallback may stand in the ledger until V-3 empties it.
+XFAIL_ALLOWED="acl2 agda coq cvc5 hol4 hol_light idris2 isabelle lean metamath pvs rocq z3"
+
+check_6() {
+  local idx="06a-xfail-ledger" idl="06b-live-fixtures" f="tests/fixtures/XFAIL.json" backends b n=0 bad=()
+  if [ ! -f "$f" ]; then
+    fail "$idx" "$f is missing"
+  elif ! is_jcs "$f"; then
+    fail "$idx" "$f is not one JCS value with a final LF"
+  elif ! backends=$(jq -r 'if type == "array" then . elif type == "object" and (.entries | type) == "array" then .entries else error("neither an array nor an object with an entries array") end
+        | map(if type == "object" and ((.backend // .prover) | type) == "string" and ((.backend // .prover) | test("^[a-z0-9_]+$"))
+              then (.backend // .prover)
+              else error("an entry does not name its backend as ^[a-z0-9_]+$: \(tojson)") end)
+        | .[]' "$f" 2>&1); then
+    fail "$idx" "$f has an unrecognised shape: $backends"
+  else
+    while IFS= read -r b; do
+      [ -n "$b" ] || continue
+      n=$((n + 1))
+      [[ " $XFAIL_ALLOWED " == *" $b "* ]] || bad+=("$b")
+    done <<<"$backends"
+    if [ ${#bad[@]} -gt 0 ]; then
+      fail "$idx" "$f lists backends outside V-3 scope: ${bad[*]}"
+    elif [ "$n" -eq 0 ]; then
+      pass "$idx" "$f is JCS and empty"
+    else
+      pass "$idx" "$f is JCS and lists only V-3 backends/IR fallbacks ($n entries)"
+    fi
+  fi
+
+  if [ ! -x scripts/ci/live-fixtures.sh ]; then
+    fail "$idl" "scripts/ci/live-fixtures.sh is missing or not executable"; return
+  fi
+  gate_cmd "$idl" "ECHIDNA_FAIL_ON_SKIP=1 scripts/ci/live-fixtures.sh" -- \
+    env ECHIDNA_FAIL_ON_SKIP=1 scripts/ci/live-fixtures.sh
+}
+
+# ------------------------------------------------ (7) Idris / Agda hygiene
+
+# ipkg_modules <ipkg>: the module names listed under `modules`, one per line,
+# for both the one-line and the leading-comma layouts.
+ipkg_modules() {
+  sed -E 's/--.*$//' "$1" | awk '
+    /^[[:space:]]*[a-z][a-z0-9_]*[[:space:]]*=/ { on = ($1 == "modules" || $0 ~ /^[[:space:]]*modules[[:space:]]*=/); sub(/^[^=]*=/, "") }
+    on { gsub(/,/, " "); for (i = 1; i <= NF; i++) print $i }'
+}
+
+check_7() {
+  local wf=.github/workflows/idris2-abi-ci.yml ipkg=src/abi/echidnaabi.ipkg rel mod mods missing=()
+  if [ -f "$wf" ] && strip_hash_comments "$wf" | grep -E '\bpostulate\b' | grep -qE 'grep|rg |for pattern in'; then
+    pass "07a-idris-postulate-grep" "$wf greps src/abi for postulate"
+  else
+    fail "07a-idris-postulate-grep" "$wf does not grep for postulate outside comments"
+  fi
+
+  if [ ! -f "$ipkg" ]; then
+    fail "07b-ipkg-coverage" "$ipkg is missing"
+  else
+    mods=$(ipkg_modules "$ipkg")
+    for rel in EchidnaABI/CapnSchemas.idr CoprocessorForeign.idr; do
+      [ -f "src/abi/$rel" ] || continue
+      mod=$(sed 's/\.idr$//; s#/#.#g' <<<"$rel")
+      grep -qxF "$mod" <<<"$mods" || missing+=("$mod")
+    done
+    if [ ${#missing[@]} -eq 0 ]; then
+      pass "07b-ipkg-coverage" "CapnSchemas and CoprocessorForeign are in $ipkg or deleted"
+    else
+      fail "07b-ipkg-coverage" "present but not in $ipkg: ${missing[*]}"
+    fi
+  fi
+
+  local mc=meta-checker/src/Echidna/MetaChecker.agda awf=.github/workflows/agda-meta-checker.yml
+  if [ -f "$awf" ] && strip_hash_comments "$awf" | grep -qE 'agda .*AxiomTrackerCompleteness\.agda'; then
+    pass "07c-meta-checker-completeness" "$awf type-checks AxiomTrackerCompleteness.agda directly"
+  elif [ -f "$mc" ] && strip_agda_comments "$mc" | grep -qE '^[[:space:]]*(open[[:space:]]+)?import[[:space:]]+Echidna\.AxiomTrackerCompleteness([[:space:]]|$)' \
+       && [ -f "$awf" ] && { strip_hash_comments "$awf" | grep -qE 'agda .*MetaChecker\.agda' \
+            || { strip_hash_comments "$awf" | grep -qE 'scripts/ci/check-agda\.sh' \
+                 && [ -f scripts/ci/check-agda.sh ] && strip_hash_comments scripts/ci/check-agda.sh | grep -qE 'MetaChecker\.agda'; }; }; then
+    pass "07c-meta-checker-completeness" "MetaChecker.agda imports Echidna.AxiomTrackerCompleteness and $awf checks MetaChecker.agda"
+  else
+    fail "07c-meta-checker-completeness" "AxiomTrackerCompleteness is not type-checked by the meta-checker job"
+  fi
+}
+
+# ------------------------------------------- (8) allow-fail expiry, Dec 1st
+
+check_8() {
+  # R0 is ruled (owner, 2026-11-05: each unit blocking or deleted), so the
+  # slip rule's DEFERRED(ruling:R0) does not apply.
+  gate_cmd "08-allow-fail-expiry" "check-allow-fail-expiry.sh as of 2026-12-01" -- \
+    scripts/ci/check-allow-fail-expiry.sh --today 2026-12-01
+}
+
+# ------------------------------------- (9) fabricated training metrics gone
+
+check_9() {
+  local id="09-no-fabricated-metrics" f=models/training_metrics.json
+  # The fabricated file (6e13847): MRR = nDCG = 0.85 over 10011 items,
+  # timestamp 2026-04-25T15:26:45.716Z, with no run behind it (L-4).
+  if [ ! -e "$f" ]; then
+    pass "$id" "$f is gone"
+  elif ! jq -e 'type == "object"' "$f" >/dev/null 2>&1; then
+    fail "$id" "$f is not a JSON object"
+  elif jq -e '(.MRR == 0.85 and .nDCG == 0.85) or ((.timestamp // "") | startswith("2026-04-25T15:26"))' "$f" >/dev/null 2>&1; then
+    fail "$id" "$f still holds the fabricated metrics"
+  elif jq -e '(.provenance | type) == "object"
+        and ((.provenance.commit // "") | test("^[0-9a-f]{40}$"))
+        and ((.provenance.run_id // "") | type == "string" and length > 0)' "$f" >/dev/null 2>&1; then
+    pass "$id" "$f carries run provenance ($(jq -r '.provenance.run_id + " at " + .provenance.commit[0:9]' "$f"))"
+  else
+    fail "$id" "$f has no run provenance (provenance.commit and provenance.run_id)"
+  fi
+}
+
+# ------------------------------------------------- (10) rulings ledger ADR
+
+RULING_IDS="D-A D-B D-C D-D D-E D-F D-G D-H D-I D-J D-K D-L D-M D-N D2 D3 D5 D6 D7"
+
+# adoc_strip_blocks <adoc>: the file with every line of a comment (////),
+# listing (----), literal (....), passthrough (++++) or fenced (```) block,
+# delimiters included, blanked. Line numbers are kept. A block closes only
+# on a line equal to its opening delimiter; an unclosed block runs to the
+# end of the file, so nothing after a stray delimiter can count.
+adoc_strip_blocks() {
+  awk '
+    delim != "" { if ($0 == delim) delim = ""; print ""; next }
+    /^(\/\/\/\/+|----+|\.\.\.\.+|\+\+\+\++)$/ || /^```/ { delim = ($0 ~ /^```/) ? "```" : $0; print ""; next }
+    { print }' "$1"
+}
+
+# ruling_sections <adr>: for every section heading (== or deeper), the line
+# "<heading line number> <ruling ids named in it>".
+ruling_sections() {
+  awk -v ids="$RULING_IDS" '
+    BEGIN { n = split(ids, id, " ") }
+    /^==+[[:space:]]/ {
+      named = ""
+      for (k = 1; k <= n; k++)
+        if (match($0, "(^|[^A-Za-z0-9-])" id[k] "([^A-Za-z0-9]|$)")) named = named " " id[k]
+      print NR named
+    }' "$1"
+}
+
+check_10() {
+  local id="10a-rulings-ledger" adrs adr r sections line from to block statuses status text problems=()
+  adrs=$(find docs/decisions -maxdepth 1 -name 'ADR-*-rulings-ledger.adoc' 2>/dev/null | sort)
+  if [ -z "$adrs" ]; then
+    fail "$id" "no docs/decisions/ADR-*-rulings-ledger.adoc"
+  elif [ "$(wc -l <<<"$adrs")" -ne 1 ]; then
+    fail "$id" "more than one rulings ledger: $(tr '\n' ' ' <<<"$adrs")"
+  else
+    adr="$adrs"
+    # Headings, :status: lines and links inside comment or verbatim blocks
+    # are not ledger content.
+    text=$(adoc_strip_blocks "$adr")
+    sections=$(ruling_sections <(printf '%s\n' "$text"))
+    while read -r line r rest; do
+      [ -n "${rest:-}" ] && problems+=("heading at line $line names more than one ruling ($r $rest)")
+    done <<<"$sections"
+    for r in $RULING_IDS; do
+      line=$(awk -v r="$r" 'NF == 2 && $2 == r { print $1 }' <<<"$sections")
+      if [ -z "$line" ]; then problems+=("$r: no section of its own"); continue; fi
+      if [ "$(wc -l <<<"$line")" -ne 1 ]; then problems+=("$r: more than one section"); continue; fi
+      from="$line"
+      to=$(awk -v f="$from" '$1 > f { print $1 - 1; exit }' <<<"$sections")
+      block=$(sed -n "${from},${to:-\$}p" <<<"$text")
+      statuses=$(grep -cE '^:status:' <<<"$block")
+      status=$(grep -E '^:status:' <<<"$block" | sed -E 's/^:status:[[:space:]]*//; s/[[:space:]]+$//')
+      if [ "$statuses" -ne 1 ]; then problems+=("$r: $statuses :status: lines"); continue; fi
+      case "$status" in
+        open) ;;
+        ruled) grep -qE 'https://github\.com/hyperpolymath/[^[:space:]]+' <<<"$block" \
+                 || problems+=("$r: ruled without a link to the owner's record on github.com/hyperpolymath") ;;
+        *) problems+=("$r: :status: $status") ;;
+      esac
+    done
+    if [ ${#problems[@]} -eq 0 ]; then
+      pass "$id" "$adr records all $(wc -w <<<"$RULING_IDS") rulings, one section each, as open or ruled-with-record"
+    else
+      fail "$id" "$adr: $(printf '%s; ' "${problems[@]}")"
+    fi
+  fi
+
+  if [ ! -x scripts/ci/ruling-cited.sh ]; then
+    fail "10b-ruling-cited" "scripts/ci/ruling-cited.sh is missing or not executable"; return
+  fi
+  gate_cmd "10b-ruling-cited" "scripts/ci/ruling-cited.sh ${W0_BASE:0:9} $W0_HEAD" -- \
+    scripts/ci/ruling-cited.sh "$W0_BASE" "$W0_HEAD"
+}
+
+# ------------------------------------- (11, 12) consumer repositories green
+
+# consumer_eval <repo> <job name>: sets C_GREEN (1 or empty) and C_DETAIL.
+consumer_eval() {
+  local repo="$1" job="$2" branch sha runs hits n bad
+  C_GREEN=""
+  if ! branch=$(gh_get "repos/$OWNER/$repo" | jq -er '.default_branch'); then
+    C_DETAIL="cannot read $OWNER/$repo"; return
+  fi
+  if ! sha=$(gh_get "repos/$OWNER/$repo/commits/$branch" | jq -er '.sha') || ! runs=$(check_runs "$OWNER/$repo" "$sha"); then
+    C_DETAIL="cannot read check runs on $OWNER/$repo $branch"; return
+  fi
+  if ! hits=$(jq -ec --arg j "$job" '[.[] | select(.name == $j or (.name | endswith(" / " + $j)))]' <<<"$runs") \
+     || ! n=$(jq -e 'length' <<<"$hits"); then
+    C_DETAIL="cannot parse check runs on $OWNER/$repo $branch"; return
+  fi
+  if [ "$n" -eq 0 ]; then
+    C_DETAIL="no check run named '$job' on $OWNER/$repo $branch (${sha:0:9})"; return
+  fi
+  bad=$(jq -r '[.[] | select(.conclusion != "success") | "\(.name)=\(.conclusion // .status)"] | join(", ")' <<<"$hits")
+  if [ -z "$bad" ]; then
+    C_GREEN=1
+    C_DETAIL="$OWNER/$repo $branch (${sha:0:9}): '$job' green ($(jq -r 'map(.name) | join(", ")' <<<"$hits"))"
+  else
+    C_DETAIL="$OWNER/$repo $branch (${sha:0:9}): $bad"
+  fi
+}
+
+# consumer_check <check id> <repo> <job name> [patch-name-substring]
+consumer_check() {
+  local id="$1" repo="$2" job="$3" sub="${4:-}"
+  consumer_eval "$repo" "$job"
+  if [ -n "$C_GREEN" ]; then
+    pass "$id" "$C_DETAIL"
+  elif handover_ok "$repo" "$sub"; then
+    deferred "$id" "no-push:$repo" "$C_DETAIL; handover committed under $(handover_dir "$repo")/"
+  else
+    fail "$id" "$C_DETAIL; no committed handover under $(handover_dir "$repo")/"
+  fi
+}
+
+check_11() {
+  local repo
+  for repo in echidnabot proof-burrower panic-attack; do
+    consumer_check "11-conformance-$repo" "$repo" prove-result-conformance
+  done
+  consumer_check "11-conformance-verisimdb" verisimdb verisim-api-list
+}
+
+check_12() {
+  consumer_check "12-proof-burrower-agda" proof-burrower agda-proofs agda
+}
+
+# --------------------------------------- (13) Lean build recorded in claims
+
+check_13() {
+  local id="13-lean-build-recorded" f=docs/proofs/claims.json hit
+  if [ ! -f "$f" ]; then
+    fail "$id" "$f is missing"; return
+  fi
+  if ! is_jcs "$f"; then
+    fail "$id" "$f is not one JCS value with a final LF"; return
+  fi
+  if ! jq -e 'type == "object"' "$f" >/dev/null 2>&1; then
+    fail "$id" "$f is not a JSON object at its root"; return
+  fi
+  if ! hit=$(jq -e '[.. | objects
+      | select(([.id, .name, .claim] | map(strings) | join(" ")) | test("\\blake[ _-]build\\b|\\blean4?[ _-]build\\b"; "i"))
+      | select(tojson | test("(^|[^0-9.])4\\.13\\.0([^0-9.]|$)"))
+      | select(([.result, .status, .outcome] | map(strings | ascii_downcase) | any(. == "green" or . == "pass" or . == "passed" or . == "success"))
+               or ((.repair | type) == "object" and ((.repair.id // "") | type == "string" and length > 0) and .repair.before == "F-3"))]
+      | length' "$f"); then
+    fail "$id" "$f cannot be evaluated"; return
+  fi
+  if [ "$hit" -gt 0 ]; then
+    pass "$id" "$f records the Lean 4.13.0 lake build as green or with a repair item before F-3"
+  else
+    fail "$id" "$f has no Lean 4.13.0 lake-build entry with a green result or a repair item before F-3"
+  fi
+}
+
+# ------------------------------------------------------------------- run
+
+printf 'W0 config: repo=%s base=%s head=%s goldens=%s consumers=%s api=%s probe_pr=%s\n' \
+  "$REPO" "$W0_BASE" "$W0_HEAD" "$GOLDENS" "$OWNER" \
+  "$([ -n "${GITHUB_TOKEN:-}" ] && echo token || echo anonymous)" "${W0_PROBE_PR:-unset}"
+
+gate_init W0
+if [ -n "${W0_CHECKS:-}" ]; then
+  for c in $W0_CHECKS; do
+    if declare -F "check_$c" >/dev/null; then "check_$c"; else fail "w0-checks" "no check $c"; fi
+  done
+  fail "w0-subset" "only checks $W0_CHECKS ran (W0_CHECKS); a subset run is not a gate result"
+else
+  for c in 1 2 3 4 5 6 7 8 9 10 11 12 13; do "check_$c"; done
+fi
+gate_finish