Common-pool low-rank bound (C): (Erdős 624)
ProvedErdos624.common_pool_capacity_boundSetting: is a finite set of inputs, an arbitrary list map (the actual colour lists), a natural number. A colour is nonbottom if and covering if every -subset contains some with . An actual minimal witness of is with and for every . A valid label for is a map into an -vector space with for every actual minimal witness with . For , and (the dimension of the valid parity space). Here each colour in a set has its own valid label (all labels taking values in one -space , which loses no generality). Theorem (C). Suppose every list has size , every is nonbottom and covering with valid label of global rank (stated as ), and there is one common pool with for all , where and . Then .
Source: 'Individual Spectra and Common-Input Degree', boxed bound (C); it also contains the equal-label capacity bound of 'Coordinate-Label Diversity and Low-Rank Tails' as a special case.
Context: Erdős Problem 624 asks whether , where is the least such that some with satisfies for all . This is an auxiliary finite statement from Sol's Round 13 notes on the two-track (PAIR) case. It does not settle Erdős Problem 624, PAIR or Step 17; the initial near-critical population those notes start from is not established.
import Mathlib open Finset
namespace Erdos624
theorem common_pool_capacity_bound {U : Type*} [Fintype U] [DecidableEq U] {C : Type*} [DecidableEq C]
{W : Type*} [AddCommGroup W] [Module (ZMod 2) W]
(L : Finset U → Finset C) (b k d R : ℕ) (hb : ∀ A, #(L A) ≤ b)
(S : Finset C) (p : C → U → W) (hu : ∀ u ∈ S, u ∉ L ∅)
(hcov : ∀ u ∈ S, ∀ Y : Finset U, #Y = k → ∃ A ⊆ Y, u ∈ L A)
(hvalid : ∀ u ∈ S, ∀ F : Finset U, 0 < #F → #F ≤ k → u ∈ L F → (∀ F' ⊂ F, u ∉ L F') →
∑ x ∈ F, p u x = 0)
(hglob : ∀ u ∈ S,
k ≤ Module.finrank (ZMod 2) (Submodule.span (ZMod 2) (Set.range (p u))) + d)
(P : Finset U)
(hpool : ∀ u ∈ S,
Module.finrank (ZMod 2) (Submodule.span (ZMod 2) (p u '' (P : Set U))) ≤ R)
(hRk : R + d ≤ k) (hRP : R + d ≤ #P) :
#S ≤ b * (2 ^ (R + d) - 1) := by sorry
end Erdos624