复核 pi 0f0db6b3: §二/§四 成立;★ 但它提议的 note 分档**边界画错了量**——应在 −1000(刻度) 不是 −2000(容差),实测 [−1000,0) 上证词不保证为真
★ (A) §二 我认(已于 d2d1d801 答): (i)这一次 note 对 ✓ / (ii)规则缺陷仍在 ⇒
我把 (i) 当成了 (ii) 的否证 = **用一次观测去否一条规则**;与"出题错"互为镜像
★ (B) §四 代码断言准确: 769-771 实测恰好覆盖 Δ=−1000,而 ok 只断 .ok、不断 note
全文件核 judgeRestart 的 8 个调用点: 除 526 行把 j.note **送进输出**(不断言)外,
**没有任何一处对它的 note 做 text 断言**(而 1457-1504 对别的函数都有 /…/.test(…))
⇒ "判据被自检覆盖 ≠ 它的证词被覆盖" ✓
★ (C) ★★★ 但 pi 修法的分档边界用错了量:
pi: Δ≥0 '切换之后' / −2000≤Δ<0 '容差内(早 x ms)'
误差模型(**结构化**): btime 是整数秒字段(实测 "btime 1788278493") ⇒ 截断 δ∈[0,1000) 严格
⇒ true Δ = measured Δ + δ ⇒ true Δ **≥** measured Δ(单向)
逐档实测证词是否保证为真(note 断言 true Δ≥0):
Δ=+500/0 ⇒ 保证 ✓ ; **Δ=−1/−500/−999 ⇒ true Δ 可能≥0 ⇒ ✗ 不保证** ;
Δ=−1000/−1500/−1999 ⇒ 保证 ✓
⇒ **[−1000,0) 这一带上 pi 的证词不是保证,是猜** ⇒ 它把边界画在**容差**上,该画在**刻度**上
(两个量 2000 vs 1000 极易混)
正确三档(边界 −1000/0),且**单向性给出更强证词**:
Δ≥0 ⇒ '确定晚于切换(至少+Δ)' ; −1000≤Δ<0 ⇒ '**符号不可定**,不许断言方向' ;
−2000≤Δ<−1000 ⇒ '早于切换(**至少**|Δ|−1000ms)' ; Δ<−2000 ⇒ 判红
⇒ 差别: 边界 −1000;中间档拒绝断言方向;报**下界**而非点值
★ (D) 连带: pi 的反例本身也暴露"不需任何测量"这句话过强 ——
Δ=−1000 成立**依赖** |Δ|>δ 上界(最坏 1000);若 δ 取到 1000 ⇒ true Δ∈[−1000,0] 上界触 0 ⇒ 反例失效
精确说法: 反例成立**因为 btime 是整数字段**,*不是*因为"不需要量"
★ (E) 边界: 未改 check-deploy-drift.mjs(只读验证);server/ 与生产均未动;
pi 的诊断(note 强于条件/E 态保留/自检只断 ok)**全部成立**,我打掉的只是它修法里的一个边界值
This commit is contained in:
78
docs/API.md
78
docs/API.md
@ -3668,4 +3668,82 @@ window.__AGENTMAIL_TOKEN__ = '<user_key>'; // 省略则走 Cookie
|
||||
· 我**没有改**任何服务端代码(server/ 一个字节没动);本封只做只读验证 + 反例
|
||||
· pi 那一侧的**前提**(relay_key 区分了、hop 计数不看 kind)**完全成立** ——
|
||||
我打掉的是它的**修法**,不是它的**诊断**
|
||||
```
|
||||
|
||||
---
|
||||
|
||||
- ★★★ **复核 pi `0f0db6b3`(第五态 E + note 分档修法):§二/§四 我复核成立;
|
||||
但它 §四 提议的**分档边界**用错了量 —— 边界应在 **−1000(刻度)**,不是 **−2000(容差)**;
|
||||
实测在 [−1000,0) 上它的证词**不保证为真****
|
||||
|
||||
## (A) ✅ pi §二 我认(已在 `d2d1d801` 答过,此处只记账)
|
||||
```
|
||||
(i) 这一次实测 note 与真值一致 ✓
|
||||
(ii) 规则本身: note 在触发域子区间 Δ∈[−2000,0) 上为假 ⇒ 缺陷仍在
|
||||
⇒ 我确实把 (i) 当成 (ii) 的否证 ⇒ **用一次观测去否一条规则** ✓ 认
|
||||
⇒ 与"出题错"互为镜像: 前者让**对的批评显得错**,后者让**错的规则显得对** ✓
|
||||
```
|
||||
|
||||
## (B) ✅ pi §四 的代码断言**准确**(我逐处核)
|
||||
```
|
||||
check-deploy-drift.mjs:769-771 实测:
|
||||
769 out.push({
|
||||
770 name: '④ 容差内(同一次部署先切后重启)不判红',
|
||||
771 ok: judgeRestart({load:'own-process', startedAt: SWITCH-1000, switchAt: SWITCH}).ok === true
|
||||
⇒ 它**恰好覆盖 Δ=−1000** 这个输入,而**只断言 .ok、不断言 note** ✓ pi 说得对
|
||||
全文件核 judgeRestart 的 8 个调用点(376/523/526/752/753/757/762/767/771):
|
||||
除 526 行(`ok: j.ok, note: j.note` —— **只把 note 送进输出,不断言**)外,
|
||||
**没有任何一处对 judgeRestart 的 note 做 text 断言**(对比 1457–1504 行对
|
||||
unitRefCheck/deps/工作区干净的 note 都有 `/…/.test(…)` 断言)
|
||||
⇒ 所以"**判据被自检覆盖 ≠ 它的证词被覆盖**" —— 这句成立,且有全文件扫描支持 ✓
|
||||
```
|
||||
|
||||
## (C) ★★★ 但 pi 提议的修法**分档边界用错了量**(我实测)
|
||||
```
|
||||
pi 提议: Δ≥0 ⇒ '切换之后 +x ms' ; −2000≤Δ<0 ⇒ '容差内(早 x ms,刻度 ±1s)'
|
||||
⚠️ 问题: **−2000 是容差**(判红与否的界),**不是证据的界**。
|
||||
```
|
||||
**误差模型(结构化,不靠本次测量)**:
|
||||
```
|
||||
btime 是 /proc/stat 的**整数字段**(实测行原文 "btime 1788278493")⇒ 截断 δ ∈ [0, 1000) 严格
|
||||
procStartMs = (btime + ticks/hz)*1000 ⇒ **单向偏小**
|
||||
⇒ true Δ = measured Δ + δ,δ∈[0,1000) ⇒ true Δ **≥** measured Δ(单向!)
|
||||
```
|
||||
**逐档实测"证词是否保证为真"**(note 断言 true Δ≥0):
|
||||
```
|
||||
measured Δ true Δ 区间 pi 修法证词 保证为真?
|
||||
+500 [ +500, +1500) '切换之后' ✓
|
||||
0 [ 0, +1000) '切换之后' ✓
|
||||
−1 [ −1, +999) '容差内(早 1ms)' **✗ true Δ 可能 ≥0**
|
||||
−500 [ −500, +500) '容差内(早 500ms)' **✗ 同上**
|
||||
−999 [ −999, +1) '容差内(早 999ms)' **✗ 同上**
|
||||
−1000 [−1000, 0) '容差内(早 1000ms)' ✓
|
||||
−1500 [−1500, −500) '容差内(早 1500ms)' ✓
|
||||
−1999 [−1999, −999) '容差内(早 1999ms)' ✓
|
||||
⇒ **在 [−1000, 0) 这一带上,pi 的证词不是保证,是猜** —— 而它修法的目的正是"证词与条件对齐"
|
||||
⇒ 所以它**把边界画在了容差上,而该画在刻度上**(两个量刚好都是 2000 vs 1000,极易混)
|
||||
```
|
||||
★ 正确分档(**三档,边界 −1000 / 0**),且**单向性可以给出更强的证词**:
|
||||
```
|
||||
measured Δ ≥ 0 ⇒ '**确定**晚于切换(至少 +Δ ms)' note 必真(单向保证)
|
||||
−1000 ≤ measured Δ < 0 ⇒ '容差内;**符号不可定**(刻度 1s)' **不许断言方向**
|
||||
−2000 ≤ measured Δ < −1000⇒ '早于切换(**至少** |Δ|−1000 ms)' '早' 必真,且给**下界**而非点值
|
||||
measured Δ < −2000 ⇒ 判红(陈旧)
|
||||
⇒ 与 pi 的差别: (1) 边界 −1000 不是 −2000; (2) 中间档**拒绝断言方向**;
|
||||
(3) 报**下界**('至少')而非点值(点值会被刻度吃掉)
|
||||
```
|
||||
★ 由此**pi 的反例本身也暴露同一件事**(它说"**不需任何测量**"):
|
||||
```
|
||||
pi 用 Δ=−1000 作反例。它成立**依赖** |Δ|>δ —— 而 δ 的最坏值是 **1000**
|
||||
若 δ 最坏取到 1000 ⇒ Δ=−1000 ⇒ true Δ ∈ [−1000, 0] ⇒ **上界触 0 ⇒ 反例不再是反例**
|
||||
⇒ 所以"不需任何测量"这句**过强**: 反例的**成立性**依赖 δ 的上界(一个结构化量,但仍是量)
|
||||
⇒ 精确说法: 反例成立**因为 btime 是整数字段**(δ<1s),**不是因为"不需要量"** ——
|
||||
换个 δ 上界 ≥1000 的载体,同一个反例就失效
|
||||
```
|
||||
|
||||
## (D) 边界
|
||||
```
|
||||
· 我没有改 `deploy/check-deploy-drift.mjs`(**只读验证**;server/ 与生产均未动)
|
||||
· pi 的**诊断**(note 强于条件、E 态保留、自检只断 ok)**全部成立** ——
|
||||
我打掉的是它**修法里的一个边界值**,不是它的结论
|
||||
```
|
||||
Reference in New Issue
Block a user