Exercise BE-110

A controlled SELECT (coeff,(s,x)) |-> (coeff,(s,p_s(x))) is a bijection with inverse applying (p_s)^{-1} under the same preserved selector s, hence unitary as a basis permutation; coherent control requires carrying the selector through for inversion.

1. Define F(coeff,(s,x)) = (coeff,(s,p_s(x))) and the candidate inverse G applying (p_s)^{-1} on the system.
2. G∘F = identity because (p_s)^{-1} undoes p_s under the preserved selector s.
3. F∘G = identity because p_s undoes (p_s)^{-1}, so F is a bijection.
4. The matrix of F is a basis permutation matrix, which is unitary over C.
5. The inverse must apply (p_s)^{-1} for the same preserved selector s; coherent control carries the selector through so the inverse re-reads the correct permutation.

Define F(coeff, (s, x)) = (coeff, (s, p_s(x))). Candidate inverse: G(coeff, (s, y)) = (coeff, (s, (p_s)^{-1}(y))). Check both composites. G(F(coeff,(s,x))) = G(coeff,(s,p_s(x))) = (coeff,(s,(p_s)^{-1}(p_s(x)))) = (coeff,(s,x)) since (p_s)^{-1} undoes p_s. F(G(coeff,(s,y))) = F(coeff,(s,(p_s)^{-1}(y))) = (coeff,(s,p_s((p_s)^{-1}(y)))) = (coeff,(s,y)). Both composites are the identity, so F is a bijection with inverse G. Its matrix is the permutation matrix of F (a 0/1 matrix with a single 1 per row and column), and every permutation matrix over C is unitary: its conjugate transpose is the permutation matrix of F^{-1}, and the product of a permutation matrix with its inverse is the identity. Hence SELECT is unitary purely because it is a basis permutation, with no amplitude arithmetic required. It is essential that G applies (p_s)^{-1} indexed by the SAME selector s: the selector is preserved by F, so on input the controlling value is s and the system permutation applied is p_s; to invert we must read that same preserved selector s and undo exactly p_s. If the inverse used a different selector's permutation p_{s'} the composite would apply p_s then (p_{s'})^{-1}, which is not the identity unless the permutations happen to coincide. Coherent control means the control register both selects which permutation acts and is itself carried through unchanged so the inverse can re-read it.

1. Exhibit the candidate inverse G applying (p_s)^{-1} on the system while preserving coefficient and selector (1 weight)
2. Verify both composites G∘F and F∘G are the identity, concluding F is a bijection (1 weight)
3. Conclude unitarity because the matrix is a basis permutation, and explain that the inverse must use the same preserved selector s so coherent control re-reads the correct permutation (1 weight)

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

• QuantumBlockEncoding/Robin/ComplexLCU.lean

  def controlledSystemEquiv (permutation : selector → system ≃ system) : LCUIndex coefficient selector system ≃ LCUIndex coefficient selector system where toFun index := (index.1, (index.2.1, permutation index.2.1 index.2.2)) invFun index := (index.1, (index.2.1, (permutation index.2.1).symm index.2.2)) left_inv index := by simp right_inv index := by simp (lines 315-327); theorem selectLift_unitary ... := equivPermutationMatrix_unitary _ (lines 340-349)

  Source SHA-256: aa51d33a6ca788b17879e1d88030b525f4f035c97d74588636ccf25f8c04b843 · MIT (repository LICENSE)

Contract: f58c46fe0545b797fbc05fe022a9413adb33d92606e70eb4f28cf219e27ab9cd

Item digest: 0cc5f51f216a0d5dbe1cc2aa09034b4fe15c07d1d632632b930ae11ec0505a4d

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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