# 基本計數原理：數字互異的三位偶數有幾個

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

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

derivation-mko-counting-principle-01 · production-20261019-adopted-96



## 目標與範圍

計算 100 到 999 之間、三個數字兩兩相異的偶數共有幾個。要求：只把互斥的類別相加；每次相乘之前，先確認每個階段的可選數對所有先前選擇都相同，不同時先分支。

只處理有限集合的計數（MKO 假設 a1）：用互斥類別的加法原理（a2）與逐階段的乘法原理（a3），並由有限計數的基本事實證明本稿使用的「依賴型」乘法引理。不處理一般的排容原理、排列組合公式或無限集合；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- finite_counting_basics
- cartesian_product_def
- injective_surjective_def
- set_operations_def
- numeric_evaluation


- G1 — 三位數是滿足 100≤n≤999 的整數；每個這樣的 n 恰有一種寫法 n=100d₁+10d₂+d₃，其中 d₁∈W⁺、d₂,d₃∈W（見 decimal_rep）。
- G2 — 所求集合 T={n∈ℤ ∣ 100≤n≤999，n 是偶數，且 n 的三個數字兩兩相異}。
- G3 — 記號：[n]={k∈ℕ ∣ 1≤k≤n}；|S|=n 表示存在雙射 S→[n]。


- T — 所求的數的集合
- d_1,d_2,d_3 — 百位、十位、個位數字
- W,\ W^{+} — W={0,1,2,3,4,5,6,7,8,9}，W⁺=W∖{0}
- E — 偶數字 {0,2,4,6,8}
- D,\ D_0,\ D_+ — 數字三元組的集合及其兩個類別
- [n] — 集合 {k∈ℕ ∣ 1≤k≤n}
- |S| — 有限集合 S 的元素個數





## 規則與來源


- finite_counting_basics · prerequisite — 有限計數：互斥有限集合 A、B 有 |A∪B|=|A|+|B|；|A×B|=|A|·|B|；有限集之間存在雙射 ⇔ 元素個數相同。
- cartesian_product_def · prerequisite — 笛卡兒積：A×B 是所有有序對 (a,b)（a∈A、b∈B）的集合；(a,b)=(c,d) ⇔ a=c 且 b=d。
- injective_surjective_def · prerequisite — 單射：f(a)=f(a′) ⇒ a=a′。滿射：每個 b∈B 都有 a∈A 使 f(a)=b。雙射：既單又滿，此時有唯一反函數 f⁻¹ 使 f⁻¹∘f=id_A、f∘f⁻¹=id_B。
- set_operations_def · prerequisite — 集合運算：x∈A∪B ⇔ x∈A 或 x∈B；x∈A∩B ⇔ x∈A 且 x∈B；x∈A∖B ⇔ x∈A 且 x∉B；在全集 U 中 Aᶜ=U∖A。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- divides_def · prerequisite — 整除：對整數 a、b，a∣b 表示存在整數 k 使 b=ak。
- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
- set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- subset_def · prerequisite — 子集：A⊆B 表示 A 的每個元素都是 B 的元素，即 ∀x (x∈A⇒x∈B)。
- eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。
- def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
- function_def · prerequisite — 函數：f:A→B 對每個 a∈A 指定恰好一個 f(a)∈B。兩函數相等 ⇔ 定義域、對應域相同且對每個 a 都有相同值。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- eq_refl_symm_trans · prerequisite — 等號的性質：u=u；若 u=v 則 v=u；若 u=v 且 v=w 則 u=w。
- mko_counting · cited — 互斥選擇類別的數量相加；連續選擇階段的可能組合數，在各階段選項數與條件明確時相乘。 · mko-counting-principle
- decimal_rep · prerequisite — 十進位表示：每個滿足 100≤n≤999 的整數 n 恰有一組數字 (d₁,d₂,d₃) 使 n=100d₁+10d₂+d₃，其中 d₁∈{1,2,3,4,5,6,7,8,9}、d₂,d₃∈{0,1,2,3,4,5,6,7,8,9}；反之每組這樣的數字給出一個這樣的 n。
- even_def · prerequisite — 整數 n 是偶數，意思是 2∣n，即存在整數 k 使 n=2k。
- finite_subset · prerequisite — 有限集合的子集合仍是有限集合。
- L_remove · lemma — 若有限集合 S 有 s 個元素，且 R⊆S 有 r 個元素，則 |S∖R|=s−r。
- L_stage · lemma — 設有限集合 X 有 m 個元素，且對每個 x∈X，有限集合 Yₓ 恰有 n 個元素（n 對所有 x 相同；集合 Yₓ 本身可以依 x 而不同）。則 P={(x,y) ∣ x∈X, y∈Yₓ} 有 m·n 個元素。





## 逐步主鏈

S01 · implies操作前

T

操作後

|T|=|D|,\ D=\{(d_1,d_2,d_3)\mid d_1\in W^{+},\ d_2,d_3\in W,\ 100d_1+10d_2+d_3\ \text{even},\ d_1,d_2,d_3\ \text{pairwise distinct}\}

條件：無

規則：decimal_rep · 依賴：G1, G2, decimal_rep

葉節點依據：decimal_rep + injective_surjective_def + finite_counting_basics

把每個 n∈T 對應到它的數字三元組 (d₁,d₂,d₃)。依 decimal_rep，這個三元組存在且唯一，所以對應是一個函數；反向以 (d₁,d₂,d₃)↦100d₁+10d₂+d₃ 還原 n，所以它是 T 到 D 的雙射。「偶數」與「數字相異」兩個條件原封不動地搬到 D。依 finite_counting_basics，有雙射的兩個有限集合元素個數相同，所以 |T|=|D|。



S02 · equivalent操作前

100d_1+10d_2+d_3\ \text{even}

操作後

d_3\in E=\{0,2,4,6,8\}

條件：d_3\in W

規則：divides_def · 依賴：S01, even_def, divides_def

葉節點依據：divides_def + even_def + distributive

令 n=100d₁+10d₂+d₃。因 100d₁+10d₂=2(50d₁+5d₂)（分配律），n−d₃ 是 2 的倍數。若 n=2k，則 d₃=2(k−50d₁−5d₂) 是偶數；反之若 d₃=2j，則 n=2(50d₁+5d₂+j) 是偶數。所以 n 偶 ⇔ d₃ 偶。0 到 9 之中的偶數字恰為 0、2、4、6、8。



S03 · equivalent操作前

D

操作後

D=\{(d_1,d_2,d_3)\mid d_1\in W^{+},\ d_2\in W,\ d_3\in E,\ d_1\neq d_2,\ d_1\neq d_3,\ d_2\neq d_3\}

條件：無

規則：set_extensionality · 依賴：S01, S02

葉節點依據：set_extensionality + set_builder

把 S01 中的「偶數」條件換成 S02 的等價條件 d₃∈E，並把「兩兩相異」拆成三個不等式。每個三元組在改寫前後滿足的條件同真同假，所以集合不變。



S04 · case_split操作前

D

操作後

D=D_0\cup D_+,\ D_0\cap D_+=\varnothing,\ D_0=\{t\in D\mid d_3=0\},\ D_+=\{t\in D\mid d_3\in\{2,4,6,8\}\}

條件：無

規則：set_operations_def · 依賴：S03, set_operations_def

葉節點依據：set_operations_def + case_analysis

為什麼要分支：若先選個位 d₃，百位 d₁ 的可選數會依 d₃ 而變。d₃=0 時，0 本來就不在 W⁺ 中，d₁ 有 9 種；d₃∈{2,4,6,8} 時，d₃ 是非零數字，必須從 W⁺ 中扣掉，只剩 8 種。MKO 假設 a3 要求每個階段的可選數相對於先前選擇明確給出，可選數不固定時就必須分支。兩類別互斥，因為 d₃ 不能同時是 0 又屬於 {2,4,6,8}；合起來涵蓋 D，因為 E={0}∪{2,4,6,8}。



S05 · theorem_application操作前

D=D_0\cup D_+,\ D_0\cap D_+=\varnothing

操作後

|D|=|D_0|+|D_+|

條件：D_0\cap D_+=\varnothing

規則：finite_counting_basics · 依賴：S04, finite_counting_basics, mko_counting

葉節點依據：finite_counting_basics + finite_subset + mko_counting

加法原理（MKO 第一句、finite_counting_basics）：兩個互斥有限集合之聯集的元素個數是兩者個數之和。D₀、D₊ 都是有限集 D 的子集合，所以有限。



S06 · implies操作前

d_3=0

操作後

|W^{+}\setminus\{0\}|=9,\ \ |W\setminus\{0,d_1\}|=8\ \text{for every}\ d_1\in W^{+}

條件：d_1\neq 0

規則：L_remove · 依賴：S04, L_remove

葉節點依據：L_remove + finite_counting_basics + numeric_evaluation

在 D₀ 中 d₃=0。階段一選 d₁：允許集合是 W⁺∖{0}，因 0∉W⁺，它就是 W⁺，有 9 個元素。階段二選 d₂：要與 d₁、d₃ 都不同，允許集合是 W∖{0,d₁}。因 d₁≥1，d₁≠0，所以 {0,d₁}⊆W 恰有 2 個元素；依引理 L_remove，|W∖{0,d₁}|=10−2=8，而且對每個 d₁ 都是 8。



S07 · theorem_application操作前

D_0

操作後

|D_0|=9\cdot 8=72

條件：|W\setminus\{0,d_1\}|=8\ \text{for every}\ d_1\in W^{+}

規則：L_stage · 依賴：S04, S06, L_stage

葉節點依據：L_stage + finite_counting_basics + numeric_evaluation

映射 (d₁,d₂,0)↦(d₁,d₂) 是 D₀ 到 P₀={(d₁,d₂) ∣ d₁∈W⁺, d₂∈W∖{0,d₁}} 的雙射：在 d₃=0 時，d₁≠d₃ 自動成立，d₂≠d₃ 就是 d₂≠0，再加上 d₂≠d₁。取 X=W⁺（m=9）、Y_{d₁}=W∖{0,d₁}（依 S06 每個都是 n=8 個），依引理 L_stage 得 |D₀|=|P₀|=9·8=72。注意 Y_{d₁} 本身依 d₁ 而不同（Y₁ 不含 0、1，Y₂ 不含 0、2），但個數相同，這正是引理所要求的。



S08 · implies操作前

d_3\in\{2,4,6,8\}

操作後

|W^{+}\setminus\{d_3\}|=8,\ \ |W\setminus\{d_1,d_3\}|=8\ \text{for every}\ d_1\in W^{+}\setminus\{d_3\}

條件：d_3\in W^{+}; d_1\neq d_3

規則：L_remove · 依賴：S04, L_remove

葉節點依據：L_remove + numeric_evaluation

在 D₊ 中，d₃∈{2,4,6,8}⊆W⁺，所以 {d₃}⊆W⁺，依 L_remove |W⁺∖{d₃}|=9−1=8，對四個 d₃ 都一樣。d₁ 從 W⁺∖{d₃} 中選，所以 d₁≠d₃，{d₁,d₃}⊆W 恰有 2 個元素，|W∖{d₁,d₃}|=10−2=8，對每一對 (d₃,d₁) 都一樣。



S09 · theorem_application操作前

Q=\{(d_3,d_1)\mid d_3\in\{2,4,6,8\},\ d_1\in W^{+}\setminus\{d_3\}\}

操作後

|Q|=4\cdot 8=32

條件：|W^{+}\setminus\{d_3\}|=8\ \text{for every}\ d_3\in\{2,4,6,8\}

規則：L_stage · 依賴：S08, L_stage

葉節點依據：L_stage + numeric_evaluation

D₊ 的前兩個階段：先選 d₃（4 種），再選 d₁（依 S08 每次 8 種）。依引理 L_stage（m=4、n=8），這些有序對共 32 個。



S10 · theorem_application操作前

D_+

操作後

|D_+|=32\cdot 8=256

條件：|W\setminus\{d_1,d_3\}|=8\ \text{for every}\ (d_3,d_1)\in Q

規則：L_stage · 依賴：S03, S04, S08, S09, L_stage

葉節點依據：L_stage + injective_surjective_def + finite_counting_basics + numeric_evaluation

映射 (d₁,d₂,d₃)↦((d₃,d₁),d₂) 只重排坐標，是 D₊ 到 {(q,d₂) ∣ q=(d₃,d₁)∈Q, d₂∈W∖{d₁,d₃}} 的雙射；兩邊的條件相同：d₃ 為非零偶數字、d₁∈W⁺、d₁≠d₃、d₂≠d₁、d₂≠d₃。再用一次 L_stage（X=Q，m=32；依 S08 每個 q 之後 n=8）得 |D₊|=32·8=256。



S11 · equivalent操作前

|D|=|D_0|+|D_+|

操作後

|D|=72+256=328

條件：無

規則：eq_replace · 依賴：S05, S07, S10

葉節點依據：eq_replace + numeric_evaluation

把 S07 的 |D₀|=72 與 S10 的 |D₊|=256 代入 S05 的加法式：|D|=72+256=328。



S12 · implies操作前

D=D'_{\mathrm{odd}}\cup D'_{\mathrm{even}}\ \text{(branch on}\ d_1)

操作後

|D|=5\cdot 5\cdot 8+4\cdot 4\cdot 8=200+128=328

條件：d_1\ \text{odd: } |E\setminus\{d_1\}|=5; d_1\ \text{even: } |E\setminus\{d_1\}|=4

規則：L_stage · 依賴：S03, L_stage, L_remove, S05

葉節點依據：L_stage + L_remove + finite_counting_basics + numeric_evaluation

獨立核對：改成先選百位 d₁。此時個位 d₃∈E∖{d₁} 的個數依 d₁ 的奇偶而變，所以依 d₁ 的奇偶分成兩個互斥類別。d₁ 奇（1、3、5、7、9，5 種）：d₁∉E，d₃ 有 5 種，d₂∈W∖{d₁,d₃} 有 8 種，得 5·5·8=200。d₁ 偶（2、4、6、8，4 種）：d₁∈E，d₃ 有 4 種，d₂ 有 8 種，得 4·4·8=128。相加 328，與 S11 一致。



S13 · implies操作前

|T|=|D|,\ |D|=328

操作後

|T|=328

條件：無

規則：eq_refl_symm_trans · 依賴：S01, S11, S12

葉節點依據：eq_refl_symm_trans

由 S01 的 |T|=|D| 與 S11 的 |D|=328，依等號傳遞得 |T|=328：100 到 999 之間數字兩兩相異的偶數共 328 個，其中 72 個以 0 結尾，256 個以 2、4、6 或 8 結尾。







## 局部子步與引理

S06.1 · implies操作前

R\subseteq S,\ |S|=s,\ |R|=r

操作後

|S\setminus R|=s-r

條件：R\subseteq S

規則：finite_counting_basics · 依賴：finite_counting_basics, set_operations_def, subset_def, finite_subset

葉節點依據：finite_counting_basics + set_operations_def + subset_def + finite_subset + eq_congruence

S 的每個元素要嘛屬於 R，要嘛屬於 S∖R，不會兩者都是；又因 R⊆S，R 的元素都在 S 中。所以 S=(S∖R)∪R 且 (S∖R)∩R=∅。S∖R 是 S 的子集合，因此有限。依加法原理 s=|S∖R|+r，兩邊同減 r 得 |S∖R|=s−r。此子步證得引理 L_remove。



S07.1 · definition操作前

|X|=m,\ |Y_x|=n\ (x\in X)

操作後

\Phi:P\to X\times[n],\ \Phi(x,y)=(x,\varphi_x(y))

條件：|Y_x|=n\ \text{for every}\ x\in X

規則：def_intro · 依賴：G3, finite_counting_basics

葉節點依據：def_intro + function_def

依 G3，|Yₓ|=n 表示有雙射 φₓ:Yₓ→[n]；對有限多個 x 各固定一個。定義 Φ(x,y)=(x,φₓ(y))。因 x∈X 且 φₓ(y)∈[n]，Φ 的值確實在 X×[n] 中。



S07.2 · implies操作前

\Phi(x,y)=(x,\varphi_x(y))

操作後

\Phi\ \text{is a bijection}

條件：無

規則：injective_surjective_def · 依賴：S07.1, injective_surjective_def, cartesian_product_def

葉節點依據：injective_surjective_def + cartesian_product_def

單射：若 Φ(x,y)=Φ(x′,y′)，依有序對相等得 x=x′ 且 φₓ(y)=φₓ(y′)，φₓ 是單射，所以 y=y′。滿射：任取 (x,k)∈X×[n]，φₓ 是滿射，有 y∈Yₓ 使 φₓ(y)=k，於是 (x,y)∈P 且 Φ(x,y)=(x,k)。可以依 x 而不同的是雙射 φₓ，不能依 x 而不同的是目標 [n]。



S07.3 · implies操作前

\Phi:P\to X\times[n]\ \text{bijective}

操作後

|P|=|X\times[n]|=m\cdot n

條件：無

規則：finite_counting_basics · 依賴：S07.2, finite_counting_basics

葉節點依據：finite_counting_basics

依 finite_counting_basics，有雙射的兩個有限集合個數相同，且 |X×[n]|=|X|·|[n]|=m·n。S07.1 到 S07.3 合起來證得引理 L_stage。







## 逐步反向審查


- S13 · sufficient_goal_reduction · S01, S11, eq_refl_symm_trans — 目標 G：|T|=328。足夠條件 H：T 與 D 之間有雙射且 |D|=328；H⇒G 由等號傳遞。H 由 S01 與 S11 從已知正向證成，沒有把 G 當作前提；S12 只是獨立核對。
- S12 · premise_audit · L_stage, L_remove, S05 — 這是換一個階段順序的第二次計數，同樣先分支再相乘；它與 S11 一致，增加信心，但結論仍由 S01 到 S11 推出。
- S11 · inverse_equivalence · S07, S10, eq_replace — 等值代換與精確加法（N8）兩向都成立。
- S10 · premise_audit · S08, S09, L_stage, finite_counting_basics — 第三階段的可選數 8 必須對每一對 (d₃,d₁) 都成立，S08 用 d₁≠d₃ 證明了這一點。坐標重排是雙射，所以個數不變。
- S09 · premise_audit · S08, L_stage — 引理的條件「每個 d₃ 之後都恰有 8 種 d₁」由 S08 提供。
- S08 · premise_audit · L_remove, S04 — 需要 d₃∈W⁺（被扣掉的確實在 W⁺ 中）與 d₁≠d₃（被扣掉的兩個數不同）。d₃=0 時第一個條件不成立，這正是 S04 分支的原因。
- S07.3 · premise_audit · S07.2, finite_counting_basics — 若各 Yₓ 個數不同，就沒有共同的 [n]，乘積公式失效。反例：X={a,b}、|Y_a|=1、|Y_b|=3，則 |P|=4，不等於 2·1 也不等於 2·3。
- S07.2 · premise_audit · S07.1, injective_surjective_def, cartesian_product_def — 兩個方向各自用到 φₓ 的單射與滿射性質；不宣稱 Φ 以外的任何對應是雙射。
- S07.1 · premise_audit · G3, def_intro — 此步只引入記號；它依賴「所有 Yₓ 對應到同一個 [n]」，也就是每個 Yₓ 都恰有 n 個元素。
- S07 · premise_audit · S06, L_stage, finite_counting_basics — 引理需要每個 Y_{d₁} 的個數都等於同一個 n；S06 對所有 d₁∈W⁺ 證明了 n=8。只檢查一個 d₁ 不夠。
- S06.1 · premise_audit · finite_counting_basics, subset_def, set_operations_def — 需要 R⊆S。反例：S={1,2}、R={2,3}，S∖R={1} 有 1 個元素，但 s−r=0。
- S06 · premise_audit · L_remove, S04 — 關鍵條件是 d₁≠0，它保證被扣掉的集合有 2 個元素而不是 1 個；這正是 a3 要求的「可選數對所有先前選擇相同」。
- S05 · premise_audit · S04, finite_counting_basics, finite_subset — 必須引用 S04 的互斥性；若類別重疊（例如「末位為 0」與「首位為 2」），直接相加會把交集算兩次（見錯誤控制一）。
- S04 · premise_audit · S03, set_operations_def — 需要兩件事：類別涵蓋全部 D，且互不重疊。前者保證不漏算，後者保證 S05 的加法不重算。
- S03 · inverse_equivalence · S02, set_extensionality — 條件逐項等價，集合依外延原則雙向相同。
- S02 · inverse_equivalence · divides_def, even_def, distributive — 兩個方向都各自寫出了整數 k 或 j，所以是等價；N1 核對 n−d₃=2(50d₁+5d₂) 這個多項式恆等式。
- S01 · premise_audit · G1, decimal_rep, finite_counting_basics — 需要表示的存在（對應有定義）與唯一（不會一個數對到兩個三元組）。若表示不唯一，數字三元組的個數就可能多於數的個數。此步只宣稱兩集合等大，不宣稱其他性質。





## 錯誤控制與反例

互斥才能直接相加MKO 指出的第一個常見誤解是對會重疊的案例直接相加。在 T 中，「個位為 0」有 72 個，「百位為 2」有 4·8=32 個，但兩者重疊於 210、230、240、250、260、270、280、290 這 8 個數。直接相加得 104，把重疊部分算了兩次；正確的聯集個數是 72+32−8=96（MKO 假設 a2：重疊需另外修正）。S04 的兩類以 d₃ 是否為 0 來分，不可能重疊，所以 S05 可以直接相加。

可選數依前一步改變時不能無條件相乘MKO 指出的第二個誤解：「先選個位 5 種，再選百位 8 種、十位 8 種」得 5·8·8=320。錯在「百位 8 種」只在個位非零時成立；個位為 0 時百位有 9 種。單看 d₃=0 這一類，錯誤算法給 1·8·8=64，實際是 72，正好少了 8 個；320+8=328。正確做法是 S04 的分支，或 S12 的另一種分支。

階段順序可換，但每個順序都要重新核對先選百位、再選十位、最後選個位時，若寫成 9·8·5=360，就假設了個位永遠剩 5 個偶數字。但百位或十位若用掉偶數字，剩下的會變少，例如 d₁=2、d₂=4 時個位只剩 0、6、8 三種。換順序本身沒有錯，錯在沒有核對每個階段的可選數是否固定；S12 依 d₁ 的奇偶分支後才相乘。


- 個位 5 種、百位 8 種、十位 8 種，所以 |T|=5·8·8=320 → reject — 個位為 0 時百位有 9 種；正確答案是 328。
- 百位 9 種、十位 8 種、個位 5 種，所以 |T|=360 → reject — 個位可選的偶數字數依前兩位而變；d₁=2、d₂=4 時只剩 3 種。
- T 中個位為 0 或百位為 2 的數有 72+32=104 個 → reject — 兩類重疊 8 個（210、230 等）；正確個數是 96。
- D₀ 與 D₊ 的個數都是乘出來的，所以 |D|=72·256 → reject — 互斥類別用加法合併；乘法只用於同一流程中先後相接的階段。





## 結論與限制

100 到 999 之間、三個數字兩兩相異的偶數共有 328 個：依個位分成互斥的兩類，個位為 0 的有 9·8=72 個，個位為 2、4、6、8 的有 4·8·8=256 個。改為依百位奇偶分支也得到 200+128=328。


- N2 在 100 到 999 的每個整數上核對「n 的奇偶與個位數字的奇偶相同」，是有限檢查，恰好涵蓋本題用到的全部 900 個數；S02 的論證不依賴它。
- 十進位表示的存在與唯一（decimal_rep）是本稿的前提，未在本稿中由帶餘除法推出。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 7f8dccaca5069630be4159d5fe0095ba10e312d6050c11349077668b0fd09b5a
- original source SHA-256: 7f8dccaca5069630be4159d5fe0095ba10e312d6050c11349077668b0fd09b5a
- Lean: NOT_RUN · independent AI: NOT_MEASURED

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-counting-principle-01.json)