Start with dimensions, inner products, isometries and explicit conventions. The same foundations support state preparation, block encoding and later quantum-information arguments.
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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