AUY83

This repository is a Lean 4 formalization of core results from

A. V. Aho, J. D. Ullman, and M. Yannakakis, On Notions of Information Transfer in VLSI Circuits, STOC 1983.

The project centers on the communication-complexity side of the paper: fooling-set measures, combinatorial rectangles, protocol partition number, formula-to-protocol constructions, and lower bounds for inner product.

What is in the development

• problem and partition models for AUY83-style information transfer;
• two-way, left-going, right-going, and one-way fooling-set notions;
• combinatorial rectangles and rectangle covers;
• protocol trees and the protocol partition number;
• boolean formulas and formula-to-protocol constructions; and
• lower-bound machinery for the inner-product example.

The main modules are:

• AUY83/Basic.lean
• AUY83/FoolingSets.lean
• AUY83/Rectangles.lean
• AUY83/Formulas.lean
• AUY83/GF2.lean
• AUY83/LowerBounds.lean

AUY83.lean is the public root module.

Build

From the repository root:

lake exe cache get
lake build AUY83

To check individual modules:

lake env lean AUY83/Basic.lean
lake env lean AUY83/Formulas.lean
lake env lean AUY83/LowerBounds.lean

The project targets Lean v4.28.0 with mathlib v4.28.0.

Scope

This is a formalization of the AUY83 communication/formula lower-bound machinery, not a full VLSI hardware model. Where the paper states results whose clean Lean formalization would require additional graph-theoretic or asymptotic infrastructure, the current development focuses on the parts that make the core mechanism explicit. In particular, the VLSI area-time theorem is not included as a formal theorem in this repository, because the underlying chip model is not formalized here.

License

MIT. See LICENSE.