Reading the formal model literally
On this page · Permalink · Source line 208
QUANTIFIERS AND ENCODING CARRY THE HYPOTHESES The generic cut theory uses a logical-input type \(X\), a wire type \(W\) with decidable equality, and a boundary structure. Its essential fields are an encoding \(\mathrm{encode}:X\to\mathrm{Bool}\to(W\to\mathrm{Bool})\), a target wire, and the proof
This target equation separates the two target branches for each fixed input. It excludes an encoding that silently ignores its supplied target bit. The source proves Boundary.target_separated; it does not assume an injective encoding of every logical-input value as an additional hypothesis.
The restoration predicate is
It is a hypothesis of the conditional theorem. The code does not assert that every gate list realizes a restored oracle. The canonical encoding sets each input wire to its input bit, each ancillary wire to zero, and the target to \(b\). Its wire type is
Sum (Fin n) (Sum (Fin a) Unit)which has exactly \(n+a+1\) wires.
In the generic C01 theorem, completeness is the existential statement
No finite disjunction is needed there. Specializing to the canonical finite wires yields the finite complete family used in the main paper. Completeness does not say that the XOR of all packets reconstructs \(f\); detecting packets can cancel under XOR. It states existence of a detecting coordinate at every positive input.
No clean-intermediate condition occurs in these predicates. Legal gates may temporarily alter inputs, dirty scratch and use the target as a control. The source examples exercise those allowances. Its compute/copy/uncompute AND example uses two Toffolis and is a restoration witness, whereas direct AND uses one Toffoli. Neither example is an unrestricted circuit-search result.