A minimal linear circuit interface

Wire types are generated by

A judgement $f:A\to B$ consumes the entire input interface and returns the specified output interface. Formation includes identities, permutations, sequential composition, and tensor composition:

The circuit constants used here are unitary gates, preparation of $|0⟩$, and destructive computational-basis measurement. Finite reversible code operations use NOT, CNOT, and Toffoli. Classical zero preparation and classical reversible gates act on $\mathsf{Bit}$ interfaces; their basis-permutation unitary lifts act on $\mathsf{Q}$ interfaces. No conversion between these types is implicit.

Linearity concerns ownership. Successive gates may consume and return the same physical factor. No rule duplicates a live quantum wire.