diff --git a/verification/HARNESS.sha256 b/verification/HARNESS.sha256
index 94335b8..adb1cf4 100644
--- a/verification/HARNESS.sha256
+++ b/verification/HARNESS.sha256
@@ -8,7 +8,7 @@ b9c907f94572c06a59135d29377d51ad8efc3f74402ac61e8644a15786d4b0ed  inventory-allo
 86ee83b703d17c1f04af654657219b344b0076bc994c0b791ca6b6c5a0090d4f  inventory-allowlist.txt
 3ebc8027f14c9e037f36322ef4119183c33214658efcc1a7bc985a98a9c32e4e  inventory_gate.sh
 736ea4be712e1b5bcda10ecb466f0dec7008a2a36eabdfd77563976299c43cce  lean-guard
-b982bd1aa56b0648b10516985a2e0f6a9cacff4e1d19b441dadc5b35d69ec732  lift-guard.sh
+2b78361105984aa8e859758849a0886b5b768766fe9bb39dd04aa8ee24d38b6c  lift-guard.sh
 1942177f13d6ae229d87a3b0b33f7fbb4b2ae20fe1059cc83010e73f6a156427  model-correspondence.py
 77e356f607c01ff597193f28f60b48a701ca2b9597cc9a991ac5b27b00aeaf81  MODEL-CORRESPONDENCE.txt
 772ca6dd22443c83dc35d5428598c8d17a01c69db5be008474d06476fa66f7f8  Proofs/Audit.lean
diff --git a/verification/lift-guard.sh b/verification/lift-guard.sh
index fa13632..0ef0a9c 100755
--- a/verification/lift-guard.sh
+++ b/verification/lift-guard.sh
@@ -1,7 +1,16 @@
 #!/usr/bin/env bash
 # lift-guard.sh <payload> <driver> [<phase-label>]
 #
-# Every variable the LIFTED PAYLOAD reads must be one the DRIVER defines.
+# Every VARIABLE the LIFTED PAYLOAD reads must be one the DRIVER defines.
+#
+# VARIABLES ONLY — and the emphasis is a round-8 correction (Claude, N1). A
+# lifted payload also inherits FUNCTIONS, shell options, traps and a working
+# directory from the script it was cut out of. This tool models none of those.
+# A lifted phase calling a function defined in a neighbouring phase fails with
+# `command not found`, loud under `set -e`, which is why it is not urgent; but
+# the banner used to read as a completeness claim about lifting and it is a
+# completeness claim about variables.
+#
 # Prints the offending names and exits 1 if any are missing.
 #
 # ───────────────────────────────────────────────────────────────────────────
@@ -42,12 +51,16 @@
 # grows a new dependency fails AT LIFT TIME, naming it, instead of dying
 # mid-run or — worse — passing for the wrong reason.
 #
-# WHAT IT IS NOT. This is a shell-text approximation, not a bash parser: it
-# cannot see indirect expansion, `eval`, or a name built at runtime. It is a
-# tripwire on the failure mode that actually occurred twice, not a proof of
-# closure. Its answer is advisory in one direction only — it can miss a
-# dependency, it does not invent one, and every name it reports is a name the
-# payload genuinely mentions and the driver genuinely does not set.
+# WHAT IT IS NOT. This is a shell-text approximation, not a bash parser. It
+# still cannot see a name built at runtime or passed through `eval`, and it
+# models variables only — not functions, shell options, traps or the working
+# directory a lifted phase also inherits. It is a tripwire on failure modes
+# that actually occurred, not a proof of closure.
+#
+# Where it CANNOT bound the reads it refuses rather than staying silent:
+# indirect expansion (`${!name}`) is detected and fails the lift. That is the
+# round-8 correction — a guard whose contract is "does not miss a dependency"
+# must say so when it cannot honour it, instead of shrugging.
 # ───────────────────────────────────────────────────────────────────────────
 set -euo pipefail
 
@@ -68,14 +81,33 @@ driver  = open(sys.argv[2]).read()
 # comment costs one lifted definition, a name missed costs a broken self-test.
 reads = set(re.findall(r'\$\{?([A-Za-z_][A-Za-z0-9_]*)', payload))
 
+# ARITHMETIC CONTEXTS READ NAMES WITHOUT A `$`. Round-8 review (Claude, N1):
+#   echo $((X + 1))      reads X
+#   (( Y > 0 )) && ...   reads Y
+# and the pattern above cannot see either, because the character after `$` is
+# `(`. This is the guard's own failure mode — a phase growing a dependency the
+# guard is blind to — and `if [ $((inm + ins)) -eq 0 ]` is already live in
+# check.sh's Phase 1b. Not lifted today, which made it latent, not absent.
+for expr in (re.findall(r'\$\(\((.*?)\)\)', payload, re.S)
+             + re.findall(r'(?<!\$)\(\((.*?)\)\)', payload, re.S)):
+    for tok in re.findall(r'[A-Za-z_][A-Za-z0-9_]*', expr):
+        reads.add(tok)
+
 # What the DRIVER defines, in every form these scripts actually use.
-# An assignment may open a line OR follow `;`, `&&`, `||`, `then`, `do`, `{` —
-# `TIMEOUT=$T; CORES="$C"` is one line with two of them, and a start-anchored
-# pattern sees only the first. That over-strictness is not harmless: a guard
-# that cries wolf gets edited away, and then it guards nothing.
+# `TIMEOUT=$T; CORES="$C"` is one line with two assignments, and a
+# start-anchored pattern sees only the first.
+# An assignment may open a line or follow `;`, `&&`, `||`, `then`, `do`, `{`,
+# and — round-8 review (Claude, N1) — `else`, a `case` branch's `)`, and `!`.
+# Six false-positive classes were demonstrated. A guard that cries wolf gets
+# edited away, so over-strictness here is not the safe direction.
 assigns  = set(re.findall(
-    r'(?:^|;|&&|\|\||\bthen\b|\bdo\b|\{)\s*([A-Za-z_][A-Za-z0-9_]*)=',
-    driver, re.M))
+    r'(?:^|;|&&|\|\||\)|!|\bthen\b|\bdo\b|\belse\b|\{)\s*'
+    r'([A-Za-z_][A-Za-z0-9_]*)=', driver, re.M))
+# `mapfile`/`readarray` and `printf -v` bind a name without an `=` at all.
+assigns |= set(re.findall(
+    r'\b(?:mapfile|readarray)\b(?:\s+-[A-Za-z]\s*\S*)*\s+([A-Za-z_][A-Za-z0-9_]*)',
+    driver))
+assigns |= set(re.findall(r'\bprintf\b[^\n]*?\s-v\s+([A-Za-z_][A-Za-z0-9_]*)', driver))
 assigns |= set(re.findall(r'\b(?:export|declare|local|readonly)\s+(?:-\w+\s+)*'
                           r'([A-Za-z_][A-Za-z0-9_]*)', driver))
 assigns |= set(re.findall(r'\bfor\s+([A-Za-z_][A-Za-z0-9_]*)\s+in\b', driver))
@@ -95,10 +127,27 @@ ENV = {'PWD', 'HOME', 'PATH', 'IFS', 'PIPESTATUS', 'BASH_SOURCE', 'FUNCNAME',
        'AENEAS_HOME', 'LEAN_PATH', 'LEAN_MEM_MB', 'LEAN_TIMEOUT',
        'LEAN_MAX_CORES'}
 
-print(' '.join(sorted(n for n in reads - assigns - ENV if not n.isdigit())))
+# INDIRECT EXPANSION DEFEATS TEXT ANALYSIS, so say so instead of staying
+# silent. `n=Q; echo "${!n}"` reads Q, and no amount of pattern-matching
+# recovers that from the source. The guard's contract is that it does not miss
+# a dependency; where it cannot honour that it must refuse, not shrug.
+if re.search(r'\$\{!', payload):
+    print('INDIRECT-EXPANSION')
+else:
+    print(' '.join(sorted(n for n in reads - assigns - ENV if not n.isdigit())))
 PYGUARD
 )
 
+if [ "$UNBOUND" = "INDIRECT-EXPANSION" ]; then
+  cat <<EOF
+FATAL: $LABEL uses indirect expansion (\${!name}).
+       The set of variables it reads cannot be derived from its text, so this
+       guard cannot certify that the lift carries them. Rewrite the phase
+       without indirection, or lift it with a driver that is known-complete by
+       other means and say so in the self-test.
+EOF
+  exit 1
+fi
 if [ -n "$UNBOUND" ]; then
   cat <<EOF
 FATAL: $LABEL reads variables this lift does not define: $UNBOUND