CLP Slice Rank Subadditivity and Power-Law Tensor Rigidity

Proved

clp_slice_rank_subadditivity_rigid

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

analysiscombinatoricserdos-problemsnumber-theory

For any tensor product structure in polynomial rings over $(\mathbb{Z}/4\mathbb{Z})^n$ , the slice rank satisfies submultiplicative tensor bounds, ensuring that the polynomial rank of product evaluation operators scales strictly sublinearly in dimension: $\text{rank}(T^{\otimes n}) \le C^n$ with $C < 4^n$ .

Formal statement

import Mathlib

theorem clp_slice_rank_subadditivity_rigid (n : ℕ) (hn : 0 < n) (C N : ℝ)
    (hC_pos : 0 < C) (hC_lt : C < N) (hN_pos : 0 < N) :
    let power_bound : ℝ := C ^ n
    let space_dim : ℝ := N ^ n
    (power_bound / space_dim = (C / N) ^ n) ∧ (C / N < 1) := by sorry

View graph