Collision identity for two maps $\mathcal P(U)\to U$ (Erdős 624)

Proved

Erdos624.collision_identity

by Ethan Cheung Wang · Oct 23, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricserdos-problems

Theorem. Let $|U|=n=2^k$ , $g_0,g_1:\mathcal P(U)\to U$ , and $Y\subseteq U$ with $|Y|=k$ . Let $J(Y)=\{g_i(A):i\in\{0,1\},A\subseteq Y\}$ and let $C(Y)=2n-|J(Y)|$ be the number of repeated evaluations among the $2n$ evaluations. Then

C(Y)=n+\bigl(n-|J(Y)|\bigr),

and the two maps have a common hole on $Y$ if and only if $C(Y)>n$ . An elementary bookkeeping identity: a two-map common hole needs more than $n$ collisions, not just large separate losses.

Formalization Note. $U=\mathrm{Fin}\,(2^k)$ ; evaluations indexed by $\mathrm{Fin}\,2\times\mathcal P(Y)$ .

Preamble

import Mathlib
import Definitions.Def_Erdos624_defs
open Finset

Formal statement

namespace Erdos624

theorem collision_identity (k : ℕ) (g : Fin 2 → Finset (Fin (2 ^ k)) → Fin (2 ^ k))
    (Y : Finset (Fin (2 ^ k))) (hY : #Y = k) :
    #((univ : Finset (Fin 2)) ×ˢ Y.powerset) -
        #(((univ : Finset (Fin 2)) ×ˢ Y.powerset).image (fun p => g p.1 p.2)) =
      2 ^ k + (2 ^ k - #(((univ : Finset (Fin 2)) ×ˢ Y.powerset).image (fun p => g p.1 p.2))) ∧
    ((∃ u, ∀ i, ∀ A ⊆ Y, g i A ≠ u) ↔
      2 ^ k < #((univ : Finset (Fin 2)) ×ˢ Y.powerset) -
        #(((univ : Finset (Fin 2)) ×ˢ Y.powerset).image (fun p => g p.1 p.2))) := by sorry

end Erdos624

Source

Erdős Problem 624 (https://www.erdosproblems.com/624); definitions from Formal Conjectures 624.lean; (1) of claim from GPT 6.1 Sol (fifth answer, Oct 23 2026), Lean-verified by Grok Bot for Ethan Cheung (Oct 23 2026)

View graph

Collision identity for two maps P(U)→U\mathcal P(U)\to UP(U)→U (Erdős 624)

Collision identity for two maps $\mathcal P(U)\to U$ (Erdős 624)