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

目標與範圍

計算 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 個元素。

逐步主鏈

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}\}

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

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

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\}

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\}\}

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

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

d_3=0

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

D_0

|D_0|=9\cdot 8=72

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\}

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

D_+

|D_+|=32\cdot 8=256

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

|D|=72+256=328

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

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

|T|=328

局部子步與引理

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

|S\setminus R|=s-r

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

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

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

\Phi\ \text{is a bijection}

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

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

逐步反向審查

• 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、反控制與修訂記錄）