{"id":"palomar/PALOMAR-2026-11-01-000013","url":"https://github.com/cbe90/Linearity-bounds-for-APN-functions/tree/d470936098c6cb9671da7eae0dacd1871eeba262","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-11-01-000013-v1.json","repo":"https://github.com/cbe90/Linearity-bounds-for-APN-functions","tags":["math.CO","cs.IT","msc:06E30","msc:05B10","msc:11B13","msc:11T71"],"score":0,"title":"Linearity bounds for APN functions","trust":"high","domain":"math.CO","source":"palomar","authors":["Christof Beierle","Lukas Kölsch"],"reviews":0,"subject":"math.CO","summary":"Lean 4 formalization of linearity bounds for almost perfect nonlinear (APN) maps F: 𝔽₂ⁿ → 𝔽₂ⁿ. Write N = 2ⁿ and let L(F) denote the maximum Walsh magnitude over components indexed by nonzero vectors. For n ≥ 5, the formalization establishes L(F) ≤ N − 6, together with L(F) ≤ N − √N/4 − 2 when n is even. For n ≥ 4, ordering the Walsh magnitudes in nonincreasing order as L_k(F) gives L_k(F) ≤ (N/√k)√(1 + (2^(k−1) − 1)/N) for 1 ≤ k ≤ N(N − 1). In particular, L₂(F) ≤ 2⌊N/3⌋ and L₄(F) ≤ N/2. Further bounds relate linearity to the count q of nonplateaued components with nonzero indices. In odd…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-11-01","reactions":{},"formalized":true,"formalizes":[{"title":"Linearity bounds for APN functions","identifier":"arXiv:2609.35689","relationship":"formalizes"}]}