Cryptographic Boolean Functions in Lean

2. Boolean functions and coding🔗

Chapter 3 develops the coding-theoretic structure of Boolean functions. The verified surface defines first-order Reed--Muller codes through algebraic degree and establishes their distance lower bound. The general-order distance theorem, equality classification, dimension formula, and duality remain visible as subsequent source-facing objectives.

  1. 2.1. Reed--Muller codes