Weighted Legal-Path Temperley-Lieb Relations

Abstract

Finite symmetric weighted legal paths carry the exact local Temperley-Lieb projections.

Theorem 1.1 (Weighted path projections satisfy all four local relations).

$$\begin{array}{c}\forall L:\mathrm{Finite},R:L\to L\to \mathrm{Prop},\mathrm{Symmetric}(R),d:L\to \mathbb{R},0<\Delta ,\forall a\in L,0<d_a\wedge \sum _{b:R(a,b)}{d}_b=\Delta d_a,\forall n\in \mathbb{N},s,t\in L,\\ \mathrm{let}\mathrm{LegalPath}(R,n,s,t):Type=\{x:\mathrm{Fin}(n+1)\to L|x\left(0\right)=s\wedge \left(x\left(n\right)=t\wedge \left(\forall k\in \mathrm{Fin}(n),R\left(x\left(k\right),x\left(k+1\right)\right)\right)\right)\};\\ \mathrm{let}{P}_i:\mathrm{Matrix}(\mathrm{LegalPath}(R,n,s,t),\mathrm{LegalPath}(R,n,s,t),\mathbb{C}),i\in \mathbb{N},1\le i<n,\forall x\in \mathrm{LegalPath}(R,n,s,t),y\in \mathrm{LegalPath}(R,n,s,t),P_i\left(x,y\right)=(\{\begin{array}{ll}Complex.ofReal(\frac{\sqrt{d\left(x\left(i\right)\right)\cdot d\left(y\left(i\right)\right)}}{\Delta \cdot d\left(x\left(i-1\right)\right)})& \text{if}(\left(\forall k\in \mathrm{Fin}(n+1),k\ne i\Rightarrow x\left(k\right)=y\left(k\right)\right)\wedge x\left(i-1\right)=x\left(i+1\right))\\ 0& \text{otherwise}\end{array});\\ (\forall i,1\le i<n\Rightarrow \mathrm{conjTranspose}(P_i)=P_i\wedge P_i{P}_i=P_i)\wedge \\ (\forall i,1\le i,i+1<n\Rightarrow P_i{P}_{i+1}{P}_i={\Delta }^{-2}{P}_i)\wedge \\ (\forall i,j,1\le i<n,1\le j<n,i+2\le j\vee j+2\le i\Rightarrow P_i{P}_j=P_j{P}_i).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Algebra/WeightedLegalPathTemperleyLieb.weighted_legal_path_temperley_lieb (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let L be any finite label type and R a symmetric Boolean adjacency relation, including possible self-loops. Every label has a strictly positive real weight d, delta is strictly positive, and the sum of d(b) over R(a,b) equals delta times d(a) for every a. Fix any path length n and endpoints s,t. The path basis contains precisely the legal length-n paths from s to t and may be empty.

For every interior i, P_i(x,y) is zero unless x and y agree outside i and x at i-1 equals x at i+1. In the remaining case its literal FT.12 coefficient is the complex cast of sqrt(d(x_i) * d(y_i)) / (delta * d(x_(i-1))). This is the source’s square root of the product, with no rescaling or normalization of P_i.

The theorem establishes self-adjointness and idempotence at every interior index, the forward adjacent triple product whenever i+1 is interior, and commutation for both ordered cases of distance at least two. Its local replacement equivalence identifies a legal fiber with the neighbors of its common flank; the proof also establishes the adjacent unique survivor and the distant locality argument. No nonempty path-space premise is used.

References

• Truth anchor: D5/S3/Quantum/Algebra/WeightedLegalPathTemperleyLieb.weighted_legal_path_temperley_lieb