Matrix Constructions

Exercise LA-118

intermediate · 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

Basis states are bit strings; the control context is the non-target restriction
A single X action flips only the target wire

The selected plane fixes states outside the chosen context
Original derivation from inspected local source; no fresh Lean verification

Question

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. Prove that two basis states lie in the same control context if and only if they are equal or related by a single X action on the target wire.

Hint: mathematical route

Two basis states share a selected RY plane's control context if and only if they are equal or related by a single target-wire X, pinning the exact 2D pair the rotation can touch.

Reduce same-context to agreement on all non-target wires and split by target-bit equality.
Equal target bits give equal states; differing bits give a target-wire X relation.
Show a target X action preserves the non-target context (converse direction).
Relate this invariant pair to the fixed-column behavior of the selected plane.

Reference solution

The control context of a basis state is the restriction of its bit string to all wires other than the target. Two states share this context exactly when they agree on every non-target wire. Consider their target bits. If the two target bits are equal, then agreeing on all other wires plus agreeing on the target wire means the two full strings are identical, so the states are equal. If the two target bits differ, then they agree everywhere except the target wire, which is precisely the relation that one is obtained from the other by flipping the target bit, i.e. a single X action on the target wire; the non-target context is manifestly unchanged by flipping only the target bit. Conversely, equal states trivially share context, and a single target-wire X action changes only the target bit and leaves every other wire fixed, so it preserves the control context. Hence same context holds if and only if the states are equal or target-wire X-related. This pins down exactly the two-dimensional invariant subspace a selected rotation can touch, and is a statement about which basis pair is affected, not about implementation cost.

Assessment rubric

Define control context as the non-target restriction and split on target-bit equality (1 weight)
Equal target bits force equal states; differing bits give a single X relation (1 weight)
Converse: equality and target X both preserve the context (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
bit_eq_or_flip12-13; x_context15-19; same_context_iff21-37
Source SHA-256: 21bb92938d2d0d81341700123e66195fdebb12e72db7faf066a897479fe942ce · MIT (repository LICENSE)
QuantumBlockEncoding/SelectedRyPlane.lean
selectedRyPlaneMatrix_fixed_column122-129
Source SHA-256: 0098a9ef2bfc1af9eeaa44357b0818628084be35f88854232496e14d715c2f40 · MIT (repository LICENSE)

Contract: 35b365b0dc232dd1074d07bb182787f10b672bcc5abc792dc30b6067516eae46

Item digest: 0d08607d4fa98a7c4e6c2f3cef267a9b7e35329c0894b2c6272a11c823fe4ffd

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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