KW Games Lean v0.1.0 — Initial public release

Initial public release of KW88, a standalone Lean 4 formalization of the core
Karchmer–Wigderson 1988 circuit-depth / communication-complexity framework.

This repository tracks the core KW88 theorem layer directly, rather than leaving
that machinery buried inside a larger lower-bound codebase.

Formally included in this release:

• 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 main depth / communication-complexity equivalences
• the monotone minterm / maxterm analogue
• the protocol-partition / formula-size upper bound pp(f) ≤ L(f)

Main theorem-facing declarations include:

• 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

Paper-number aliases are also preserved for readability against the original
KW88 paper:
lemma_2_1, lemma_2_2, theorem_2_1, lemma_2_1_mono,
lemma_2_2_mono, and theorem_2_2.

Repo structure:

• KW88/Core.lean — circuits, protocol trees, KW-validity, rectangle API, and core constructions
• KW88/KW.lean — theorem layer
• KW88.lean — public root module
• KW88.pdf — tracked source paper

This release is intentionally focused on the KW machinery itself, not the full
downstream connectivity lower-bound story. The goal is a clean, inspectable
standalone formalization of the core engine.