Cryptographic Boolean Functions in Lean

2. Boolean functions and coding🔗

Chapter 3 defines Reed--Muller codes and proves the order-one specialization and full general-order form of Carlet's Theorem 1, Proposition 12's complete minimum-weight equality classification, the dimension and cardinality formulas, and Theorem 2 on duality.

  1. 2.1. Reed--Muller codes