diff --git a/deploy/check-relay-counts.sh b/deploy/check-relay-counts.sh index 8aa115f..63d103c 100755 --- a/deploy/check-relay-counts.sh +++ b/deploy/check-relay-counts.sh @@ -198,11 +198,23 @@ chk_true "**空真**: kind<>'failure' 的计数 == 已绑定(对全表恒真 "$([ "$NAIVE" -eq "$BOUND" ] && echo 1 || echo 0)" chk_true "真判据 **严格小于** 空真判据(否则判据没起作用)" \ "$([ "$REAL" -lt "$NAIVE" ] && echo 1 || echo 0)" -chk_true "子串 %failure% **多于** 三前缀(差即 homeagent 族 = 命名巧合)" \ - "$([ "$SUBSTR_N" -gt "$PREFIX_N" ] && echo 1 || echo 0)" -chk_eq "homeagent 族 == 子串 − 三前缀" "$HOMEAGENT" "$((SUBSTR_N - PREFIX_N))" -chk_true "残留集合 = 1 未绑定 + 1 已绑定(**不是同一行**)" \ - "$([ "$RESIDUE" -eq 2 ] && [ "$RESIDUE_UNBOUND" -eq 1 ] && echo 1 || echo 0)" +# ★ 量的是**包含关系**,不是"恰好只有四族": +# 三个前缀字面量本身都含 "failure" ⇒ 它们匹配的键必然也被 `%failure%` 匹配(子集)。 +# 而 homeagent 族既不以那三者为前缀、又含 failure ⇒ 必落在**差集**里(子集)。 +# 两条都由机制决定。先前写成 `HOMEAGENT == SUBSTR_N - PREFIX_N`,是把 +# "当下只存在这四个族"当成了不变量 —— 任一桥改用第五种拼法(如 `pi-failure:`) +# 会让差集 +1 而 homeagent 不变 ⇒ **假红**(新增命名是正常演进,不是故障)。已实测复现。 +chk_true "三前缀 ⊆ 子串(三前缀字面量都含 failure)" \ + "$([ "$PREFIX_N" -le "$SUBSTR_N" ] && echo 1 || echo 0)" +chk_true "homeagent 族 ⊆ 差集(它非三前缀之一、且含 failure)" \ + "$([ "$HOMEAGENT" -le "$((SUBSTR_N - PREFIX_N))" ] && echo 1 || echo 0)" +# ★ 那两行残留是**快照,不是不变量** —— 与文件头 24-27 行同一条规则。 +# 未绑定那行是"claim 后早退没退键"留下的化石;**清掉它是正确动作**, +# 而 `RESIDUE == 2 && UNBOUND == 1` 会把那个正确动作判成失败 +# (实测:清后 1/0 ⇒ 假红)。⇒ 改为只打印(见上面"当下读数"), +# 另用一条**与清理无关**的关系接住:未绑定必是占位,口径一致。 +chk_true "残留中未绑定的 ⊆ 占位行(未绑定必是占位,两者口径一致)" \ + "$([ "$RESIDUE_UNBOUND" -le "$PLACE" ] && echo 1 || echo 0)" chk_true "两口径抑制数**不同**(沿链范围不同 ⇒ 量的是不同集合)" \ "$([ "$S_FULL_S" -ne "$S_FAIL_S" ] && echo 1 || echo 0)" chk_true "完整链口径的抑制数 **大于** failure 链口径" \