Proof of Lemma 1, p. 5 — S†_i = S_i when the layer set is closed under adjoint

Proved

QCircMITM.Search.adjoint_layer_products

by mikedeng1 · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

circuit-depthp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1quantum-circuit-synthesis

Let $V \subseteq U(2^n)$ be a finite set of $n$ -qubit unitaries that is closed under adjoint ( $W \in V \Rightarrow W^\dagger \in V$ ), and let $S_i$ be the set of products of $i$ elements of $V$ ( $S_0 = \{I\}$ ). Then for every $i \ge 0$ and every unitary $U$ ,

U \in S_i^\dagger = \{\,X^\dagger : X \in S_i\,\} \iff U \in S_i ,

that is, $U^\dagger \in S_i$ if and only if $U$ can be implemented in depth $i$ .

This is the observation that opens the proof of Lemma 1. With $V = \mathcal V_{n,\mathcal G}$ the hypothesis on $V$ is the previous milestone.

Formalization Note. $V$ stands for $\mathcal V_{n,\mathcal G}$ ; the statement is made for every finite set of unitaries closed under inverse, which is all the paper's argument uses. In the unitary group $U^{-1} = U^\dagger$ .

Preamble

import Mathlib
import Definitions.Def_QCircMITM_Search_Algorithm

Formal statement

namespace QCircMITM.Search

theorem adjoint_layer_products {n : ℕ} (V : Finset (Unitary n)) (hV : ∀ W ∈ V, W⁻¹ ∈ V)
    (i : ℕ) (U : Unitary n) :
    U⁻¹ ∈ S V i ↔ U ∈ S V i := by sorry

end QCircMITM.Search

Source

Amy, Maslov, Mosca, Roetteler, A meet-in-the-middle algorithm for fast synthesis of depth-optimal quantum circuits, arXiv:1206.0758v3, p. 5, proof of Lemma 1

Human review

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

View graph