QuantumComputinglib learn · inspect · formalize
Checked on this commit 4,524 public declarations commit 4e2c5b2c0be5 Build record

Shared mathematical foundations / Wire Placement

Wire Placement

Exercise LA-014

intermediate · concept · test_public

nl bridge from inspected source. Current content-bound mathematical second pass accepted. 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

Question

A circuit uses only single-qubit rotations, bit flips and controlled bit flips. A bijection relabels all physical wires, preserving which wire controls which target. Which of total instruction count, rotation count and controlled-bit-flip count must stay unchanged? Does this alone prove equal nearest-neighbor routing cost on fixed hardware?

Hint: mathematical route

A circuit uses only single-qubit rotations, bit flips and controlled bit flips. A bijection relabels all physical wires, preserving which wire controls which target. Which of total instruction count, rotation count and controlled-bit-flip count must stay unchanged? Does this alone prove equal nearest-neighbor routing cost on fixed hardware?

  1. Wire renaming maps each instruction to the same instruction kind.
  2. Count positions of each kind to preserve all logical counts.
  3. Fixed hardware distance is outside this semantic bijection.
Reference solution

All three logical counts stay unchanged: map each instruction to the same kind with relabeled target/control, so there is a one-to-one position-preserving correspondence of lists. Counting all positions, rotation positions or controlled-bit-flip positions therefore yields equal counts. Hardware routing cost need not stay unchanged because the permutation can map an adjacent control-target pair to a distant pair while the hardware graph is fixed. Equal logical counts are a semantic placement invariant, not an assumption that connectivity or physical SWAP overhead is free.

Assessment rubric
  1. All three logical counts invariant (1 weight)
  2. Preserve control-target roles (1 weight)
  3. No inferred physical routing equality (1 weight)

Graph-grounded prerequisites

These are support/source anchors, not an automatically extracted theorem-dependency proof.

Download the shared core registry

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.

Read the Lean track and existing diagnostic warmups

Sources and provenance

Contract: f95717a058c12722f9dbbcc46334fe7fe005f966843bf85b6b01824e03392e54

Item digest: cc4258a0f2ab565d82b3abe29fb1f7cbd0112c16d5ad88e0b35d780ac7c0bdd1

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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