Exercise BE-108

Same-bijection reindexing is a star-preserving algebra equivalence and preserves unitarity. Independent row/column bijections also preserve unitarity by two-sided unitary cancellation; what generally fails is using their fixed two-axis map as a unital multiplicative algebra equivalence.

1. Define R=T_e(O) by R[e(i),e(j)]=O[i,j], i.e. pullback along e^{-1} on both axes, with the same finite source/target bases.
2. For simultaneous reindexing, swapping matrix axes under adjoint leaves the same bijection on each axis, so T_e(O)†=T_e(O†).
3. The same-axis transformation preserves products by consistently relabeling the contracted index and is unital: T_e(A)T_e(B)=T_e(AB).
4. Apply the original O†O=I identity, same-map adjoint/product rules and T_e(I)=I to get R†R=I and hence finite-dimensional unitarity.
5. The same-bijection restriction belongs to this fixed-map algebra-equivalence proof, not a universal necessity for unitarity: independent-axis relabeling remains square/unitary as U_e O U_f†, while its same-map product/identity/adjoint rules can fail.

Let I,K be finite index sets, e:I->K a bijection, and O a complex unitary matrix on I. Write U_e for its basis-relabeling matrix, U_e[e(i),i]=1 and all other entries zero; it is a unitary map from C^I to C^K. Define T_e(A)=U_e A U_e†, so T_e(A)[e(i),e(j)]=A[i,j], equivalently T_e(A)[a,b]=A[e^{-1}(a),e^{-1}(b)]. This is the simultaneous pullback along e^{-1} on the two matrix axes.

Conjugate transpose commutes with this SAME-axis relabeling. Entrywise, T_e(A)†[a,b]=conjugate(A[e^{-1}(b),e^{-1}(a)])=T_e(A†)[a,b]; equivalently (U_e A U_e†)†=U_e A† U_e†. Multiplication also commutes: T_e(A)T_e(B)=U_e A(U_e†U_e)B U_e†=U_e AB U_e†=T_e(AB). In entries the contracted label z in K is replaced bijectively by e^{-1}(z) in I. Finally T_e(I_I)=I_K. Therefore T_e(O)† T_e(O)=T_e(O†)T_e(O)=T_e(O†O)=T_e(I_I)=I_K. The analogous reverse product is also I_K (or follows for square finite-dimensional isometries); hence the reindexed operator is unitary. This is exactly the same-map algebra-equivalence proof implemented by reindex_unitary.

The question's word 'essential' must be read with its explicit qualification 'for the argument': using the same bijection is what makes this single transformation T_e a unital star-algebra isomorphism between the two square-matrix algebras, commuting with adjoint. It is NOT a necessary condition for the resulting matrix to remain square or unitary. To see the boundary, consider arbitrary bijections e,f:I->K and the two-axis map T_{e,f}(A)=U_e A U_f†. It still gives a square K×K matrix. Its adjoint is T_{f,e}(A†), with the axes exchanged, rather than in general T_{e,f}(A†). Also T_{e,f}(A)T_{e,f}(B)=U_e A(U_f†U_e)B U_f†, which is generally not T_{e,f}(AB), and T_{e,f}(I)=U_e U_f† need not be I. Thus one cannot repeat the SAME fixed-map algebra-homomorphism proof when e differs from f.

Unitarity nevertheless survives by a different cancellation: R=U_e O U_f† implies R†R=U_f O†(U_e†U_e)O U_f†=U_f I_I U_f†=I_K, and RR†=I_K similarly. More generally the correctly matched transformation rule T_{e,f}(A)T_{f,g}(B)=T_{e,g}(AB) explains how the swapped axes in the adjoint give this cancellation. Consistent contracted indices are needed for composition; that does not require the output and input basis bijections to be equal in a general two-sided relabeling.

For an explicit two-dimensional counterexample to any stronger necessity claim, take O=I_2, e=identity and f=swap. Then U_e=I_2, U_f=X=[[0,1],[1,0]], and R=X is square and unitary despite e!=f. Here T_{e,f}(I)=X!=I and T_{e,f}(I)T_{e,f}(I)=I!=X=T_{e,f}(I*I), displaying failure of the one-map unital/product rules without failure of unitarity. Adjoint commutation with that same map can fail too: for Z=diag(1,-1), T_{e,f}(Z)=ZX has adjoint -ZX, whereas T_{e,f}(Z†)=ZX. In zero- or one-dimensional spaces the same-axis proof still holds; there may simply be no distinct bijections available to instantiate this two-dimensional boundary example.

These comparisons do not replace the original standing hypothesis: the requested proof remains the same-bijection theorem. They correct only an overstatement about why that proof works. The result is exact finite-dimensional complex algebra; it makes no primitive-circuit or finite-bit cost claim and does not by itself preserve a separately chosen clean projected block unless its register/clean basis identifications are transported consistently.

1. Defines simultaneous reindexing by T_e(A)[e(i),e(j)]=A[i,j] and states O†O=I and the goal T_e(O)†T_e(O)=I. (1 weight)
2. Proves same-axis adjoint commutation, multiplicativity and identity preservation, then uses these to prove unitarity (with finite square dimensions or both unitary identities understood). (1 weight)
3. Explains SAME is essential to this fixed-map algebra-equivalence proof, not to squareness or unitarity in general. Gives R=U_e O U_f† for independent axes and a valid cancellation/counterexample, explicitly rejecting the old 'not square-compatible' explanation without changing the standing same-axis theorem. (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 reindex_unitary {ι κ : Type*} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (equiv : ι ≃ κ) (operator : _root_.Matrix ι ι ℂ) (unitary : operator ∈ _root_.Matrix.unitaryGroup ι ℂ) : _root_.Matrix.reindexAlgEquiv ℂ ℂ equiv operator ∈ _root_.Matrix.unitaryGroup κ ℂ (lines 105-119)

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

Contract: 9d0c3c71f51d29071eb2ae9233bdbed5a785dbfdc336519086097ec5a8d4efa7

Item digest: 5eee24b8ce50209e2e4427318cd14e08055a01afadd92c2fbdd3e5aa2bb61e32

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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

{ "predecessor_item_digest": "a6acd83107961bd9360a0c2c55995f194064e1416340d73260285f5dbcb73c02", "predecessor_key": "qcb-core-be-108", "repair_record": "shared/repairs/be-108-reindex-isomorphism-boundary-repair.json", "repair_record_digest": "4c19bd5b346da36b690a62c8c64cb1293de7db96437a66becae0054e511a1e69", "review_record": "reports/textbook-v1/repairs/be-108-reindex-isomorphism-boundary-repair-review.json", "review_digest": "2ff580871e5f7433c15b32425921046217aa207b97600fc0622e36544df4076e" }