Linearity bounds for APN functions
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-11-01-000013
curl -X POST /api/v1/records/palomar/PALOMAR-2026-11-01-000013/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-11-01-000013/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'