KW88

This repository is a Lean 4 formalization of the core Karchmer-Wigderson connection between boolean circuit depth and communication complexity, based on

M. Karchmer and A. Wigderson, Monotone Circuits for Connectivity Require Super-logarithmic Depth, STOC 1988.

If you want the one-line summary, it is this:

• circuit depth is the same thing as Karchmer-Wigderson communication complexity;
• the monotone version says the same thing with minterms and maxterms; and
• formula size gives an upper bound on the protocol partition number.

This is not meant to be a giant proof dump. The point of the project is to make the underlying mechanism legible: circuits, protocol trees, validity conditions, the rectangle property, and then the theorem-level equivalences on top.

What is formalized

The development includes:

• boolean circuits in negation normal form;
• monotone circuits;
• deterministic protocol trees for two-party communication;
• the KW game and its monotone variant;
• the rectangle property for protocol trees;
• circuit-to-protocol and protocol-to-circuit constructions;
• the depth/communication-complexity equivalences; and
• the bound pp(f) ≤ L(f).

The main theorem-facing declarations live in KW88/KW.lean:

• KW.commComplexity_le_circuitDepth
• KW.circuitDepth_le_commComplexity
• KW.circuitDepth_eq_commComplexity
• KW.commComplexityMono_le_monoCircuitDepth
• KW.monoCircuitDepth_le_commComplexityMono
• KW.monoCircuitDepth_eq_commComplexityMono
• KW.protPartNum_le_formulaSize

For convenience, the paper-number names are still there as aliases: lemma_2_1, lemma_2_2, theorem_2_1, lemma_2_1_mono, lemma_2_2_mono, and theorem_2_2.

File layout

• KW88/Core.lean contains the infrastructure: circuits, protocol trees, KW-validity, the rectangle API, and the circuit-to-protocol constructions.
• KW88/KW.lean contains the theorem layer: the main equivalence results, the monotone version, and the protocol-partition/formula-size bound.
• KW88.lean is the public root module.
• KW88.pdf is the paper this project is tracking against.

Build

This project uses Lean 4 with mathlib. From the repository root:

lake exe cache get
lake build KW88

If you only want to check a single module:

lake env lean KW88/Core.lean
lake env lean KW88/KW.lean

The current lakefile.toml targets mathlib v4.28.0.

Scope

This repository is focused on the KW machinery itself, not the full downstream connectivity lower-bound story from the paper. In other words: the communication complexity/circuit-depth interface is the main object here.

That is deliberate. I would rather have a clean standalone formalization of the core engine than a bloated repo that tries to swallow the whole paper at once.

License

MIT. See LICENSE.