Matrix Constructions
Exercise LA-116
local source supported. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.
Assumptions and conventions
- Finite real matrix indexed by width-(q+1) labels; a fixed label/index bijection
- The same bijection relabels rows and columns
- Symmetric reindexing is an algebra equivalence on matrices preserving multiplication and the identity
- Original derivation from inspected local source; no fresh Lean verification
Question
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 (the same bijection on each side). Prove that this relabeling preserves orthogonality, i.e. if A^T A = I then the Gray-coordinate matrix is again orthogonal, and that it preserves the determinant exactly. Identify precisely why using the same bijection on rows and columns is essential.
Hint: mathematical route
Symmetric Gray-coordinate relabeling of a matrix preserves orthogonality and the determinant exactly, because one shared row/column bijection makes it a multiplicative identity-fixing reindexing.
- Describe symmetric relabeling as a multiplicative, identity-fixing reindexing map.
- Apply the map to A^T A = I and use transpose compatibility to get orthogonality.
- Conclude the determinant is unchanged under the symmetric relabeling.
- Explain that one shared bijection is required for multiplicativity and sign-free determinant.
Reference solution
The symmetric relabeling is the reindexing map that sends a matrix A to the matrix whose (i,j) entry is A at the labels corresponding to i and j under the fixed bijection. Because the same bijection is applied to rows and to columns, this map is multiplicative: the reindexing of a product equals the product of the reindexings, since the internal summation index of matrix multiplication is itself relabeled consistently and a bijective reindexing of a finite sum does not change its value. It also sends the identity matrix to the identity, because the identity's entries depend only on whether the two labels coincide, a property preserved by any bijection applied equally to both sides. Orthogonality: apply the reindexing to the hypothesis A^T A = I. Transpose commutes with symmetric relabeling (swapping row and column roles is unaffected by using one bijection on both), so reindex(A)^T reindex(A) = reindex(A^T A) = reindex(I) = I. Hence the Gray-coordinate matrix is orthogonal. Determinant: a symmetric reindexing is a similarity-type conjugation by a permutation, and the determinant is invariant under relabeling both axes by the same permutation, so det is unchanged exactly. The same-bijection requirement is essential: if rows and columns were relabeled by different bijections, the map would not respect multiplication (the shared summation index would be split), transpose would not commute with it, and the determinant could pick up a relative permutation sign. Thus using one bijection on both axes is exactly what makes relabeling an algebra isomorphism preserving these invariants. This is an exact transport fact, not a numerical change of basis cost.
Assessment rubric
- State that symmetric relabeling is multiplicative and fixes the identity (1 weight)
- Derive orthogonality by applying the relabeling to A^T A = I, using transpose compatibility (1 weight)
- Argue determinant invariance and explain why one shared bijection is essential (1 weight)
Graph-grounded prerequisites
These are support/source anchors, not an automatically extracted theorem-dependency proof.
Lean view and evidence boundary
No aligned Lean view has been admitted for this native core in this textbook checkpoint. This is not a claim that the underlying mathematics lacks a formal proof. Contributions must preserve this exact target contract and split.
Sources and provenance
- QuantumBlockEncoding/GrayGivensCompiler.lean
grayCoordinates159-162; grayCoordinates_orthogonal169-175; grayCoordinates_det177-180
Source SHA-256:21bb92938d2d0d81341700123e66195fdebb12e72db7faf066a897479fe942ce· MIT (repository LICENSE)
Contract: a3493ab8c01c291a12369dc92e326e4813083e68c542d1912e2d4ce520abb40b
Item digest: e13c0d1bd06158bd627632029146044c6323a71aaaf22ded1d505d62b6f8e2e2
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 4. This is not measured graph distance or model difficulty.