Abstract and conclusions: arbitrarily long-range two-point correlations

Open

QAlgorithms.Papers.Independent.Intakethird100.P57.arbitrarily_long_range

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

prove2quantum

For every $N\ge2$ , there are bond-one periodic tensors $A$ , admissible weighted graph data $\Phi$ , and local unitaries $V_k\in U(2)$ for which the RAGE raw vector $v$ is nonzero. Its normalization $\psi=v/\|v\|$ is a unit vector and has

\langle Z_1Z_N\rangle_\psi-\langle Z_1\rangle_\psi\langle Z_N\rangle_\psi=1.

Here $Z_k$ is the Pauli $Z$ operator on site $k$ , with eigenvalues $+1,-1$ on computational bits $0,1$ . The endpoints have chain distance $N-1$ . This is an existential expressiveness statement for arbitrarily large distances.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P57

Formal statement

noncomputable section

open scoped ComplexConjugate Matrix

namespace QAlgorithms.Papers.Independent.Intakethird100.P57

attribute [local instance] Classical.propDecidable

/-- Abstract PDF p.1 and conclusions p.4: correlations need not decay with separation.
A phase-π edge between the first and last sites and a Hadamard at one endpoint gives a Bell pair. -/
theorem arbitrarily_long_range (N : ℕ) (hN : 2 ≤ N) :
    ∃ (A : Tensors N 1) (G : PhaseGraph N) (V : Fin N → Matrix.unitaryGroup Bool ℂ),
      rage A G V ≠ 0 ∧ IsState (normalizeRageVector (rage A G V)) ∧
      connectedZ (normalizeRageVector (rage A G V)) ⟨0, by omega⟩ ⟨N - 1, by omega⟩ = 1 := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P57

end

Source

Renormalization algorithm with graph enhancement, arXiv:0802.1211v1, PDF p. 1, Abstract and conclusions: arbitrarily long-range two-point correlations

Read-back

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

For every natural number $N\ge2$ , there exist complex $1\times1$ matrices $A_k(t)$ for every site $k\in\{0,\ldots,N-1\}$ and bit $t$ , real weights $w_{k\ell}$ satisfying $w_{k\ell}=w_{\ell k}$ , $w_{kk}=0$ , and $0\le w_{k\ell}<2\pi$ , and unitary $2\times2$ complex matrices $V_k$ , such that the vector

r(b)= \sum_{c\in\{0,1\}^N} \left(\prod_{k=0}^{N-1}V_k(b_k,c_k)\right) \exp\!\left(\mathrm{i}\sum_{k<\ell}w_{k\ell}c_kc_\ell\right) \operatorname{tr}\!\left(A_0(c_0)\cdots A_{N-1}(c_{N-1})\right)

is nonzero, its normalization $u=\|r\|^{-1}r$ has Euclidean norm $1$ , and its two specified endpoint sites satisfy

\sum_b(-1)^{b_0+b_{N-1}}|u(b)|^2 - \left(\sum_b(-1)^{b_0}|u(b)|^2\right) \left(\sum_b(-1)^{b_{N-1}}|u(b)|^2\right) =1.

Here bits in exponents and products are interpreted as $0$ or $1$ , and the matrix product is ordered by increasing site index.

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