§III E–F, Eqs.(34)–(35): coherent relational-coordinate expansion

Open

QAlgorithms.Papers.Independent.Intakethird100.P67.relational_coordinates

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

prove2quantum

Fix normalized sample vectors, an anchor $\phi_a$ , a unit input $\psi$ , and a finite history $k_1,\ldots,k_T$ . Set $\psi_0=\psi$ and $\psi_{t+1}=R(k_{t+1})(I-|\phi_a\rangle\langle\phi_a|)\psi_t$ . With unary address $|t\rangle=|1\rangle^{\otimes t}|0\rangle^{\otimes(T-t)}$ , the actual ordered erasure unitary satisfies

W_T\cdots W_1(|\psi\rangle|-\rangle^{\otimes T})=|\phi_a\rangle\otimes\sum_{t=0}^{T-1}\langle\phi_a|\psi_t\rangle|t\rangle+|\psi_T\rangle\otimes|T\rangle.

Every coefficient is unchanged when the same unitary transforms the input, all samples and the anchor. The residual is retained at finite $T$ ; neither algebra generation nor a successful erasure assumption is needed for this exact expansion.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P67

Formal statement

noncomputable section

open scoped ComplexConjugate Matrix Matrix.Norms.L2Operator

attribute [local instance] Classical.propDecidable

open MeasureTheory Filter

namespace QAlgorithms.Papers.Independent.Intakethird100.P67

variable {I J K L A : Type*} [Fintype I] [DecidableEq I]
  [Fintype J] [DecidableEq J] [Fintype K] [DecidableEq K]
  [Fintype L] [DecidableEq L] [Fintype A] [DecidableEq A]

/-- PDF pp.8–9, Eqs.(34)–(35): complete coherent expansion and simultaneous-unitary
invariance of its coordinates, including transformation of the anchor. -/
theorem relational_coordinates (phi : K → EuclideanSpace ℂ I) (a : K)
    (hphi : ∀ k, IsState (phi k)) (T : ℕ) (h : Fin T → K)
    (psi : EuclideanSpace ℂ I) (hpsi : IsState psi) :
    act (historyUnitary (erasureGate phi a) h) (tensorVec psi (minusRegister T)) =
      coordinateExpansion phi a h psi ∧
    (∀ (U : Matrix.unitaryGroup I ℂ) (t : ℕ),
      inner ℂ (act (U : Matrix I I ℂ) (phi a))
        (residual (fun k => act (U : Matrix I I ℂ) (phi k)) a (act (U : Matrix I I ℂ) psi)
          ((List.ofFn h).take t)) =
      inner ℂ (phi a) (residual phi a psi ((List.ofFn h).take t))) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P67

end

Source

Universal Quantum Emulator, arXiv:1606.02734v2, PDF p. 8, §III E–F, Eqs.(34)–(35): coherent relational-coordinate expansion

Read-back

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

Let $I,K$ be finite index types with decidable equality, let $\phi_k\in\mathbb C^I$ have norm $1$ for every $k\in K$ , fix $a\in K$ , and let $\psi\in\mathbb C^I$ have norm $1$ . Let $T$ be any natural number and $h:\{0,\ldots,T-1\}\to K$ any history. Put $P=\phi_a\phi_a^\dagger$ , $R_k=1-2\phi_k\phi_k^\dagger$ , $C(V)=1_I\otimes|0\rangle\langle0|+V\otimes|1\rangle\langle1|$ , $H=2^{-1/2}\begin{pmatrix}1&1\\1&-1\end{pmatrix}$ , and $E_k=C(R_k)(1_I\otimes H)C(R_a)$ . Let $V_h=E_{h_{T-1}}^{(T-1)}\cdots E_{h_0}^{(0)}$ , with the $j$ -th factor acting on the system and ancilla $j$ , and let $\eta_T=((|0\rangle-|1\rangle)/\sqrt2)^{\otimes T}$ . Define residual vectors by $r_0=\psi$ and $r_{s+1}=R_{h_s}(1-P)r_s$ for $s<T$ , and define the bit string $u_t$ by $(u_t)_j=\mathrm{true}$ exactly when $j<t$ . Then

V_h(\psi\otimes\eta_T) = \sum_{t=0}^{T-1}\langle\phi_a,r_t\rangle\, \phi_a\otimes|u_t\rangle +r_T\otimes|u_T\rangle.

Furthermore, for every unitary $U$ on $\mathbb C^I$ and every natural number $t$ , let $s=\min(t,T)$ and form $\widetilde r_s$ from $U\psi$ and the first $s$ history entries by replacing every $\phi_k$ in the residual recursion with $U\phi_k$ ; then $\langle U\phi_a,\widetilde r_s\rangle=\langle\phi_a,r_s\rangle$ . Thus $t$ is not required to be at most $T$ : taking a prefix longer than the history uses the whole history. The case $T=0$ is included, with an empty sum, identity history operator, and the unique empty bit string.

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