QuantumComputinglib learn · inspect · formalize
Checked on this commit 4,524 public declarations commit 4e2c5b2c0be5 Build record

QuantumComputingBench · graph-grounded exercise book

Matrix Constructions

Start with dimensions, inner products, isometries and explicit conventions. The same foundations support state preparation, block encoding and later quantum-information arguments.

Back to Shared mathematical foundations

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.

test_public · proof · formal view pending

Exercise LA-101

A planar rotation acts on two rows by the half-angle convention: the first row becomes cos(t/2)*x - sin(t/2)*y and the second becomes sin(t/2)*x + cos(t/2)*y, where (x,y) are the two entries in some column. Choosing the …

local source supported

test_public · proof · aligned Lean reference checked

Exercise LA-102

Replacing two distinct rows i and j of a square matrix by the linear mixtures (a*row_i + b*row_j) and (c*row_i + d*row_j) multiplies the determinant by (a*d - b*c). Use this to prove that a plane rotation acting on rows …

local source supported

dev · proof · formal view pending

Exercise LA-103

A sequence of plane rotations is applied to a matrix in chronological order (the first listed rotation acts first). Prove that reversing the list and negating every rotation angle undoes the whole sequence exactly, retur…

local source supported

test_public · proof · formal view pending

Exercise LA-104

A column is cleared by a bottom-up sweep: starting from a low index, adjacent rows are rotated upward one pair at a time so that each lower entry is folded into the one above it. Prove that after sweeping the window of r…

local source supported

train · proof · formal view pending

Exercise LA-105

Let B have orthonormal columns (B^T B = I) and suppose one column c of B is supported only on its diagonal row, i.e. every entry of column c off that row is zero. Prove that the diagonal entry B[c,c] squares to 1. If in …

local source supported

train · proof · formal view pending

Exercise LA-106

Suppose a real NxN matrix A is orthogonal (A^T A = I), has determinant 1, and its first N-1 columns have already been reduced to the standard identity prefix (column c equals the c-th coordinate vector for every c < N-1 …

local source supported

train · proof · formal view pending

Exercise LA-107

A width-n binary-reflected Gray labeling assigns to each index in 0..2^n-1 a computational-basis string, little-endian, with the recursion that index 2*q+b carries head bit (b xor (q mod 2)) over the Gray label of q. Pro…

local source supported

train · proof · formal view pending

Exercise LA-108

A rectangular NxM real matrix A is reduced to an upper-trapezoidal residual by accumulating plane rotations into a single orthogonal transform matrix T, so that T*A equals the residual. Prove that T^T times the residual …

local source supported

train · proof · formal view pending

Exercise LA-109

A finite matrix-product chain of width-D cores produces an amplitude for a bit string by chronological matrix contraction, with a fixed left boundary vector of length D. Contracting that left boundary into the first core…

local source supported

train · proof · formal view pending

Exercise LA-110

In a matrix-product chain with width-D cores and a fixed right boundary vector of length D, define the readout of a bit string as the chronological matrix-vector product that starts from the right boundary and applies ea…

local source supported

test_public · boundary · formal view pending

Exercise LA-111

A matrix-product chain stores dense local cores; the number of stored scalars sums 2*l*m across cores, where l and m are the left and right bond dimensions of each core. Given that every bond of the chain is at most D an…

local source supported

train · proof · formal view pending

Exercise LA-112

A rectangular NxM real matrix is reduced column by column: at column k, if a pivot row exists, a bottom-up adjacent sweep clears that column below the diagonal. Say a matrix has the upper-prefix property at index k when,…

local source supported

train · proof · formal view pending

Exercise LA-114

A greedy swap process extends a finite injection e from r original indices into N physical positions: starting from the identity permutation, at stage k it swaps the current image of index k with the target e(k). Prove t…

local source supported

train · proof · formal view pending

Exercise LA-115

An orthogonal matrix U is reoriented to have determinant 1 by multiplying it with a sign-flip on a single designated unused column exactly when U already has the wrong sign; the choice is made by the parity (sign) of an …

local source supported

train · boundary · formal view pending

Exercise LA-116

A real matrix indexed by width-(q+1) computational-basis labels is converted to Gray coordinates by relabeling both its rows and its columns through a fixed bijection between labels and the numerical indices 0..2^(q+1)-1…

local source supported

train · proof · formal view pending

Exercise LA-117

A real SO matrix on 2^(q+1) Gray-ordered indices is compiled to a circuit by first decomposing it into adjacent plane rotations, then realizing each plane as a selected RY rotation whose target wire is the single Gray-fl…

local source supported

train · proof · formal view pending

Exercise LA-118

A selected RY plane fixes every computational-basis vector whose control context differs from the chosen one, and acts as a 2x2 real rotation on the single pair sharing the chosen context and differing on the target bit.…

local source supported

dev · counterexample · formal view pending

Exercise LA-119

A selected RY rotation with c controls uses exactly 2^c RY gates and 2*(2^c - 1) CX gates per selected rotation and makes zero oracle calls. A reader claims that because a general real SO matrix on these wires is realize…

nl bridge from inspected source

dev · proof · formal view pending

Exercise LA-120

A list of plane rotations can be applied to a matrix in two ways. The step-by-step action takes the list and the matrix and applies the first listed rotation to the matrix, then the next to the result, and so on. Alterna…

local source supported