Exercise BE-111

Composition of basis-permutation matrices multiplies them in reverse order (second times first realizes first-then-second), because each column's single 1 collapses the product to function composition and left action forces the reversal.

1. Left multiplication by P(e) picks the single term at the inverse image: (P(e)*X)[r,c] = X[e^{-1}(r),c].
2. Setting X = P(first), e = second gives (P(second)*P(first))[r,c] = P(first)[second^{-1}(r),c].
3. This entry is 1 iff second^{-1}(r) = first(c), equivalently r = second(first(c)).
4. That is the matrix of the composite 'first then second', so P(second)*P(first) = P(first then second).
5. The order reversal is forced because left action means second*(first*v); any other order contradicts the inverse-image selection.

Let P(e) denote the permutation matrix of e, with P(e)[r,c] = 1 if r = e(c) else 0. Multiplying P(e) on the left of any operator applies e^{-1} to the row index: (P(e) * X)[r,c] = X[e^{-1}(r), c], because the matrix product sums over an intermediate index k the term P(e)[r,k] X[k,c], and P(e)[r,k] is nonzero (equal to 1) only at the single index k = e^{-1}(r). Now take X = P(first) and e = second: (P(second) * P(first))[r,c] = P(first)[second^{-1}(r), c] = 1 iff second^{-1}(r) = first(c), i.e. iff r = second(first(c)). That is exactly the condition defining P(first then second), the composite that applies 'first' and then 'second'. Hence P(second) * P(first) = P(first then second). The single surviving term is the heart of the computation: because each column of a permutation matrix has exactly one 1, the convolution sum over the contracted index collapses to one summand, turning matrix multiplication into function composition. The order reversal is forced, not conventional: a matrix acts on column vectors from the left, so applying 'first' then 'second' to a state means second*(first*v), and reading off the induced map on basis labels gives the composite in the order r = second(first(c)) with the matrices written right-to-left. Any other ordering would contradict how left multiplication selects the inverse-image row.

1. Establish that left multiplication by P(e) sends row index r to the single term at e^{-1}(r), because each column has exactly one 1 (1 weight)
2. Compute (P(second)*P(first))[r,c] = 1 iff r = second(first(c)), matching P(first then second) (1 weight)
3. Explain the order reversal is forced by left action on column vectors (second*(first*v)), not a free convention (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

  theorem equivPermutationMatrix_mul_apply (equiv : ι ≃ ι) (operator : _root_.Matrix ι κ ℂ) (row : ι) (column : κ) : (equivPermutationMatrix equiv * operator) row column = operator (equiv.symm row) column (lines 167-187); theorem equivPermutationMatrix_mul (first second : ι ≃ ι) : equivPermutationMatrix second * equivPermutationMatrix first = equivPermutationMatrix (first.trans second) (lines 206-223)

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

Contract: 330eae3b85a045c8741e4a59046edb32f4f5c72a6ee7540a2a73dd635addbadf

Item digest: 9b7764d055cff46ba40805e22a51db043464ec809fb8b49c72ab4ffd7bed969a

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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