This repository contains code and data for verifying the Unit Gap Theorem: for any Boolean function f in the AND-Inverter Graph (AIG) basis, the gap between the tree upper bound and the optimal circuit size is at most 1. That is, tree_UB(f) - opt(f) in {0, 1}. The tree Bellman equation (minimizing 1 + opt(a) + opt(b) over all AND/NAND decompositions f = AND(a, b)) is therefore a 1-additive approximation to exact circuit complexity. We also verify the Threshold Law (gap = 1 implies opt >= n essential variables), the Tree Theorem (opt <= 3 implies gap = 0), and catalog the sharing mechanisms that cause gap = 1, finding exactly two (dual-polarity and same-polarity/CSE) through n = 7.

python -m venv .venv
source .venv/bin/activate
pip install -r requirements.txt

Requires Python 3.10+. The only external dependency is python-sat (used by the data generation script; the verify scripts need only the standard library).

All scripts should be run from the repository root.

python scripts/verify_unit_gap.py

Verifies gap in {0, 1} for all 3-input (248) and 4-input (20,660) functions. Prints the gap distribution by optimal cost level:

--- n=3 (248 non-trivial functions) ---
  gap    count   fraction
    0      222      89.5%
    1       26      10.5%

--- n=4 (20660 non-trivial functions) ---
  gap    count   fraction
    0    17564      85.0%
    1     3096      15.0%

python scripts/verify_threshold.py

Verifies that every gap=1 function satisfies opt(f) >= n_essential(f). Tests 3,122 gap=1 functions across n=3 and n=4 with 0 violations.

python scripts/verify_tree_theorem.py

Verifies that opt <= 3 implies gap = 0 (optimal tree circuit exists). Tests 1,362 functions. Shows the phase transition: gap=1 first appears at opt = 4.

python scripts/verify_mechanisms.py

Classifies all gap=1 circuits from n=5, n=6, and n=7 by sharing mechanism. Finds exactly two mechanisms with no new type through n=7:

  n  circuits  dual-pol       CSE   new?
  5        31       52%       48%     NO
  6       165       67%       33%     NO
  7        60       92%        8%     NO

See data/README.md for field descriptions.

MIT. See LICENSE.