Matrix Constructions
Exercise LA-107
local source supported. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.
Assumptions and conventions
- Little-endian primitive basis strings of a fixed width
- Gray recursion: head of 2*q+b is b xor (q mod 2) over the Gray label of q
- A single X action flips exactly one chosen wire of the basis string
- Original derivation from inspected local source; no fresh Lean verification
Question
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. Prove that two numerically consecutive indices (second = first + 1) carry labels that differ in exactly one physical bit, i.e. the second label is obtained from the first by a single X action on one wire.
Hint: mathematical route
Consecutive binary-reflected Gray indices differ by exactly one physical wire flip, proved by width induction with parity-split head/tail casework.
- Reduce to width induction and split on the parity of the first index.
- Even first index: tail unchanged, head bit toggles.
- Odd first index: head bit unchanged, tail quotient advances.
- Lift the inductive single-wire flip of the tail to the full string.
Reference solution
Induct on the width n. For n=0 there are no two distinct indices, so the claim is vacuous. For width n+1 write first = 2*q + b. There are two cases by the parity of first. If first is even (b=0), then first+1 = 2*q+1 shares the same tail q, so the Gray tails coincide and only the head bit can change; the head recursion gives head(first+1) = flip(head(first)) because the tail q is unchanged and the stored head toggles, so exactly the head wire flips. If first is odd (b=1), then first+1 = 2*(q+1), the head bit is governed by the parity of the quotient and stays equal while the tail advances from q to q+1; applying the induction hypothesis to the tail yields a single flipped wire there, and lifting that wire through the tail embedding gives one physical X action on the full string. In both cases exactly one wire changes, and the explicit head-parity lemmas certify which. This is a statement about which single basis relabeling realizes the step, not a gate-cost estimate.
Assessment rubric
- Set up induction on width with the correct even/odd split on the first index (1 weight)
- Even case: tail fixed, head toggles via the head-parity lemma (1 weight)
- Odd case: head fixed, tail advances and the induction hypothesis gives one flipped wire (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/GrayBasis.lean
equiv15-22; headBit_even37-42; headBit_odd44-52; adjacent54-94
Source SHA-256:658e01d906fc1ed4dd12983ae62c1a45f5639a9d0cbff35c825db9b78445d3db· MIT (repository LICENSE)
Contract: 6b63716fa9ca0e18880cdc0f230ca156fcf550e0aed43dc735d9091f26d7748f
Item digest: 87706ea5c66f54bf0bffd4b1d4fcaab38075224230201e30e5d530af8ae448e2
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 4. This is not measured graph distance or model difficulty.