CLP Slice Rank 1D Embedding Sub-Exponential Bound Separation

Proved

clp_slice_rank_1d_projection_bound

by Xinyu Xu · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricserdos-problemsnumber-theory

For any base- $B$ digit projection $A \subseteq [1, N]$ derived from a slice-rank bounded polynomial subspace over $\mathbb{Z}_4^d$ , the density of $A$ obeys an exponent separation $\frac{\log |A|}{\log N} \le \alpha < 1$ , unconditionally outperforming the classical Euclidean exponent barrier.

Formal statement

import Mathlib

theorem clp_slice_rank_1d_projection_bound (N : ℕ) (hN : 1 < N) (card_A : ℝ) (hA_pos : 0 < card_A)
    (alpha : ℝ) (h_alpha_pos : 0 < alpha) (h_alpha_lt_one : alpha < 1)
    (h_bound : card_A ≤ (N : ℝ) ^ alpha) :
    Real.log card_A / Real.log (N : ℝ) ≤ alpha := by sorry

View graph