test(ac15): arrearsCallUserIDs 落成 fail-closed + 表驱动单测；W4-C 补「按用户额度」「跨用户不干扰」；BACKLOG B4

## 一、`arrearsCallUserIDs`：知识从注释变成闸

1. **每个分支挂 dump 依据**：
   · `counteract_arrears_course(IN inputStudentid INT, …)` —— 参数名就是 `inputStudentid`（`spdump proc` 头）⇒ 学生 id；
   · `use_activity_recommend(IN inputUserid INT, …)` —— 两处内嵌 CALL 分别是
     `…(inputUserid, …)` / `…(recommendUserid, …)`；行号 **763389 / 763410 由 team-lead 提供、我未独立复核**，
     本次在注释里把来源标出来（而不是当成自己核过的）。
2. **fail-closed**：未知 Op 返回**空集**，不许"不在表里就放行"。
   否则新增一支带 `Arrears` 的 Op 时忘了登记，校验会自动退化成"随便什么 key 都合法"——
   **而那种退化没有任何症状**。
3. **表驱动单测** `TestArrearsCallUserIDs`：三条（课酬→学生 id / 老带新→两个 userid / 未登记→空集）。
   它把"忘了登记"变成**单测红**，而不是等跑双跑才炸。

## 二、W4-C 补两条断言（team-lead 要求）

**① 每人各自的核销上限 = m，且 Σ ≤ m**（按用户汇总，不按全局）：
`legacy Σ=+5000 / target Σ=+5000 / 期望 +5000 / 上限 m=5000`（两个用户各一条）。
- `Σ ≤ m` 挡"核销无上限"；
- `Σ = m` 挡"额度没被用满"；
- **按用户**汇总挡"两人串成一份"（全局汇总 Σ=2m 会把"某人核两次、另一人没核"算成对的）。

**② 跨用户不干扰**：两次 CALL 是同一个 SP、同一个学校/校区，**只差第一个实参**。
"实参串了"在终态上表现为：某人 Σ=2m、另一人 Σ=0。
若只断言"两人各 +5000"而期望表也恰好是"两人各 5000"，总额照样对 —— 所以必须按用户分别比。

## 三、BACKLOG 新增 **B4 · 语句次序在双跑中不可观测**

按 team-lead 要求，顺序那条不只写在 W4-C 的 Note 里（Note 只对一条 case 可见）。
B4 写明：理由（终态对两域互不依赖的顺序不敏感）、已落地的处置、**不打算做 SQL 序列 harness**，
以及读法（"顺序不可观测" ≠ "这里没测"）。

## 四、报数（粘贴；两个门禁分两行）

```
分母：DefaultCases=55 ｜ 应跑 55 ｜ 实跑 55
总览：55 个 case，55 PASS，0 FAIL
Skipped 98 ｜ 业务 346 ｜ 基建 118 ｜ 未分类 0
代价 SQL 3350 次 / 19.561s / 60.9 次 per case / 356ms per case
grep "本块比对了" = 7

go build OK ｜ go vet OK ｜ go test OK
```

未 push。

internal/academic/dualrun/stage2/BACKLOG.md

@@ -281,3 +281,25 @@ DU-2 的 PASS 实际含义
 - 看到绿先问「**这条绿是哪条分支产生的**」：兜底分支？恒真断言？`0 vs 0`？
 - 再问「**这条绿值多少档**」：数这支的调用点；`= 0` 就把结论里的"验证"改成"复刻"
 - 只有能回答"是主判据、走的是主路径、非空、且档位已标注"的绿，才可以往交付结论里写
+
+---
+
+## B4 · 证据强度声明：SP 内**语句次序**在双跑中不可观测
+
+**结论**：凡"顺序风险"类判断（"必须先入账再核销，否则……"），目前**只能靠读 dump 正文得出**，
+**不能靠 case 兜住**。理由是硬性的，不是没做：
+
+- 双跑比对的是 **before / after 两份终态**；
+- 若两条语句改的是**互不依赖的两个域**（例：`t_user_expense*` 与 `t_courses_student`），
+  换序后终态**完全相同** ⇒ 终态上不存在可观测差异；
+- 顺序只在 **SQL 执行序列**里可见，而 harness 不记录序列。
+
+**已落地的处置**（3d W4-C）：不钉顺序，只钉"两件事都发生、金额各为 m"，
+并在 case Note 里写死"本 case 不声称钉住了次序"。
+
+**不打算做**：SQL 序列 harness（要接管 gorm 全部执行路径，成本远大于收益；
+且执行计划/批量路径一变就噪声满屏）。真要防"换序导致语义变"，前提是**换序会改变态** ——
+那种支不存在（若存在，终态断言本来就能抓住）。
+
+**读到这条的人要注意**：看到某 case 的 Note 写"顺序不可观测"时，不要把它当成"这里没测"，
+而要读成"**这里测的是终态等价，顺序不在本 case 的证明范围内**"。

internal/academic/dualrun/stage2/arrears_calls_test.go

@@ -0,0 +1,46 @@
+package stage2
+
+import "testing"
+
+// TestArrearsCallUserIDs 表驱动锁住"每条 Op 的 CALL 会把哪个 id 当 studentid 传出去"。
+//
+// 为什么必须有这张表：这条知识一旦只活在注释里，新增一支带 `Arrears` 的 Op 时
+// 最可能的结果是"忘了登记"，而 `arrearsCallUserIDs` 的 fail-closed 会让它 **FATAL** ——
+// 但只有本测试能把"忘了登记"变成一条**单测红**，而不是等到跑双跑时才炸。
+//
+// 另一个价值：它把「两个 SP 的第一实参不是同一种东西」这个事实固定下来（§19 的又一实例）。
+func TestArrearsCallUserIDs(t *testing.T) {
+	cases := []struct {
+		name string
+		c    Case
+		want []int64
+	}{
+		{
+			name: "课酬核销 → 学生 id（inputStudentid）",
+			c:    Case{Op: OpCounteractArrears, LegacyStudentID: 900001, LegacyUserID: 17735},
+			want: []int64{900001},
+		},
+		{
+			name: "老带新 → 两个 userid（inputUserid / recommendUserid）",
+			c:    Case{Op: OpUseActivityRecommend, LegacyUserID: 17735, RecommendUserID: 17738, LegacyStudentID: 0},
+			want: []int64{17735, 17738},
+		},
+		{
+			// fail-closed：未登记的 Op 必须返回空集 ⇒ key 检查全灭 ⇒ FATAL。
+			name: "未登记的 Op → 空集（fail-closed，不是放行）",
+			c:    Case{Op: OpRecharge, LegacyStudentID: 900001, LegacyUserID: 17735},
+			want: nil,
+		},
+	}
+	for _, tc := range cases {
+		got := arrearsCallUserIDs(tc.c)
+		if len(got) != len(tc.want) {
+			t.Fatalf("%s：期望 %v，实得 %v", tc.name, tc.want, got)
+		}
+		for i := range got {
+			if got[i] != tc.want[i] {
+				t.Fatalf("%s：期望 %v，实得 %v", tc.name, tc.want, got)
+			}
+		}
+	}
+}

internal/academic/dualrun/stage2/arrears_seed.go

@@ -450,19 +450,31 @@ func guardArrearsPairsUnused(ctx context.Context, tx *gorm.DB, c Case, side, cou
 
 // arrearsCallUserIDs 返回"这条 Op 的 CALL 会真正当作 `studentid` 传出去的那些 id"。
 //
-// 为什么要按 Op 分开：两个 SP 的第一个实参**不是同一种东西** ——
-// 课酬核销传的是学生 id，老带新传的是 userid（SP 内部把它当 studentid 用）。
-// 把它们并成一个集合，就会让"给课酬 case 种了一个 userid 的欠费行"这种错静默通过。
+// 两个 SP 的第一个实参**不是同一种东西** —— 这是 §19「同一列两套 id 空间」的又一个实例：
+//
+//	① sp_courses_student_counteract_arrears_course(IN inputStudentid INT, inputSchoolid, inputCampusid, inputMoney)
+//	   参数名就是 `inputStudentid`（见 `spdump proc` 的 CREATE PROCEDURE 头）⇒ **学生** id。
+//	   对应 case 字段 `LegacyStudentID`（RA-1 / RA-2 用 900001 / 900002）。
+//
+//	② sp_courses_activity_use_activity_recommend(IN inputUserid INT, inputOrder, inputRemark, inputCreateUserid)
+//	   第一实参是 `inputUserid`，而它的两处内嵌 CALL 是
+//	     `CALL sp_courses_student_counteract_arrears_course(inputUserid, …)`（被推荐人）
+//	     `CALL sp_courses_student_counteract_arrears_course(recommendUserid, …)`（推荐人）
+//	   —— dump 763389 / 763410（team-lead 提供行号；我独立核到的是"两处 CALL 的实参分别是
+//	   `inputUserid` / `recommendUserid`"，行号未独立复核，故标注来源）。
+//	   ⇒ 这一支传的是 **userid**，SP 内部把它当 studentid 去查 `t_courses_student.studentid`。
+//	   对应 case 字段 `LegacyUserID` / `RecommendUserID`。
+//
+// **fail-closed**：未知 Op 返回**空集**（不是"放行"）。
+// 空集会让 `validateArrearsSeed` 的 key 检查对所有 key 都失败 ⇒ FATAL。
+// 为什么必须这样：将来新增一支带 `Arrears` 的 Op 时若忘了登记，
+// "放行"会让校验**自动变成随便什么 key 都合法**，而那种退化没有任何症状。
 func arrearsCallUserIDs(c Case) []int64 {
 	switch c.Op {
 	case OpUseActivityRecommend:
 		return []int64{c.LegacyUserID, c.RecommendUserID}
 	case OpCounteractArrears:
 		return []int64{c.LegacyStudentID}
-	default:
-		if c.Arrears != nil {
-			return []int64{c.LegacyStudentID, c.LegacyUserID, c.RecommendUserID}
-		}
-		return nil
 	}
+	return nil
 }

internal/academic/dualrun/stage2/recommend_compare.go

@@ -264,6 +264,50 @@ func recommendArrearsAssertions(c Case, lg, tg *SideResult) ([]Diff, []Assertion
 				e.Row.RemainderReceivableCents, c.AmountCents),
 		})
 	}
+	// ---- 每人各自的核销上限 = m，且 Σ核销 ≤ m ----
+	//
+	// 为什么按**用户**汇总而不是全局汇总：两个 CALL 的上限各自都是 `activityMoney`，
+	// 全局汇总（Σ = 2m）会把"某人被核了两次 / 另一人没被核"算成正确。
+	type userSum struct{ l, t, want int64 }
+	sums := make(map[int64]*userSum, len(c.Arrears.ByUser))
+	for _, u := range c.Arrears.userIDs() {
+		sums[u] = &userSum{}
+	}
+	for _, e := range c.Arrears.flatRows() {
+		w := want[e.Row.BizNo]
+		sums[e.User].l += lgD[e.Row.BizNo].NetDelta
+		sums[e.User].t += tgD[e.Row.BizNo].NetDelta
+		sums[e.User].want += w.NetDelta
+	}
+	for _, u := range c.Arrears.userIDs() {
+		s5 := sums[u]
+		asserts = append(asserts, Assertion{Kind: AssertionBusiness,
+			Name: fmt.Sprintf("W4-C 用户 %d 的核销总额 = m 且 ≤ m（每人各自一份额度，不与另一人共享）", u),
+			Pass: s5.l == s5.want && s5.t == s5.want && s5.l <= c.AmountCents && s5.t <= c.AmountCents,
+			Detail: fmt.Sprintf("legacy Σ=%+d ｜ target Σ=%+d ｜ 期望 %+d ｜ 本人上限 m=%d。"+
+				"`<= m` 挡「核销无上限」，`= m` 挡「额度没被用满」，按用户汇总挡「两人串成一份」",
+				s5.l, s5.t, s5.want, c.AmountCents)})
+	}
+
+	// ---- 跨用户不干扰（W4-C 独有维度）----
+	//
+	// 两条 CALL 是同一个 SP、同一个学校/校区，**只差第一个实参**。
+	// "实参串了"（把推荐人的 id 传成被推荐人的）在终态上的表现是：
+	// 一个人的行被核两次（Σ = 2m），另一个人的行完全没动（Σ = 0）。
+	// 若只断言"两人各有一行 +5000"，而期望表恰好也是"两人各 5000"，总额仍然对得上 ——
+	// 所以必须**按用户分别**比对，这一条才抓得住它。
+	if len(c.Arrears.ByUser) == 2 {
+		ids := c.Arrears.userIDs()
+		a, b := sums[ids[0]], sums[ids[1]]
+		asserts = append(asserts, Assertion{Kind: AssertionBusiness,
+			Name: "W4-C 跨用户不干扰：两次 CALL **各动各自的行**（不是把同一个 id 传两次）",
+			Pass: a.l == a.want && b.l == b.want && a.t == a.want && b.t == b.want &&
+				a.want > 0 && b.want > 0,
+			Detail: fmt.Sprintf("user %d：legacy %+d / target %+d（期望 %+d）｜ user %d：legacy %+d / target %+d（期望 %+d）。"+
+				"若某人 Σ=2m 而另一人 Σ=0 ⇒ 两次 CALL 的**第一个实参是同一个 id**",
+				ids[0], a.l, a.t, a.want, ids[1], b.l, b.t, b.want)})
+	}
+
 	// 正向断言：**两个用户各核了一笔**。少了它，"两侧都 0"会全绿 ——
 	// 而那正是"第二个 CALL 没执行"或"两个用户共用一个额度"的形态。
 	asserts = append(asserts, Assertion{Kind: AssertionBusiness,