Pigeonhole.lean

View source on GitHub

compress

A helper that removes one element from Fin (n+1), compressing the remaining elements into Fin n. Elements below the removed value keep their index; elements above shift down by 1.

private def compress {n : Nat} (v x : Fin (n + 1)) (h : x ≠ v) : Fin n :=
  if hlt : x.val < v.val then
    ⟨x.val, by omega⟩
  else
    ⟨x.val - 1, by ...⟩

Fin.no_injection

There is no injective function from Fin (n+1) to Fin n. Proved by induction on n with element removal at each step.

theorem Fin.no_injection (n : Nat)
    : ∀ g : Fin (n + 1) → Fin n, ¬ Function.Injective g

Base case: Fin 1 → Fin 0 is impossible since Fin 0 is empty. Inductive step: given g : Fin (k+2) → Fin (k+1), remove the image of the last element from the codomain. The compressed function g' : Fin (k+1) → Fin k inherits injectivity, contradicting the induction hypothesis.

pigeonhole

Among N+1 values in Fin N, at least two must collide. The collision gives specific indices i < j where f i = f j.

theorem pigeonhole {N : Nat} (f : Fin (N + 1) → Fin N)
    : &exists; i j : Fin (N + 1), i < j ∧ f i = f j

Uses Fin.no_injection by contradiction: if no collision existed, f would be injective, which is impossible.

# Pigeonhole: N+1 items into N slots => collision
# This is why bounded transducers must repeat states.

def find_collision(values, num_slots):
    """Map N+1 values into Fin(N). Return colliding pair."""
    seen = {}
    for i, v in enumerate(values):
        slot = v % num_slots
        if slot in seen:
            return (seen[slot], i, slot)
        seen[slot] = i
    return None  # impossible if len(values) > num_slots

N = 4
items = list(range(N + 1))  # 5 items into 4 slots
i, j, slot = find_collision(items, N)
print(f"{N+1} items into {N} slots:")
print(f"  item[{i}]={items[i]} and item[{j}]={items[j]}"
      f" both map to slot {slot}")
print(f"  Collision guaranteed — no injection from"
      f" Fin({N+1}) to Fin({N})")

pigeonhole_nat

A convenience wrapper for Nat-indexed sequences: among values f(0), ..., f(N), at least two in Fin N must collide.

Connections

• Stochasticity.lean — uses pigeonhole to get state collisions in bounded transducers
• Removal.lean — A3 and Co1 removal tests assume the collision that pigeonhole provides
• Axioms.lean — capacity_bound gives the finite state space that pigeonhole needs