Watrous amplitude-product unitaries fail closure under composition and inverse

Proved

QAlgorithms.Papers.Independent.Intakethird100.P96.watrous_nonclosure

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

prove2quantum

Fix a cyclic binary chain of length $L\ge5$ and its computational basis. A matrix is of Watrous form if a single translation-invariant local amplitude function $u$ satisfies $W(a\mid b)=\prod_x u(a_x\mid b_{x+N})$ . Allow $N$ to be the whole ring, so this includes every smaller neighborhood. Let $H$ be the tensor product of single-qubit Hadamards, and let $P$ be the product of controlled-phase gates $\operatorname{diag}(1,1,1,-1)$ on all adjacent pairs. Then $H,P$ are unitary and

H,P\in\mathcal W_L,\qquad PH\notin\mathcal W_L,\qquad (PH)^*\in\mathcal W_L.

Here $\mathcal W_L$ denotes the matrices of Watrous form in this fixed basis. Thus composing two such unitaries can leave the class, and a member of the class can have its inverse outside it. The ring length is encoded as $L=5+e$ with $e\ge0$ .

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P96

Formal statement

noncomputable section

open scoped TensorProduct Kronecker BigOperators

namespace QAlgorithms.Papers.Independent.Intakethird100.P96

open QAlgorithms.Papers.Independent.Information100.P26 (Mat)

/-- §V.B, PDF pp.14--15: WQCA unitaries fail closure under product and inverse.
Phase pi and ring length at least five avoid the trivial short rings. -/
theorem watrous_nonclosure (extra : ℕ) :
    ringHadamard extra ∈ Matrix.unitaryGroup (RingConfiguration extra) ℂ ∧
    ringPhase extra ∈ Matrix.unitaryGroup (RingConfiguration extra) ℂ ∧
    IsWatrous extra (ringHadamard extra) ∧
    IsWatrous extra (ringPhase extra) ∧
    ¬ IsWatrous extra (ringPhase extra * ringHadamard extra) ∧
    IsWatrous extra (star (ringPhase extra * ringHadamard extra)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P96

end

Source

Reversible quantum cellular automata, arXiv:quant-ph/0405174v1, PDF p. 14, §V.B: Watrous-form unitaries are not closed under composition or inverse

Read-back

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

For every natural number $extra$ , put $L=extra+5$ and let $\mathcal C$ be the Boolean configurations on $\mathbb Z/L\mathbb Z$ . Define complex matrices indexed by $\mathcal C$ by

H_{a,b}=2^{-L/2}(-1)^{|\{x:a_x=b_x=\mathrm{true}\}|}, \qquad R_{a,b}= \begin{cases} (-1)^{|\{x:b_x=b_{x+1}=\mathrm{true}\}|},&a=b,\\ 0,&a\ne b, \end{cases}

where neighboring positions are interpreted modulo $L$ . Say that a matrix $M$ has the factorization property if there exists $u:\{\mathrm{false},\mathrm{true}\}\times\mathcal C\to\mathbb C$ such that $M_{a,b}=\prod_x u(a_x,(b_{x+k})_k)$ for all configurations $a,b$ , with position addition modulo $L$ and no further restrictions on $u$ . The assertion is that $H$ and $R$ are both unitary, each has this factorization property, their ordinary matrix product $RH$ does not have this property, and the conjugate transpose $(RH)^*$ does have this property. Each affirmative factorization may use its own function $u$ , and the assertion includes $extra=0$ , corresponding to five positions.

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