Cryptographic Boolean Functions in Lean

1. Generalities on Boolean functions🔗

Chapter 2 develops scalar Boolean-function representations and the Fourier--Walsh interface. The verified surface covers algebraic and numerical normal forms, raw Walsh and pseudo-Boolean Fourier transforms, subspace identities, derivatives, finite-field representations, Hamming distance, and affine functions. Fourier-analytic results reuse FABL through explicit normalization bridges.

The Blueprint also records the remaining source-facing families: the complete affine-change and restriction laws, Proposition 5's integrality criterion, the full trace-monomial degree formula, and the spectral-support bounds. Their open status remains visible in the dependency graph.

  1. 1.1. Representation and Walsh foundations
  2. 1.2. Walsh inversion and Parseval
  3. 1.3. Fourier operations and subspaces
  4. 1.4. Derivatives and autocorrelation
  5. 1.5. Algebraic normal form skeleton
  6. 1.6. Algebraic normal form existence and uniqueness
  7. 1.7. Numerical normal form
  8. 1.8. Finite-field representations
  9. 1.9. Algebraic degree, distance, and affine functions