Main properties (ii): one family has both exact translation invariance and volume-law entropy

Open

QAlgorithms.Papers.Independent.Intakethird100.P57.invariant_volume_law

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

prove2quantum

For every integer $L\ge1$ , there is a bond-one RAGE vector on $N=2L$ sites with normalized plus input, identity final rotations, and phase $\pi$ precisely on pairs of opposite sites of the cycle. Its symmetric graph weights lie in $[0,2\pi)$ . The vector $\psi$ is normalized and exactly cyclically invariant. For every cyclically contiguous block $B$ of length $0\le\ell\le L$ ,

T\psi=\psi,\qquad S(\rho_B)=\ell\ \text{bits}.

Here $\rho_B$ is the actual reduced density matrix of $\psi$ . This one explicit compatible family simultaneously realizes exact translation invariance and maximal volume-law block entropy, including wrapping blocks.

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

/-- PDF p.2, (i)–(ii): one family is simultaneously cyclically invariant and has maximal
volume-law entropy for every contiguous block of length at most half the chain. The compatible
circulant matching pins the source's existential claim; no external theorem is imported. -/
theorem invariant_volume_law (L : ℕ) (hL : 1 ≤ L) :
    ∃ G : PhaseGraph (2 * L), G.weight = oppositeWeights L ∧
      let v := rage (productTensors (plusFactors (2 * L))) G (fun _ => 1)
      IsState v ∧ CyclicInvariant v ∧
      (∀ (start : Fin (2 * L)) (ell : ℕ), ell ≤ L →
        IsDensityMatrix (rageMarginal v (cyclicBlock (2 * L) start ell)) ∧
        vnEntropy (rageMarginal v (cyclicBlock (2 * L) start ell)) = (ell : ℝ)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P57

end

Source

Renormalization algorithm with graph enhancement, arXiv:0802.1211v1, PDF p. 2, Main properties (ii): one family has both exact translation invariance and volume-law entropy

Read-back

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

For every natural number $L\ge1$ , there exists a graph $G$ on the indices $\{0,\ldots,2L-1\}$ whose real weights are symmetric, zero on the diagonal, nonnegative, and strictly less than $2\pi$ , and whose weights satisfy

w_{ij}= \begin{cases} \pi,&i\ne j\ \text{and}\ (i+L)\bmod(2L)=j,\\ 0,&\text{otherwise}. \end{cases}

For this graph, form the vector $v$ by taking one-dimensional tensor matrices with every entry $1/\sqrt2$ , multiplying their trace amplitudes by the graph phases, and applying identity matrices at all sites; explicitly, identifying Boolean values with $0,1$ , its amplitude at a bit string $b\in\{0,1\}^{2L}$ is

v_b=2^{-L}\exp\!\left(i\pi\sum_{r=0}^{L-1}b_r b_{r+L}\right).

The vector has Euclidean norm $1$ and satisfies $v_{(b_{(r+1)\bmod(2L)})_r}=v_b$ for every bit string $b$ . Moreover, for every starting index $s<2L$ and every natural number $\ell\le L$ , let $S=\{(s+t)\bmod(2L):0\le t<\ell\}$ . The matrix indexed by bit assignments $a,b$ on $S$ , with entries

\rho_{ab}=\frac{1}{\|v\|^2}\sum_{e\in\{0,1\}^{S^{\mathrm c}}} v_{a\cup e}\,\overline{v_{b\cup e}},

where $a\cup e$ combines the assignments on $S$ and its complement, is positive semidefinite and has trace $1$ . Its entropy is exactly $\ell$ : if its eigenvalues, counted with multiplicity, are $\lambda_r$ , then $-\sum_r\lambda_r\log_2\lambda_r=\ell$ , with $0\log_2 0=0$ . The assertion includes $\ell=0$ , when the retained set is empty and the entropy equals $0$ .

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