Track the represented operator, its normalizer and the accepted subspace. Keep preparation, SELECT, unprepare, workspace cleanup and resource tiers visible when composing constructions.
These links open the shared core's formal companion panel. Each card distinguishes admitted fixed-reference views from pending formalization. Preserve the exact core contract and split; a formal view is not another core.
train · proof · formal view pending
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 · formal view pending
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 · formal view pending
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 · formal view pending
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 · formal view pending
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 · formal view pending
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 · formal view pending
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 · formal view pending
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 · formal view pending
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 · formal view pending
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 · formal view pending
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 · formal view pending
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 · formal view pending
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