Every function through three inputs has a matching oracle
On this page · Permalink · Source line 389
The small calibration concerns every truth table on one, two, or three inputs. It is not a search through all reversible circuit words. A theorem lower bound and an explicit construction coincide.
Affine functions use target CNOTs and possibly NOT. A nonaffine quadratic through three bits has alternating quadratic rank two, so it is a product of two independent linear forms plus an affine residual. Compute those forms on clean wires, apply one Toffoli, uncompute, and append the residual.
Every three-bit cubic is a translated three-variable monomial plus an affine residual. The singleton monomial needs three Toffolis by complete coverage, and compute/toggle/uncompute attains that number.
The new figure script rebuilds and validates all 276 circuits and both target branches, covering 4,240 scalar input/target cases via exact truth tables. Its totals match the frozen baseline. Zero-input constants were checked in the separate dual suite, rather than being added to this 276-function count.
Matching written lower bounds and exact constructed implementations; not exhaustive optimal-circuit synthesis. The generic monomial cost theorem is not newly Lean-certified by this edition.