# Collision and ceiling load in a complete map

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-pigeonhole-principle/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

derivation-mko-pigeonhole-principle-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

Use all fibres to prove a collision and the generalized lower bound.

A finite total map with nonempty codomain; no sampling inference about general maps.





## Givens and symbols


- work


- G1 — A={0,1,2,3,4}, B={a,b}, with complete f table(a,b,a,b,a).


- ℓ_b — load of box b
- m,k — domain and codomain sizes





## Rules and sources


- mko_definition · cited — For complete finite A,B and total f:A→B, |A|>|B| implies distinct a1,a2 with f(a1)=f(a2). The reverse size condition does not generally certify a given map injective. The generalized maximum-load bound is ceil(|A|/|B|), with a nonempty codomain. · mko-pigeonhole-principle
- work · prerequisite — Fibres of a finite total map form a partition; loads sum to the domain size; ceil(r)-1<r.





## Main derivation

S01 · impliesBefore

f=(a,b,a,b,a)

After

\forall x\in A:\ \exists!y\in B:\ f(x)=y

Conditions: none

Rule: work · Uses: G1, work

Leaf basis: work

Each of the five domain elements has one legal image, proving totality.



S02 · impliesBefore

|A|=5,\quad|B|=2

After

|A|>|B|

Conditions: none

Rule: work · Uses: G1, S01, work

Leaf basis: work

The finite sizes satisfy the strict inequality.



S03 · impliesBefore

f^{-1}(a)

After

\{0,2,4\},\quad\ell_a=3

Conditions: none

Rule: work · Uses: G1, S02, work

Leaf basis: work

List the complete fibre over a and its load.



S04 · impliesBefore

f^{-1}(b)

After

\{1,3\},\quad\ell_b=2

Conditions: none

Rule: work · Uses: G1, S03, work

Leaf basis: work

Complete the other fibre; both are disjoint and cover A.



S05 · impliesBefore

0\ne2,\quad f(0)=a=f(2)

After

f\text{ is not injective}

Conditions: none

Rule: work · Uses: G1, S04, work

Leaf basis: work

Give an actual collision witness with two distinct domain elements.



S06 · impliesBefore

\lceil|A|/|B|\rceil=\lceil5/2\rceil

After

\max(\ell_a,\ell_b)=3\ge3

Conditions: none

Rule: work · Uses: G1, S05, work

Leaf basis: work

The generalized ceiling bound is 3 and is attained here.



S07 · impliesBefore

\ell_b\le q-1\text{ for every box},\quad q=\lceil m/k\rceil

After

m=\sum_b\ell_b\le k(q-1)<m\quad(k\ge1)

Conditions: none

Rule: work · Uses: G1, S06, work

Leaf basis: work

If every load were below the ceiling, their sum would contradict the domain size m; therefore at least one load is at least ceil(m/k).



S08 · impliesBefore

A'=\{0,1\},\ B'=\{a,b\},\ g=(a,a)

After

|A'|\le|B'|\quad\text{but }g\text{ not injective}

Conditions: none

Rule: work · Uses: G1, S07, work

Leaf basis: work

A complete counterexample refutes the erroneous converse size condition.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · G1, S07, work — A smaller domain does not force an arbitrary map to be injective.
- S07 · premise_audit · G1, S06, work — The ceiling definition gives q-1<m/k; multiply by positive k.
- S06 · premise_audit · G1, S05, work — A nonempty codomain is required for this quotient.
- S05 · premise_audit · G1, S04, work — f(0)=f(0) is not a witness using distinct elements.
- S04 · premise_audit · G1, S03, work — The load sum3+2=5 cross-checks completeness.
- S03 · premise_audit · G1, S02, work — 0,2,4 are three distinct preimages.
- S02 · premise_audit · G1, S01, work — Equal sizes would not trigger this collision guarantee.
- S01 · premise_audit · G1, work — The entry for4 cannot be omitted.





## Error controls and negative controls

TotalityList all five entries with values in B.

CeilingRound5/2 upward to 3, not truncation.


- f(0)=f(0) is a collision certificate. → reject — The preimages must be distinct.
- |A|≤|B| forces f injective. → reject — g=(a,a) is a complete counterexample.
- Floor(5/2)=2 is the exact generalized bound. → reject — The theorem's bound is the ceiling3, not the floor2.





## Result and limitations

0 and 2 collide and maximum load3=ceil(5/2); the reverse size condition does not ensure injectivity.







## Verification and source binding

2 declared checks for this guide; only the listed expressions are covered.


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 48e01e622b425eb10256bc6b5df9a4828d74b8b553ae3c51ccf7fa2cb0e937d4
- original source SHA-256: f37dc77a23f2d409b8bd4520337371982021634ea482500e91e66470d7d0c189
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-pigeonhole-principle-01.json)