Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -7,19 +7,19 @@ import TNLean.MPS.ParentHamiltonian.BNTBlockDiagonalCrossingTrace
/-!
# Boundary-condition comparisons for block-diagonal parent spaces

The word-indexed comparison from arXiv:quant-ph/0608197
The boundary-crossing comparison from arXiv:quant-ph/0608197
\[
A^j_\beta C^j_{i,\rho}
=
\bigl((\mu_j^NX_j)A^j_\beta\bigr)A^j_\rho
\]
is the local boundary-crossing coordinate form of the \(C^j,D^j\) trace
is the cut-adapted boundary-crossing form of the \(C^j,D^j\) trace
comparison from arXiv:quant-ph/0608197, Theorem 12, proof lines 1446--1451,
after specializing \(D^j_\beta\) to \((\mu_j^N X_j)A^j_\beta\). The normalized
\(E^j\)-calculation then implies the periodic-boundary single-block constraints
and the finite-range block-diagonal periodic-boundary equality used here.

The source proof writes this comparison with site-indexed matrices
The source proof writes this comparison with boundary-indexed matrices
\(C^j_{i_1}\), \(D^j_{i_{m+1}}\), and the derived matrix \(E^j\). The words
\(\beta\) and \(\rho\) below are cut-adapted coordinates for the same
periodic-boundary comparison, not additional source terminology.
Expand All @@ -36,7 +36,7 @@ boundary representation to periodic single-block states.

Under the normalized BNT hypotheses, every vector in the block-diagonal
periodic-boundary ground space has block-diagonal boundary conditions \(X_j\). If those
same boundary conditions satisfy the source comparison, in the word-indexed
same boundary conditions satisfy the source comparison, in the cut-adapted
boundary-crossing form
\[
A^j_\beta C^j_{i,\rho}
Expand Down Expand Up @@ -119,7 +119,7 @@ single-block states.
Assume the vector \(\psi\in\mathcal G_{N,L}(\oplus_j\mu_jA_j)\) has already
been written with block-diagonal boundary matrices \(X_j\). If every
boundary-crossing interval has the simultaneous block-word spanning property,
then the local constraint produces the word-indexed \(C^j,D^j\) comparison,
then the local constraint produces the cut-adapted \(C^j,D^j\) comparison,
and the normalized \(E^j\)-calculation gives
\[
\Gamma_N^{A_j}(\mu_j^NX_j)\in\mathcal G_{N,L}(A_j).
Expand Down Expand Up @@ -433,16 +433,16 @@ theorem chainGroundSpace_toTensorFromBlocks_eq_iSup_of_crossing_pgvwc_comparison
periodic-boundary equality in the finite BNT range.

This theorem assumes the source \(C^j,D^j\) comparison only up to the
word-indexed matrix identity
cut-adapted matrix identity
\[
A^j_\beta C^j_{i,\rho}
=
\bigl((\mu_j^NX_j)A^j_\beta\bigr)A^j_\rho
\]
for every boundary-crossing interval, local word \(\beta\) before the cut,
and outside word \(\rho\), with \(D^j_\beta\) already specialized to
\((\mu_j^NX_j)A^j_\beta\). The words \(\beta\) and \(\rho\) are formal
word coordinates for the opened boundary comparison; they reindex the source
\((\mu_j^NX_j)A^j_\beta\). The words \(\beta\) and \(\rho\) are
cut-adapted coordinates for the opened boundary comparison; they reindex the source
end-site comparison by blocked words rather than replacing the source indices.
The normalized \(E^j\)-calculation
and the block-injective crossing-window argument then give the
Expand Down Expand Up @@ -518,7 +518,7 @@ the equality conclusion
=
\bigvee_j\mathcal G_{N,L}(A_j),
\]
under the assumed word-indexed \(C^j,D^j\) comparison.
under the assumed cut-adapted \(C^j,D^j\) comparison.

**Scope restriction (length-\(L_0\) injectivity range):** Theorem 12 of
arXiv:quant-ph/0608197 assumes \(L\ge 3(b-1)(L_0+1)+1\). This theorem is stated in the current BNT
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -12,15 +12,14 @@ \subsection{Periodic-boundary ground space for a block-diagonal tensor}
comparison in the periodic ring. The source proof
\cite{PerezGarcia2007Matrix} writes this comparison with $C^j_{i_1}$,
$D^j_{i_{m+1}}$, and the normalized matrix $E^j$; the symbols $\beta$ and
$\rho$ below are formal word variables introduced after opening the periodic
cut, not additional terminology from the paper. In these
coordinates the source comparison becomes
$\rho$ below are the cut-adapted words obtained after opening the periodic
cut. In these coordinates the source comparison becomes
\[
A^j_\beta C^j_{i,\rho}
=
\bigl(\mu_j^N X_j A^j_\beta\bigr)A^j_\rho,
\]
which is the formal word-coordinate counterpart of
which is the blocked-word form of
$A^j_{i_{m+1}}C^j_{i_1}=D^j_{i_{m+1}}A^j_{i_1}$ with
$D^j_\beta=(\mu_j^NX_j)A^j_\beta$.

Expand Down Expand Up @@ -385,7 +384,7 @@ \subsection{Periodic-boundary ground space for a block-diagonal tensor}
\]
and the $N$-site ground spaces $G_N(A_j)=\mathcal G_{N,N}(A_j)$
have internal sum.
The present formal statement is the equality-level consequence of the
The present statement is the equality-level consequence of the
boundary-condition comparison in
\cite[Theorem~12, proof lines~1436--1451]{PerezGarcia2007Matrix} in the
length-$L_0$ injectivity range
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -244,7 +244,7 @@ \section{The remaining boundary condition}
block-diagonal boundary matrices whose block components again belong to the
blockwise periodic-boundary spaces.

The present formal boundary isolates the remaining source comparison in local
The present boundary isolates the remaining source comparison in cut-adapted
coordinates for boundary-crossing windows. Suppose
\begin{align}
\psi
Expand All @@ -255,7 +255,7 @@ \section{The remaining boundary condition}
For a cyclic interval beginning at \(i\) and crossing the boundary cut, put
\(a=i+L-N\). The word \(\beta\) records the part of the interval before the
chosen cut, while \(\rho\) records the outside word of length \(N-L\). These
are local coordinates for the proof, not names used in the source statement.
are the blocked words obtained by opening the source boundary-index comparison.
The conditional theorem assumes that, for every block \(j\) and every such
outside word \(\rho\), there is a matrix \(E_{j,i,\rho}\) such that for every
word \(\beta\) of length \(a\),
Expand Down Expand Up @@ -283,7 +283,7 @@ \section{The remaining boundary condition}
\leanid{MPSTensor.chainGroundSpace_toTensorFromBlocks_eq_iSup_and_iSupIndep_of_complementary_identities}.}

The live blueprint records that larger source statement with explicit citations
and separately marks the local cut coordinates used by the formalization,
and separates the cut-adapted coordinates from the paper's boundary indices,
without claiming that the source statement is proved.\footnote{Blueprint locations:
\path{def:parent_hamiltonian_ground_space_bnt} for the block-diagonal
periodic-boundary ground space,
Expand Down Expand Up @@ -495,7 +495,7 @@ \section{Conclusion}
and
\leanid{MPSTensor.chainGroundSpace_toTensorFromBlocks_eq_iSup_and_iSupIndep_of_trace_decomposition_bnt_c1_span}.}

The word-indexed \(C^j,D^j\) route is closer to the proof of
The cut-adapted \(C^j,D^j\) route is closer to the proof of
\cite[Theorem~12]{PerezGarcia2007MPSReps}.
The words \(\beta\) and \(\rho\) are local word coordinates introduced after

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Incomplete terminology pass. This PR replaces the "formal word"/"word-indexed"/"local coordinate" phrasing for the PGVWC (C^j,D^j) boundary comparison with "cut-adapted coordinates" everywhere else in this note (lines 247, 258, 286) and in the Lean docstring and blueprint. But this line still calls (\beta,\rho) "local word coordinates," and the immediately preceding line (498) was just changed to "The cut-adapted (C^j,D^j) route." Using two different labels for the same (\beta,\rho) objects within one paragraph undercuts the internal consistency the PR is establishing, which the paper-gap policy (docs/paper-gaps/policy.tex, "Shared commands"/coherence) asks notes to maintain.

Suggested alignment:

Suggested change
The words \(\beta\) and \(\rho\) are local word coordinates introduced after
The words \(\beta\) and \(\rho\) are cut-adapted coordinates introduced after

The rest of the sentence — "they reindex the source end-site comparison (i_1,i_{m+1}) by blocked words, and are not additional hypotheses or terminology from the paper" — already carries the not-source-notation disclaimer and can stay.

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Incomplete terminology pass: line 498 was changed to "The cut-adapted (C^j,D^j) route," but this line still calls the same objects (\beta,\rho) "local word coordinates." Within a single paragraph (lines 498–503), the two adjacent sentences now use inconsistent labels for the identical mathematical objects. The paper-gap policy (docs/paper-gaps/policy.tex, §4 "Shared commands"/coherence) expects internal consistency within a note.

Suggested fix: change "local word coordinates" to "cut-adapted coordinates" to match line 498. The rest of the sentence already carries the not-source-notation disclaimer and can remain unchanged.

opening and blocking the cyclic boundary comparison; they reindex the source
Expand Down
Loading