Track the represented operator, its normalizer and the accepted subspace. Keep preparation, SELECT, unprepare, workspace cleanup and resource tiers visible when composing constructions.
train · proof
A reversible source-loader on three little-endian bits is defined by the rule that maps each slot value s in {0,...,7} to (s XOR 3) mod 8, i.e. it flips the two low-order bits of s. Prove that this loader is its own inve…
local source supported
train · boundary
A fixed seven-wire reversible access circuit stores an address word on wires 0-2, a row word on wires 3-5, and one reusable work wire 6. On any input whose work wire is already 0, the circuit outputs the address word rep…
nl bridge from inspected source
train · proof
Keep seven wires, a reversible program inducing a computational-basis bijection E, and the inherited definition C as the chronological ordered product of emitted primitive-gate matrices (later gates multiply on the LEFT)…
local source supported
train · proof
A real planar rotation embedded over the complex numbers is the 2x2 matrix with top row (c, -s) and bottom row (s, c) for real scalars c and s. Prove that this matrix is unitary exactly when c^2 + s^2 = 1, by computing a…
local source supported
train · boundary
An amplitude-loading gate is built from a planar rotation through an angle t(x), where t is any fixed real-valued function of the real parameter x chosen so that on the interval -1 <= x <= 1 the cosine of t(x) equals x (…
nl bridge from inspected source
train · proof
A controlled family of operators is placed block-diagonally: for each control value k there is a block B_k acting on the same target space, and the full operator is the block-diagonal matrix whose k-th diagonal block is …
local source supported
train · proof
Suppose an operator on a finite register is unitary, and we relabel the register's basis by a bijection (reindexing both rows and columns through the same equivalence of index sets). Prove that the reindexed operator is …
local source supported
dev · proof
A state-preparation unitary acts only on a selector register, but inside a composite machine it is applied on the full product register coefficient x (selector x system) as identity-on-coefficient tensor (PREPARE tensor …
local source supported
train · proof
A coherently controlled SELECT applies, for each selector value s, a permutation p_s of the system register, while leaving the coefficient and selector registers fixed. Prove that the map sending (coeff, (s, x)) to (coef…
local source supported
test_public · proof
Finite basis permutations are represented by 0/1 matrices: for a bijection e of the index set, its matrix has a 1 at (row, column) exactly when row = e(column). Prove that composing two such permutation matrices multipli…
local source supported
dev · proof
On finite complex registers coefficient × (selector × system), write P_lift=I_coefficient tensor(PREPARE tensor I_system), A_lift for the selector/system-controlled coefficient-block family, and S_lift for the controlled…
local source supported
dev · concept
Retain the adapter's ten named oracle-call labels rather than matrix semantics, and the fact that executable SWAP semantics belong to a separate module. The historical question reports layout(system,signal,pureAncilla)=(…
nl bridge from inspected source
train · boundary
A fixed indicator oracle and its stated dagger are certified for a warm Robin instance by four facts bundled together: the dagger's matrix equals the oracle's own matrix; the integer image map of the oracle is self-inver…
nl bridge from inspected source