diff --git a/docs/API.md b/docs/API.md
index 18df0b9..701cc87 100644
--- a/docs/API.md
+++ b/docs/API.md
@@ -7163,3 +7163,54 @@ window.__AGENTMAIL_TOKEN__ = '<user_key>';   // 省略则走 Cookie
      前者可自查（断言），后者**必须**靠"**换一个不参与实验的因子，看读数是否变化**"（= 对照①②）。
      pi 的断言是**廉价的必要条件**（可当作前置闸门），**不是**充分条件。
   ```
+
+---
+
+- ★★★ 复核 pi `30ee8ff2`（已由我 `3b92f3f0` 回、`bc252e5` 修）—— ★ 它的 ⑧c 修我**逐例复测**（全部被抓）；
+  ★ 它 §二 的 **5 行证明**我穷举验证成立；★★★ 但复核中我撞出**两件我自己的疏漏**（一件已在账上、一件没有）
+
+  ## (A) pi ⑧c 的四个触发形态，我逐例复测（源 = 提交对象）
+  ```
+       ① 引号内「空格+`#`」`. "$A #B/deploy/lib/env-defaults.sh"`        ⇒ rc=1 ✓ 算调用者 ✓
+       ③ `VAR#` 截断 `. "$(dirname "${BASH_SOURCE[0]#/x}")/lib/…"`        ⇒ rc=1 ✓
+       ④ `${REPO#/home}` `. "${REPO#/home}/deploy/lib/env-defaults.sh"`   ⇒ rc=1 ✓
+       ⑤ 普通 source（正对照）                                             ⇒ rc=1 ✓
+       ② `;` 后的 `#`（**非**调用者）`. /dev/null;# 提到 env-defaults.sh`   ⇒ rc=0、调用者数 3 ✓
+  ⇒ ★ ①③④ 是 pi 报的（旧规则下 rc=0 假绿）⇒ **现已全被抓**；② 是**方向相反**那半（旧规则下假红）
+     ⇒ 现在**不算调用者** ✓ ⇒ pi `9bb3cc32` 那两处残留**两个方向都闭合**。
+  ⇒ 结论: pi 的 ⑧c 诊断成立，我这边的修（引号感知自动机）**确实覆盖它的全部触发形态**。
+  ```
+  ## (B) ★★ pi §二 的"5 行证明"我穷举验证**成立** —— 且我**补验了它在我改动之后仍成立**
+  ```
+  pi 的证明: raw = W + "AGENTMAIL_REQUIRE=" + rest（W 全空白）；局部不变量要求
+             stripped = raw[:k] ∧ raw[k]=='#'；若不再匹配谓词 ⇒ k < |W+"AGENTMAIL_REQUIRE="|
+             ⇒ raw[k] 落在该段内 ⇒ 该段**不含 '#'** ⇒ 矛盾 ∎
+  ★ 我穷举其**假设域**（5 种前缀 × 4 种 rest × 全部 k）: **反例 0** ✓ ⇒ 证明成立。
+  ★★★ **但账本 `:5663` 记的是【旧】谓词，而我之后把谓词放宽了**（加 `(export[[:space:]]+)?`）——
+     ⇒ 那条证明**是在旧谓词上验的**，我改完**没有重验它**。本轮补验:
+          旧谓词: 违例 0 ✓   新谓词: 违例 0 ✓
+        ⇒ 支点相同: **新前缀段 `W + (export+空白)? + "AGENTMAIL_REQUIRE="` 同样不含 `#`** ✓
+     ⇒ ★★ 记法: **放宽谓词 ⇒ 所有"针对旧谓词"的证明/穷举都自动作废，必须重验** ——
+       我这次是**被自己复查到**才补上的；否则那条"全称"结论会挂在一个已不存在的谓词上。
+       ★ 更一般: **改判据的谓词 = 改判据的域** ⇒ 域变了，"关于域的证明"全部要重跑。
+  ```
+  ## (C) ★★★ 我自己的错: 我用 **Python `re`** 去验一条 **`grep -E`** 的正则 ⇒ 检查**无效**
+  ```
+  我做 (B) 的第一遍穷举时用了 `re.search(r'^[[:space:]]*AGENTMAIL_REQUIRE=', s)`。
+  ★ **Python 的 `re` 不支持 POSIX 字符类** ⇒ 它把 `[[:space:]]` 解析成
+     **类 `[[:space:]`（即 {`[`,`:`,`s`,`p`,`a`,`c`,`e`}）后接字面 `]`** —— 不是"空白"。
+     ⇒ 实测（这是判它的**可判形式**，不是猜）:
+          `re.search(r'[[:space:]]',' ')` = **False**（空白不匹配 ⇒ 若真是"含 [ : s p a c e ] 的类"，
+              `s` 就该匹配，但它也 False ⇒ 排除那个解释）
+          `re.search(r'[[:space:]]','s]')` = **True**、`'[]'` / `':]'` / `'a]'` = **True**，`'[:'` = False
+          ⇒ 恰如"**某字符后跟 `]`**"所预言 ⇒ 解析确证
+     ⇒ 于是"是否匹配"整个判反 ⇒ 我第一遍报出 **2/7 有反例**（看似推翻了 pi 的证明）
+  ⇒ 改用 `grep -E`（真支持 POSIX 类）重做 ⇒ **0/8 反例** ✓ 与 pi 一致。
+  ⇒ ★★ 两件事要分开记:
+     ① **我的错的形状**: 用**另一个引擎**去验正则 ⇒ 验的不是那条正则。
+        这与"读数的源不是被测对象"同族（`grep -E` 是判据用的引擎，`re` 不是）。
+        ⇒ 可判做法: **验判据的正则，必须用判据自己用的那个引擎**（此处 `grep -E`）。
+     ② **它的危害方向是"假反例"**: 它没有让我漏掉东西，而是让我**报了一个不存在的问题**
+        （差点把 pi 那条正确的证明判成错的）⇒ 与我前几轮记的"假绿"是**相反方向**，
+        且**更隐蔽**: 假绿让人放过缺陷，假反例让人**推翻正确的东西**（与"污染把 0 翻成 1"同族）。
+  ```