Main properties (i): arbitrary block entropy, including maximal volume law

Open

QAlgorithms.Papers.Independent.Intakethird100.P57.arbitrary_block_entropy

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

prove2quantum

Let $N\ge1$ , $0\le L\le N$ , and let $h$ be any real number satisfying $0\le h\le\min(L,N-L)$ . There exist bond-one RAGE data with nonzero raw vector $v$ such that $v/\|v\|$ is a pure state and its reduced density matrix $\rho_L$ on the first $L$ sites satisfies

S(\rho_L)=-\operatorname{tr}(\rho_L\log_2\rho_L)=h.

Thus every admissible entropy value, including the maximal value $\min(L,N-L)$ bits, occurs within this family. Empty and whole-chain blocks have entropy zero. For $L\le N/2$ , the maximal entropy is exactly $L$ bits, giving a volume law. The entropy unit is bits, with $0\log_2 0=0$ .

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 p.1 and Main properties (i), p.2: all entropy values up to the maximal
bipartite value occur already at D=1. Entropy is measured in bits. -/
theorem arbitrary_block_entropy (N L : ℕ) (hN : 1 ≤ N) (hL : L ≤ N)
    (h : ℝ) (hlo : 0 ≤ h) (hhi : h ≤ (min L (N - L) : ℕ)) :
    ∃ (A : Tensors N 1) (G : PhaseGraph N) (V : Fin N → Matrix.unitaryGroup Bool ℂ),
      rage A G V ≠ 0 ∧ IsState (normalizeRageVector (rage A G V)) ∧
      IsDensityMatrix (rageMarginal (rage A G V) (firstBlock N L)) ∧
      vnEntropy (rageMarginal (rage A G V) (firstBlock N L)) = h := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P57

end

Source

Renormalization algorithm with graph enhancement, arXiv:0802.1211v1, PDF p. 1, Main properties (i): arbitrary block entropy, including maximal volume law

Read-back

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

For all natural numbers $N,L$ with $N\ge1$ and $L\le N$ , and every real number $h$ satisfying $0\le h\le\min(L,N-L)$ , there exist complex $1\times1$ matrices $A_k(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$ matrices $V_k$ , where $k,\ell\in\{0,\ldots,N-1\}$ and $t\in\{0,1\}$ , such that

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 and $\|\|r\|^{-1}r\|=1$ . For $S=\{0,\ldots,L-1\}$ , define a matrix indexed by bit assignments $a,b$ on $S$ by

\rho_{a,b} = \frac{1}{\|r\|^2} \sum_{e\in\{0,1\}^{S^c}} r(a\cup e)\,\overline{r(b\cup e)},

where $a\cup e$ denotes the full bit string with restrictions $a$ and $e$ . This matrix is positive semidefinite, has trace $1$ , and satisfies

-\operatorname{Re}\operatorname{tr}\bigl(f(\rho)\bigr)=h, \qquad f(x)=x\log_2x,

where $f(\rho)$ is defined by continuous functional calculus and $f(0)=0$ . All matrix products defining $r$ use increasing site order. The permitted cases $L=0$ and $L=N$ force $h=0$ ; when $L=0$ , the matrix $\rho$ has its single row and column indexed by the empty bit assignment.

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