Balanced cuts turn coverage into a Toffoli bound
On this page · Permalink · Source line 256
Choose a cut after \(\lfloor T/2\rfloor\) Toffolis. Both sides have at most \(\lceil T/2\rceil\) Toffolis. Reversing the suffix preserves its count because every gate is self-inverse. Each forward or inverse-suffix coordinate has degree at most \(\lceil T/2\rceil+1\), and their XOR has the same upper bound.
For every positive \(v\), completeness chooses a discrepancy \(H_i\) that detects \(v\). Its safety and degree bound imply
The integer rounding matters. If \(T=2r\), the first bound gives \(2\beta\le T+2\). If \(T=2r+1\), it gives \(2\beta\le T+3\). The uniform bound uses the latter constant.
An affine output mask \(\ell(x)\) costs zero additional Toffolis: append CNOTs from restored inputs and, if needed, a target NOT. This constructs a restored oracle for \(f+\ell\), so the bound applies to every affine mask. Define
Together with the output degree bound,
There are finitely many affine masks. The Lean definition uses the least upper bound of their beta values, which equals this finite maximum. Its affine-output theorem constructs legal gates rather than assuming masks are free transformations of an arbitrary interior computation.
Written theorem and archived endpoint restored_degree_and_cover_bound; the dual is a separate written result.