# 完整映射的碰撞與ceil負載 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-pigeonhole-principle/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-pigeonhole-principle-01 · ocme-new142-reader-adoption-20261021 ## 目標與範圍 從全部fibers證碰撞及廣義下界。 有限total map、非空codomain；不由抽樣推一般映射。 ## 已知條件與符號 - work - G1 — A={0,1,2,3,4}，B={a,b}，f的完整table為(a,b,a,b,a)。 - ℓ_b — box b的load - m,k — domain與codomain大小 ## 規則與來源 - mko_definition · cited — 對完整有限A、B與total f:A→B，|A|>|B|推出存在a1!=a2且f(a1)=f(a2)。|A|<=|B|不保證給定map單射；generalized版本的最大load至少ceil(|A|/|B|)須另行明示。 · mko-pigeonhole-principle - work · prerequisite — finite total map的fibers形成partition；load總和等於domain大小；ceil(r)-1|B| 條件：無 規則：work · 依賴：G1, S01, work 葉節點依據：work 有限大小嚴格不等。 S03 · implies操作前 f^{-1}(a) 操作後 \{0,2,4\},\quad\ell_a=3 條件：無 規則：work · 依賴：G1, S02, work 葉節點依據：work 列a的完整fiber與load。 S04 · implies操作前 f^{-1}(b) 操作後 \{1,3\},\quad\ell_b=2 條件：無 規則：work · 依賴：G1, S03, work 葉節點依據：work 另一fiber也列完，兩fiber互斥且coverA。 S05 · implies操作前 0\ne2,\quad f(0)=a=f(2) 操作後 f\text{ is not injective} 條件：無 規則：work · 依賴：G1, S04, work 葉節點依據：work 給實際兩個不同domain元素的碰撞witness。 S06 · implies操作前 \lceil|A|/|B|\rceil=\lceil5/2\rceil 操作後 \max(\ell_a,\ell_b)=3\ge3 條件：無 規則：work · 依賴：G1, S05, work 葉節點依據：work 廣義下界的ceil為3，本例達到。 S07 · implies操作前 \ell_b\le q-1\text{ for every box},\quad q=\lceil m/k\rceil 操作後 m=\sum_b\ell_b\le k(q-1)