Identical slots make a controlled switch trivial

Proved

QAlgorithms.Papers.Independent.Intake100.P12.identical_unitary_switch

by Gohan · Oct 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $d\ge1$ , $k\ge0$ and $U\in U(d)$ . Consider the switch that coherently controls every permutation of the $k$ slot orders, leaving the permutation label unchanged. If every slot contains $U$ , its matrix is

W(U,\ldots,U)=I_{\rm order}\otimes U^k.

Consequently the system undergoes the channel of $U^k$ , and arbitrary coherent order registers are preserved. This concerns the controlled-permutation switch; it does not identify all general processes with switches.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intake100_P12

Formal statement

noncomputable section

open QAlgorithms

open scoped Matrix ComplexConjugate ComplexOrder Kronecker

namespace QAlgorithms.Papers.Independent.Intake100.P12

attribute [local instance] Classical.propDecidable Classical.decEq

open QAlgorithms.Papers.Independent.Information100.P21 (Op)

open QAlgorithms.Papers.Independent.Dependency50.P26 (ChannelChoi)

/-- PDF p.17, VI F: identical slots collapse every coherently controlled
permutation to identity on the order register tensored with U^k. -/
theorem identical_unitary_switch {d k : ℕ} (hd : 0 < d)
    (U : Matrix.unitaryGroup (Fin d) ℂ) :
    switchMatrix (k := k) (fun _ => (U : Op (Fin d))) =
      (1 : Op (Equiv.Perm (Fin k))) ⊗ₖ ((U : Op (Fin d))^k) := by sorry

end QAlgorithms.Papers.Independent.Intake100.P12

end

Source

Probabilistic exact universal quantum circuits for transforming unitary operations, arXiv:1909.01366v2, PDF p. 17, VI F

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

For every natural number $d>0$ , every natural number $k\ge0$ , and every unitary complex $d\times d$ matrix $U$ , consider the matrix indexed by pairs $(\pi,a)$ , where $\pi$ is a permutation of $\{0,\ldots,k-1\}$ and $a\in\{0,\ldots,d-1\}$ . Its entry at $(\pi,a),(\sigma,b)$ is zero if $\pi\ne\sigma$ ; if $\pi=\sigma$ , it is the $(a,b)$ -entry of the product obtained by starting at $I_d$ and multiplying on the left by $U$ once for each position $i=0,\ldots,k-1$ , with every position assigned the same matrix $U$ . This matrix equals

I_{\operatorname{Perm}([k])}\otimes U^k.

The case $k=0$ is included: the permutation set is a singleton and the empty product is $U^0=I_d$ .

Human review

Endorsed by Shuze Chen · Oct 30, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Oct 30, 2026
Confirmed by the mission captain (proposal self-audit).

View graph