Wire Placement
Exercise LA-013
nl bridge from inspected source. Explicit question version 2 with distinct contract-change review; the predecessor question is not equivalent current gold. Core, family and split are retained. No new Lean verification is claimed for this NL view.
Assumptions and conventions
- Finite-dimensional complex Hilbert spaces unless real amplitudes are explicitly specified
- All basis/register permutations are fixed and applied to both input and output
- Column-vector action; Euclidean induced operator norm for norm claims
- Source inspection only; no fresh formal verification
This question explicitly revises its historical contract. A Lean companion must bind the current contract hash, not the predecessor hash. This is one reserved core, not two exercises.
Question
Let sigma be a bijection of the N physical wires, sigma:Fin N equiv Fin N. Its INDUCED bitstring bijection is R_sigma(b)(w)=b(sigma^{-1}(w)); define P by P|b>=|R_sigma(b)>. Thus P is specifically this wire-induced basis permutation, not an arbitrary permutation of all2^N computational labels. A primitive circuit has chronological matrices U_1,...,U_t, with first-listed gate acting first. Consistently rename each gate's target and each control by sigma, retaining gate kind and angle.
Prove that the renamed circuit realizes P(U_t...U_1)P^{-1}, rather than insertion of a one-sided physical permutation. Justify the single-gate conjugation from the induced bitstring action and show the interior inverse/permutation cancellations through the chronological product. Explain why output-only relabeling fails to preserve products, giving two identity stages and an actual nontrivial involutive wire swap as a witness when N>=2. Include empty circuit and N=0,1 boundaries. Finally assess why the same wire-renaming assertion would be false if P were an arbitrary unrelated basis-label permutation: on one wire compare P=X with a nonzero RY. Distinguish algebraic basis reindexing from a physical SWAP/routing implementation; no hardware routing cost follows for free.
Hint: mathematical route
Wire renaming induces one specific permutation of bitstring labels. Each renamed primitive is conjugated by that permutation, so chronological products telescope; arbitrary unrelated basis permutations are not generally wire renamings.
- The wire bijection induces a specific bitstring permutation, and the renamed gate is conjugated by its matrix P.
- Both input and output basis maps make interior P^{-1}P cancel through the chronological product, including the empty case.
- Output-only reindexing fails by an actual involutive wire-swap/identity-stage witness; unrelated basis-label permutations require a distinct operation.
Reference solution
For a bitstring b, R_sigma(b)(sigma(w))=b(w), so renaming the physical target/control wires transports their stored bits exactly. X flips the renamed target; RY/RZ act with the same2x2 matrix on that target with the same spectator context; CX tests the renamed control and flips the renamed distinct target. Hence each renamed primitive U'_j satisfies U'_j P=P U_j on every basis ket, and U'_j=P U_j P^{-1}. Equivalently its entry at(a,b) is U_j(a composed with sigma,b composed with sigma), matching the source matrix_apply formula. This per-gate statement uses the RELATION between sigma and P; it is not true for an unrelated P merely because P is a basis permutation.
Chronological evaluation multiplies later gates on the left. Therefore U'_t...U'_1=(P U_t P^{-1})...(P U_1 P^{-1})=P(U_t...U_1)P^{-1}, since every interior P^{-1}P cancels. The empty product isI and PIP^{-1}=I, so no extra stage is inserted. For N=0 or1 the wire-bijection group is trivial, P=I, and the theorem reduces to unchanged evaluation; those cases do not supply a nontrivial wire-swap example.
Output-only renaming would assign U_j the matrix P U_j. For two identity stages this gives P^2, while output-only reindexing of their composed identity givesP. At N=2 take sigma swapping the two wires, whose induced P sends|01> to|10> and vice versa, fixes|00>,|11>, is nontrivial and hasP^2=I. Thus P^2!=P, so one-sided reindexing is not multiplicative. For more wires the same swap with all others fixed works.
An arbitrary basis permutation still supports a valid ALGEBRAIC conjugation M->PMP^{-1}. It need not correspond to renaming wires gate-by-gate. On one wire the sole wire permutation is identity, so renaming leaves RY(theta) unchanged. The unrelated basis swapP=X instead obeys X RY(theta) X=RY(-theta) for the standard half-angle rotation [[cos(theta/2),-sin(theta/2)],[sin(theta/2),cos(theta/2)]]. At theta=pi/2 the off-diagonal signs differ, so RY(-theta)!=RY(theta). This refutes the original unrestricted reading without contradicting general matrix conjugation.
Both boundary label maps are representational: all input/output labels are consistently changed. This is not an assertion that an arbitrary basis permutation is implementable by physical wire swaps, or that routing on a fixed hardware graph is free. The source eval_gate/eval_circuit proofs certify the induced-wire primitive list under exact matrix semantics; static reading is not a new execution.
Assessment rubric
- Uses the actual wire-induced R_sigma and P, derives U'_j=P U_j P^{-1} with target/control roles and spectator context preserved, then cancels interior factors in chronological order. (1 weight)
- Gives the two-identity-stage output-only failure with an induced nontrivial involutive wire swap at N>=2, and handles empty circuit/N=0,1 without inventing a nontrivial wire permutation. (1 weight)
- Refutes the unrelated arbitrary-basis P reading on one wire using X RY(theta) X=RY(-theta), e.g.theta=pi/2, and distinguishes representation reindexing from physical SWAP/routing costs. (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/PrimitiveWireRename.lean
matrix_mul lines35-38; eval_gate83-109; eval_circuit111-118; module placement boundary
Source SHA-256:9f9b653ddda82a40bc9eafde31f6c932f59f631c03bfe24fbdc282acb8307727· MIT (repository LICENSE)
Contract: ae8929927ad4dffcc2d10d957b43dcf6354d24de5af0fbeff6d1277908c76635
Item digest: 8d4bf06a789c537652e35cf927f0aefd4e5a562d2fa585f1f16b501763a6b62e
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.
Question revision lineage
{ "question_version": 2, "predecessor_key": "qcb-core-la-013", "predecessor_item_digest": "f7dfea0e196e67a9b833837bf177bf9c36da072211cae75d84abed089fd87226", "predecessor_contract_hash": "9ee6494ba1c46bb565bbb37ed3e59665c616ad6633e47368efec9a3c722dccb7", "current_contract_hash": "ae8929927ad4dffcc2d10d957b43dcf6354d24de5af0fbeff6d1277908c76635", "changed_contract_fields": [ "question" ], "repair_record": "shared/repairs/la-013-wire-induced-permutation-successor.json", "repair_record_digest": "d6a2668fec88fe31956e2579b6a4b00e95906a46ef340cffc073562305bc627d", "review_record": "reports/textbook-v1/repairs/la-013-wire-induced-permutation-successor-review.json", "review_digest": "53968a2870d757838222a708d5a1079bdaa6c9f0a6cbf7b3d7f7dfa4593c1d55", "equivalence_to_predecessor_claimed": false, "additional_core_count": 0 }