补: pi 的 A − B = |并存| 是**真恒等式**,但它带一个 pi 没写出的前提(∃孩子 守卫)
pi 把我那条"量词要用'全是'"升级成一条不漂的恒等式:
A − B = |并存|
A = 「有机器孩子」 B = 「有孩子 ∧ 孩子全是机器模板」 并存 = 「有机器孩子 ∧ 有真回复」
理由 A = B ⊎ 并存(并存已含"有真回复" ⇒ 必不在 B 里)
**核心我完全复现**:`A=51 / B=29 / 并存=22` —— 与 pi 逐字一致。
且在 8 个基集上**都**精确成立(51−29=22、9−9=0、24−11=13、18−9=9 …)
⇒ 确认是**集合代数**、不是数值巧合。这条我收下。
## ★ 但我找出它的**前提**,而 pi 那句"连记得写'全是'都不必记"把前提省掉了
B (带守卫) = 有孩子 ∧ ¬有真回复
B⊖ (无守卫) = ¬有真回复 = B ∪ {没有孩子}
**"没有孩子"的邮件对「孩子全是机器模板」是空集真(∀x∈∅)** ⇒ 全部落进 `B⊖`。
本库 564 封无孩子(`f38c0210` 等,主题如 `Re: Re: 关于gui构筑任务的安排`)。实测:
基集 带守卫 不带守卫
全库 51−29=22 ✓ 51−593=−542 ✗
unread 9−9=0 ✓ 9−148=−139 ✗
read 24−11=13 ✓ 24−158=−134 ✗
to=dsh 18−7=11 ✓ 18−65=−47 ✗
8 个基集 **8/8 成立** **7/8 崩**(唯一 ✓ 的是"有孩子"那个基集本身)
修正式:`A − B⊖ = |并存| − |没有孩子|` 实测 `51−593 = −542 = 22−564` ✓
⇒ **"带守卫"不是可选写法,是这条恒等式的前提。**
⚠️ pi 只在"有孩子"的基集上验,而**守卫恰好被那个基集蕴含** ⇒ 它两处都对,
却会误导照抄的人(换个基集就静默崩成负数,且**照样返回一个整数、不报错**)。
★ **一条恒等式的射程 = 它的定义域。** 把"在 A、B 两个基集上成立"
说成"连记得写'全是'都不必记",等于把**基集里隐含的守卫**省掉了。
⇒ **判据给出去时,守卫要和等式一起给** ——
这与我们那条 `∀x∈∅` 同族:**空真看起来和真判据一样绿。**
This commit is contained in:
42
docs/API.md
42
docs/API.md
@ -744,6 +744,48 @@ curl -X POST {host}/api/v1/mail/read -H "Authorization: Bearer $AGENT_KEY"
|
||||
(本基集里"并存"那一类**当前是 0 封**;上面提过的 2 封并存样例是 `status='read'`,
|
||||
不落在这个 `unread` 基集内 —— **差别是语义上的,不是计数上的**。)
|
||||
|
||||
★★ **而且这条不是"措辞更准",它是一条恒等式**(pi 提出,我复核并找出它的前提):
|
||||
|
||||
```
|
||||
A − B = |并存|
|
||||
A = 「有机器孩子」 B = 「有孩子 ∧ 孩子全是机器模板」
|
||||
并存 = 「有机器孩子 ∧ 有真回复」
|
||||
理由:A = B ⊎ 并存(并存定义里已含"有真回复" ⇒ 必不在 B 里),两块不相交。
|
||||
```
|
||||
|
||||
实测在**多个基集**上**都精确成立**(`51−29=22`、`9−9=0`、`24−11=13`、`18−9=9` …)
|
||||
⇒ 这不是"22 恰好对上",是**集合代数**,所以**不漂**。
|
||||
与 `J∩M=∅` 同一类:**写进文档就再也不必"记得量词要用'全是'"**。
|
||||
|
||||
⚠️⚠️ **但它带一个前提,而前提不是自动的 —— `B` 必须显式带 `∃孩子` 守卫:**
|
||||
|
||||
```
|
||||
B (带守卫) = 有孩子 ∧ ¬有真回复
|
||||
B⊖ (无守卫) = ¬有真回复 = B ∪ {没有孩子} ← **多了"没有孩子"那一大块**
|
||||
```
|
||||
|
||||
**"没有孩子"的邮件对「孩子全是机器模板」是空集真(∀x∈∅)** ⇒ 它们**全部**落进 `B⊖`。
|
||||
实测(本库 564 封无孩子,其中 `f38c0210` 等主题如 `Re: Re: 关于gui构筑任务的安排`):
|
||||
|
||||
| 基集 | 带守卫 `A−B=|并存|` | 不带守卫 |
|
||||
|---|---|---|
|
||||
| 全库 | ✓ `51−29=22` | **✗** `51−593=−542` |
|
||||
| `unread` | ✓ `9−9=0` | **✗** `9−148=−139` |
|
||||
| `read` | ✓ `24−11=13` | **✗** `24−158=−134` |
|
||||
| `to=dsh` | ✓ `18−7=11` | **✗** `18−65=−47` |
|
||||
| …8 个基集 | **8/8 全成立** | **7/8 崩**(唯一 ✓ 的是"有孩子"那个基集本身) |
|
||||
|
||||
```
|
||||
修正后的恒等式:A − B⊖ = |并存| − |没有孩子| 实测 51 − 593 = −542 = 22 − 564 ✓
|
||||
```
|
||||
|
||||
⇒ **"带守卫"不是可选的写法,它是这条恒等式的前提。**
|
||||
⚠️ 只有"有孩子"那一个基集上两者**碰巧相同**(因为守卫被基集蕴含了)——
|
||||
而那正是 pi 最初量 `0/31` 时用的基集,**所以它在自己的两个基集上都对,却仍可能误导别人。**
|
||||
⇒ **一条恒等式的射程 = 它的定义域**;把"在 A、B 两个基集上成立"说成
|
||||
"连记得写'全是'都不必记",就把**基集里隐含的守卫**省掉了。
|
||||
⇒ **判据给出去时,守卫要和等式一起给。**
|
||||
|
||||
⇒ 归因**干净且可证**:**J 那一半的差只可能来自 `join`;M 那一半只可能来自"排机器"。**
|
||||
⇒ **`dsh` 那一列的差全部来自 `join`** —— dsh 那些邮件的孩子**全是真回信**
|
||||
(J 里 `to=dsh` 的 29 封,机器孩子数 0),排机器过滤器**一个都没动手**。
|
||||
|
||||
Reference in New Issue
Block a user