Controlled-unitary content from folded eigenphases and its cost

Open

QAlgorithms.Papers.Independent.Intakethird100.P99.controlledUnitary_content_cost

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $H$ be a Hermitian Hamiltonian on two qubits $A,B$ , with canonical interaction coefficients $\alpha=(\alpha_1,\alpha_2,\alpha_3)$ satisfying $\alpha_1\ge\alpha_2\ge|\alpha_3|$ . Local terms in $H$ are allowed. Local unitary controls are instantaneous and free, interaction intervals are nonnegative, and $\hbar=1$ . Write $C_H(U)$ for the infimum of the interaction durations of protocols implementing the gate $U$ , allowing the ideal limit of arbitrarily fine pulses at fixed total duration and disregarding global phase. This cost is an extended nonnegative real, with value $+\infty$ for an impossible simulation. Let $W$ be any one-qubit unitary and $\mathrm{ctrl}\text{-}W=|0\rangle\langle0|\otimes I+|1\rangle\langle1|\otimes W$ . There exists a scalar $z$ of modulus one such that $zW$ has eigenvalues $e^{2ib},e^{-2ib}$ for some $0\le b\le\pi/2$ . For every such choice let $c=\min\{b,\pi/2-b\}$ . Assuming $\alpha_1>0$ ,

\beta(\mathrm{ctrl}\text{-}W)=(c,0,0),\qquad C_H(\mathrm{ctrl}\text{-}W)=\frac{c}{\alpha_1}.

The scalar phase of $W$ induces a free phase gate on the control. Folding the half-angle removes the branch ambiguity in the interaction content.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P99

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P99

open scoped Matrix Kronecker NNReal ENNReal

open QAlgorithms.Papers.Independent.Information100.P10 (pauli)

open QAlgorithms.Papers.Independent.Information100.P32 (evolution)

noncomputable section

/-- PDF pp.7,13, III.D.1 and Appendix A: after a free determinant phase, the eigenvalues
are exp(±2ib), 0≤b≤pi/2. The content coordinate is min(b,pi/2-b). -/
theorem controlledUnitary_content_cost (W : OneGate) (H : TwoMatrix) (a : Triple)
    (hH : HasCanonicalHamiltonian H a) (ha : 0 < a 0) :
    (∃ b : ℝ, ControlPhase (W : OneMatrix) b) ∧
    ∀ b : ℝ, ControlPhase (W : OneMatrix) b →
      HasContent (controlled (W : OneMatrix)) (controlledContent b) ∧
      interactionCost H (controlled (W : OneMatrix)) =
        ENNReal.ofReal (min b (Real.pi / 2 - b) / a 0) := by sorry

end

end QAlgorithms.Papers.Independent.Intakethird100.P99

Source

Characterization of non-local gates, arXiv:quant-ph/0205100v3, PDF p. 7, III.D.1 and Appendix A: controlled-U content and cost

Read-back

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

For every one-qubit unitary $W$ , complex two-qubit matrix $H$ , and real triple $a$ , assume $H=H^\dagger$ , $a_1\le a_0$ , $|a_2|\le a_1$ , $a_0>0$ , and there exist one-qubit unitaries $A,B$ and Hermitian one-qubit matrices $K,L$ such that

(A\otimes B)H(A\otimes B)^\dagger =\sum_{j=0}^2a_j\sigma_j\otimes\sigma_j+K\otimes I+I\otimes L, \qquad(\sigma_0,\sigma_1,\sigma_2)=(X,Y,Z).

There exists a real $b\in[0,\pi/2]$ for which some complex scalar $z$ , $|z|=1$ , satisfies

\operatorname{charpoly}(zW) =(x-e^{2ib})(x-e^{-2ib}).

For every real $b$ satisfying precisely this interval and characteristic-polynomial condition, put $d=(\min(b,\pi/2-b),0,0)$ . The controlled matrix $V$ , which acts as the identity on the target when the control bit is false and as $W$ when the control bit is true, is unitary, $d$ satisfies $d_1\le d_0$ , $|d_2|\le d_1$ , $d_0\le\pi/4$ , and there are four one-qubit unitaries $A',B',C',D'$ with $V=(A'\otimes B')\exp(-i\sum_jd_j\sigma_j\otimes\sigma_j)(C'\otimes D')$ . Its interaction cost satisfies

C_H(V)=\frac{\min(b,\pi/2-b)}{a_0}.

Here $C_H(V)$ is the extended nonnegative infimum, with empty infimum $+\infty$ , of times $t\ge0$ admitting arbitrarily accurate finite pulse simulation: for every $\varepsilon>0$ , one-qubit unitaries and nonnegative durations summing exactly to $t$ give a product $(A_m\otimes B_m)e^{-it_mH}\cdots(A_1\otimes B_1)e^{-it_1H}(A_0\otimes B_0)$ at operator-norm distance strictly less than $\varepsilon$ from $z'V$ for some $|z'|=1$ . Empty pulse lists are permitted, and the phase range includes $b=0$ and $b=\pi/2$ , where the displayed cost is zero.

Human review

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

View graph