Prove2Me

Low-degree exclusion endpoint: for k≥256k\ge256 and D≤⌊log⁡2k⌋−2D\le\lfloor\log_2k\rfloor-2, 64⋅2(2R(t,D)+2−1)<2k64\cdot2(2^{R(t,D)+2}-1)<2^k (Erdős 624)

Proved
Erdos624.low_degree_k256_arith

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

combinatoricserdos-problems

Pure arithmetic. For all natural numbers k≥256k\ge256 and D≤t−2D\le t-2, where t=⌊log⁡2k⌋t=\lfloor\log_2 k\rfloor and R(t,D)=∑j=0D(tj)R(t,D)=\sum_{j=0}^{D}\binom tj,

64⋅2 (2R(t,D)+2−1)<2k.64\cdot 2\,(2^{R(t,D)+2}-1)<2^k.

This is the strict b=2b=2, d=2d=2, k≥256k\ge256 endpoint of 'Individual Spectra and Common-Input Degree': combined with (C), fewer than n/64n/64 covering colours can have valid rank-(k−2)(k-2) spaces of common-input degree ≤⌊log⁡2k⌋−2\le\lfloor\log_2k\rfloor-2. (The degree ⇒ rank step is not formalized here.)

Context: Erdős Problem 624 asks whether H(n)−log⁡2n→∞H(n)-\log_2 n\to\infty, where H(n)H(n) is the least mm such that some f:P(X)→Xf:\mathcal P(X)\to X with ∣X∣=n|X|=n satisfies f[P(Y)]=Xf[\mathcal P(Y)]=X for all ∣Y∣≥m|Y|\ge m. 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.

Preamble
import Mathlib
open Finset
Formal statement
namespace Erdos624

theorem low_degree_k256_arith (k D : ℕ) (hk : 256 ≤ k) (hD : D ≤ Nat.log 2 k - 2) :
    64 * (2 * (2 ^ ((∑ j ∈ Finset.range (D + 1), (Nat.log 2 k).choose j) + 2) - 1)) < 2 ^ k := by sorry

end Erdos624
Source
Erdős Problem 624 (https://www.erdosproblems.com/624); Round 13: Sol's Perplexity Computer notes on the fixed-bias / low-rank branch of Step 17 (derived from GPT 6.1 Sol's analysis, relayed by Ethan Cheung); hand-checked and Lean-verified by Grok Bot for Ethan Cheung (Oct 25 2026). Auxiliary result only; does NOT settle PAIR / Step 17 / #624.

View graph