Matrix Constructions

Exercise LA-117

advanced · proof · train

local source supported. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.

Assumptions and conventions

A real SO matrix on 2^(q+1) indices; the adjacent pair differs by one Gray wire flip
Every non-target wire is a control; the target is the Gray-flip wire

Plane orders the pair numerically; the selected plane orders by target bit 0 then 1
Reversed ordering negates the RY half-angle
Original derivation from inspected local source; no fresh Lean verification

Question

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-flip wire of that adjacent pair, with every other wire a control. Prove that reindexing the adjacent plane matrix by the Gray labeling equals the selected two-level plane on that target wire, and explain how the half-angle sign depends on the target bit of the first index.

Hint: mathematical route

Reindexing an adjacent plane rotation by the Gray labeling equals a selected RY two-level plane on the Gray-flip wire; the half-angle is theta or -theta according to the first index's target bit, from the pair ordering.

Characterize the two reindexed-plane indices as the shared-context target-wire pair.
Match identity action off the control context entrywise.
On the context, reduce both sides to the real RY 2x2 block.
Track the pair ordering to get angle theta or -theta from the first index target bit.

Reference solution

Fix an adjacent pair (first, second) with second = X_target(first) in Gray labels. Reindexing the plane matrix by the Gray equivalence sends row/column named states back to their numerical indices. The plane rotates only the two indices first and second and fixes all others; under Gray labeling these two indices are exactly the two computational-basis states that share the same control context (all non-target bits equal) and differ only on the target wire, which is precisely the pair acted on by the selected RY plane with that chosen control context. For a named state outside this control context, both the reindexed plane and the selected plane act as the identity, matching entrywise. Inside the context, the 2x2 action is the real RY block; here the orientation matters: the plane's convention lists the pair by numerical order (first, then second), whereas the selected plane orders the pair by the target bit value 0 then 1. If the first index already has target bit 0 the orders agree and the angle is theta; if the first index has target bit 1 the two orderings are swapped, which conjugates the RY block by the bit-swap and is exactly the RY block at angle -theta. Hence the reindexed plane equals the selected plane at angle theta when the first target bit is 0 and at -theta otherwise. This matches a basis relabeling to a controlled rotation; it is a semantic correspondence, not a gate-count claim.

Assessment rubric

Identify the Gray pair as the shared-control-context two-level pair (1 weight)
Match identity action for states outside the control context (1 weight)
Explain the half-angle sign flip from first index target bit via pair ordering (1 weight)

Graph-grounded prerequisites

These are support/source anchors, not an automatically extracted theorem-dependency proof.

Download the shared core registry

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.

Read the Lean track and existing diagnostic warmups

Sources and provenance

QuantumBlockEncoding/GrayGivensCompiler.lean
same_context_iff21-37; edge_plane_transport54-86
Source SHA-256: 21bb92938d2d0d81341700123e66195fdebb12e72db7faf066a897479fe942ce · MIT (repository LICENSE)
QuantumBlockEncoding/SelectedRyPlane.lean
realRyPlaneBlock42-45; selectedRyPlaneMatrix58-66
Source SHA-256: 0098a9ef2bfc1af9eeaa44357b0818628084be35f88854232496e14d715c2f40 · MIT (repository LICENSE)

Contract: 37c45da4e70da73127157c132c951870dd5106003ca7b22ad3afa6e2c3a70695

Item digest: c187f71e1150c9fa98992c1dc15dbe5e22c6e35ff1be3cc2a8acccb8244daf96

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

Authored support steps: 4. This is not measured graph distance or model difficulty.