# 三條自然數列的全稱編碼

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-at-most-countable-set/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-at-most-countable-set-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

N₀×{0,1,2}以c(n,j)=3n+j單射到N₀，故至多可數。

有限集合證書加上全稱整數仿射編碼；不提出不可數性結論。





## 已知條件與符號


- calc


- G1 — N₀={n∈Z:n≥0}；X=N₀×{0,1,2}；c(n,j)=3n+j。


- N_0 — 含0的自然數
- c — 仿射整數編碼
- j — 三條列索引





## 規則與來源


- calc · prerequisite — 假設整數帶餘除法、非負整數與單射定義；至多可數以存在到N₀的單射定義。
- mko_definition · cited — 本輪以完整有限集合證書或整數仿射編碼的全稱單射證書處理。某個編碼失敗只否證該witness，不證集合不可數。 · mko-at-most-countable-set





## 逐步主鏈

S01 · implies操作前

(n,j)\in X

操作後

n\ge0,\quad j\in\{0,1,2\}\Rightarrow3n+j\in N_0

條件：無

規則：calc · 依賴：G1

葉節點依據：calc

編碼是整數且非負，所以codomain宣告正確。



S02 · implies操作前

c(n,j)=c(m,k)

操作後

3(n-m)=k-j

條件：無

規則：calc · 依賴：G1, S01

葉節點依據：calc

對任意兩輸入假設像相同，移項得3的倍數等於小差。



S03 · implies操作前

j,k\in\{0,1,2\}

操作後

-2\le k-j\le2,\quad3\mid(k-j)\Rightarrow k-j=0

條件：無

規則：calc · 依賴：G1, S02

葉節點依據：calc

範圍內唯一3的倍數是0，因此j=k。



S04 · implies操作前

3(n-m)=0,\quad j=k

操作後

n=m,\quad(n,j)=(m,k)

條件：無

規則：calc · 依賴：G1, S02, S03

葉節點依據：calc

整數中3非零，消去3得到n=m，故c全稱單射。



S05 · implies操作前

c:X\hookrightarrow N_0

操作後

X\text{ is at most countable}

條件：無

規則：calc · 依賴：G1, S01, S04

葉節點依據：calc

這個全稱單射直接滿足至多可數定義，不依有限測試。



S06 · implies操作前

r\in N_0

操作後

r=3q+j,\quad q\in N_0,\quad j\in\{0,1,2\}

條件：無

規則：calc · 依賴：G1, S04

葉節點依據：calc

非負整數帶餘除法亦給每個r的前像，因此此特定c其實是雙射。



S07 · implies操作前

Y=\{a,b,c\},\quad e(a)=0,e(b)=1,e(c)=2

操作後

e:Y\hookrightarrow N_0,\quad |Y|=3

條件：無

規則：calc · 依賴：G1

葉節點依據：calc

完整三元素映射的像互異，給有限集合的至多可數證書。



S08 · implies操作前

b(n,j)=3n

操作後

b(0,0)=b(0,1)=0,\quad c(0,0)=0\ne1=c(0,1)

條件：無

規則：calc · 依賴：G1, S05

葉節點依據：calc

另一編碼b碰撞，只否證b這個witness；已證的c仍認證同一X。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · G1, S05 — 一個壞編碼不能推出X不可數，因已有完整反證性良好編碼。
- S07 · premise_audit · G1 — Y至多可數但不是可數無限，因此兩個術語不能混同。
- S06 · premise_audit · G1, S04 — 額外滿射證書才允許稱X可數無限；前一步單射本身只證至多可數。
- S05 · premise_audit · G1, S01, S04 — 不需要先證滿射；至多可數也容許有限集合。
- S04 · premise_audit · G1, S02, S03 — 相等像已推出輸入兩座標都相等，不只第一座標。
- S03 · premise_audit · G1, S02 — 兩端界−2與2都必須納入；沒有±3所以結論成立。
- S02 · premise_audit · G1, S01 — 這裡沒有抽樣n或m，是全稱碰撞分析。
- S01 · premise_audit · G1 — 若允許n負數便不一定進入N₀；參數域不可省。





## 錯誤控制與反例

參數域c的證明固定n≥0及0≤j≤2；允許j=3會和下一條列碰撞。

見證與集合編碼失敗只否證該函數；不可直接標集合不可數。


- b(n,j)=3n是單射。 → reject — (0,0)與(0,1)都送到0。
- b失敗表示X不可數。 → reject — c(n,j)=3n+j已全稱證單射。
- 有限Y至多可數，因此Y可數無限。 → reject — Y只有三個元素，不與無限N₀雙射。





## 結論與限制

N₀×{0,1,2}以c(n,j)=3n+j單射到N₀，故至多可數。







## 驗證及來源綁定

1 個本稿宣告算術檢查；只支持所列算式。


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: bcd07b59b5e83e1216ba1fb8c780353d2a97cf3c8fd58ec701dee7656e7f25d5
- original source SHA-256: bcd07b59b5e83e1216ba1fb8c780353d2a97cf3c8fd58ec701dee7656e7f25d5
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-at-most-countable-set-01.json)