Native operators and bounds for the equal-spin diamond

Abstract

Native normalized spin operators on four complete complex factors satisfy weight invariance, singlet isotropy and a uniform pair-order bound.

Let S be a natural number. Each of the four factors is the complete complex spin-S space with orthonormal basis indexed by W(S) = Fin(2S+1). Index r has weight S−r; the native normalized raising matrix Jplus(2S) has coefficient √((r+1)(2S−r)) from r+1 to r, with zero endpoint, and lowering is its adjoint. Put C(S) = Fin(4) → W(S), V(S) = C(S) → ℂ and O(S) = Matrix(C(S),C(S),ℂ). Norms are the Euclidean norms and inner products conjugate the first argument. Matrices act on every complex superposition in V(S). Sites 0,1,2,3 correspond to vertices 1,2,3,4. A submodule infimum denotes intersection; bottom is the zero submodule.

Definition 1.1 (An operator at one site).

$$\forall (S:\mathbb{N}),(\forall (i:\mathrm{Fin}\left(4\right)),(\forall (A:\mathrm{Matrix}\left(W\left(S\right),W\left(S\right),\mathbb{C}\right)),(\forall (x:C\left(S\right)),(\forall (y:C\left(S\right)),(\mathrm{site}\left(S,i,A,x,y\right)=A\left(x\left(i\right),y\left(i\right)\right)\cdot \mathrm{prodExcept}\left(i,x,y\right))))))$$

Formalization. D5/S3/Quantum/SpinChains/DiamondSpinBounds.site (✓ std3).

Source. Repository-derived.

Commentary.

prodExcept(i,x,y) is the product of Kronecker deltas δ(xⱼ,yⱼ) over the three sites j≠i. Thus site is exactly the tensor placement of A with identities on all other factors.

Definition 1.2 (The raising operator at a site).

$$\forall (S:\mathbb{N}),(\forall (i:\mathrm{Fin}\left(4\right)),(\mathrm{raising}\left(S,i\right)=\mathrm{site}\left(S,i,\mathrm{Jplus}\left(2\cdot S\right)\right)))$$

Formalization. D5/S3/Quantum/SpinChains/DiamondSpinBounds.raising (✓ std3).

Source. Repository-derived.

Commentary.

This is the normalized native raising matrix on the full factor.

Definition 1.3 (The lowering operator at a site).

$$\forall (S:\mathbb{N}),(\forall (i:\mathrm{Fin}\left(4\right)),(\mathrm{lowering}\left(S,i\right)=\mathrm{site}\left(S,i,(\mathrm{Jplus}\left(2\cdot S\right){)}^{\ast }\right)))$$

Formalization. D5/S3/Quantum/SpinChains/DiamondSpinBounds.lowering (✓ std3).

Source. Repository-derived.

Commentary.

The adjoint convention includes both ladder endpoints.

Definition 1.4 (The five edges).

$$\mathrm{edges}=\mathrm{finset}\left((0,1),(0,2),(0,3),(1,2),(1,3)\right)$$

Formalization. D5/S3/Quantum/SpinChains/DiamondSpinBounds.edges (✓ std3).

Source. Repository-derived.

Commentary.

Each listed unordered edge is included once. The absent edge is (2,3); there are no loops or additional coefficients.

Definition 1.5 (The diamond Hamiltonian).

$$\forall (S:\mathbb{N}),(\mathrm{hamiltonian}\left(S\right)=\sum _{(i,j)\in \mathrm{edges}}2\cdot (X\left(i\right)\cdot X\left(j\right)+Y\left(i\right)\cdot Y\left(j\right)))$$

Formalization. D5/S3/Quantum/SpinChains/DiamondSpinBounds.hamiltonian (✓ std3).

Source. Repository-derived.

Commentary.

Writing Xᵢ=site(S,i,Jx(2S)) and Yᵢ=site(S,i,Jy(2S)), this is 2Σedges(XᵢXⱼ+YᵢYⱼ). The native Cartesian identity proves it equals Σedges(Jᵢ⁺Jⱼ⁻+Jᵢ⁻Jⱼ⁺), with coefficient +1 on each of the five edges. Operators at distinct sites commute, so the Hamiltonian is Hermitian.

Definition 1.6 (Total raising).

$$\forall (S:\mathbb{N}),(\mathrm{totalRaising}\left(S\right)=\sum _{i\in \mathrm{Fin}\left(4\right)}\mathrm{raising}\left(S,i\right))$$

Formalization. D5/S3/Quantum/SpinChains/DiamondSpinBounds.totalRaising (✓ std3).

Source. Repository-derived.

Commentary.

The sum runs over all four sites.

Definition 1.7 (Total lowering).

$$\forall (S:\mathbb{N}),(\mathrm{totalLowering}\left(S\right)=\sum _{i\in \mathrm{Fin}\left(4\right)}\mathrm{lowering}\left(S,i\right))$$

Formalization. D5/S3/Quantum/SpinChains/DiamondSpinBounds.totalLowering (✓ std3).

Source. Repository-derived.

Commentary.

This is the adjoint of total raising.

Definition 1.8 (Total weight).

$$\forall (S:\mathbb{N}),(\mathrm{totalWeight}\left(S\right)=\sum _{i\in \mathrm{Fin}\left(4\right)}\mathrm{site}\left(S,i,\mathrm{Jz}\left(2\cdot S\right)\right))$$

Formalization. D5/S3/Quantum/SpinChains/DiamondSpinBounds.totalWeight (✓ std3).

Source. Repository-derived.

Commentary.

At configuration x its diagonal entry is 4S−Σᵢxᵢ. The Hamiltonian commutes with total weight.

Definition 1.9 (The entire singlet space).

$$\forall (S:\mathbb{N}),(\mathrm{singletSpace}\left(S\right)=\inf \left(\ker \left(\mathrm{totalRaising}\left(S\right)\right),\ker \left(\mathrm{totalLowering}\left(S\right)\right)\right))$$

Formalization. D5/S3/Quantum/SpinChains/DiamondSpinBounds.singletSpace (✓ std3).

Source. Repository-derived.

Commentary.

Both kernels are taken on V(S). No pair-coupling sector or multiplicity is selected. The total ladder commutator implies that every vector here has total weight zero.

Definition 1.10 (The entire zero-weight space).

$$\forall (S:\mathbb{N}),(\mathrm{zeroWeightSpace}\left(S\right)=\ker \left(\mathrm{totalWeight}\left(S\right)\right))$$

Formalization. D5/S3/Quantum/SpinChains/DiamondSpinBounds.zeroWeightSpace (✓ std3).

Source. Repository-derived.

Commentary.

It consists exactly of vectors supported on configurations Z(S) with Σᵢxᵢ=4S. These coordinate vectors form an orthonormal basis of the entire kernel. The middle configuration xᵢ=S belongs to Z(S), including at S=0.

Definition 1.11 (The actual Hermitian restriction).

$$\forall (S:\mathbb{N}),(\forall (x:Z\left(S\right)),(\forall (y:Z\left(S\right)),(\mathrm{restrictedHamiltonian}\left(S,x,y\right)=\mathrm{hamiltonian}\left(S,\mathrm{val}\left(x\right),\mathrm{val}\left(y\right)\right))))$$

Formalization. D5/S3/Quantum/SpinChains/DiamondSpinBounds.restrictedHamiltonian (✓ std3).

Source. Repository-derived.

Commentary.

Z(S) is the subtype of C(S) just described. Invariance of zero weight identifies this submatrix with the genuine restricted operator, including its action, inner product and eigenvectors.

Definition 1.12 (The weight operator at a site).

$$\forall (S:\mathbb{N}),(\forall (i:\mathrm{Fin}\left(4\right)),(z\left(S,i\right)=\mathrm{site}\left(S,i,\mathrm{Jz}\left(2\cdot S\right)\right)))$$

Formalization. D5/S3/Quantum/SpinChains/DiamondSpinBounds.z (✓ std3).

Source. Repository-derived.

Commentary.

At configuration x the diagonal entry is S−xᵢ.

Definition 1.13 (The transverse pair operator).

$$\forall (S:\mathbb{N}),(\forall (i:\mathrm{Fin}\left(4\right)),(\forall (j:\mathrm{Fin}\left(4\right)),(\mathrm{xy}\left(S,i,j\right)=\mathrm{raising}\left(S,i\right)\cdot \mathrm{lowering}\left(S,j\right)+\mathrm{lowering}\left(S,i\right)\cdot \mathrm{raising}\left(S,j\right))))$$

Formalization. D5/S3/Quantum/SpinChains/DiamondSpinBounds.xy (✓ std3).

Source. Repository-derived.

Commentary.

Both ladder products act on the complete four-factor carrier.

Definition 1.14 (The vertical pair operator).

$$\forall (S:\mathbb{N}),(\forall (i:\mathrm{Fin}\left(4\right)),(\forall (j:\mathrm{Fin}\left(4\right)),(\mathrm{zz}\left(S,i,j\right)=z\left(S,i\right)\cdot z\left(S,j\right))))$$

Formalization. D5/S3/Quantum/SpinChains/DiamondSpinBounds.zz (✓ std3).

Source. Repository-derived.

Commentary.

For distinct sites this is their commuting weight product.

Definition 1.15 (The isotropic pair operator).

$$\forall (S:\mathbb{N}),(\forall (i:\mathrm{Fin}\left(4\right)),(\forall (j:\mathrm{Fin}\left(4\right)),(\mathrm{dot}\left(S,i,j\right)=\frac{1}{2}\cdot \mathrm{xy}\left(S,i,j\right)+\mathrm{zz}\left(S,i,j\right))))$$

Formalization. D5/S3/Quantum/SpinChains/DiamondSpinBounds.dot (✓ std3).

Source. Repository-derived.

Commentary.

This is XᵢXⱼ+YᵢYⱼ+ZᵢZⱼ. The native pair bound holds for every distinct pair.

Definition 1.16 (The isotropic diamond sum).

$$\forall (S:\mathbb{N}),(\mathrm{isotropic}\left(S\right)=\sum _{(i,j)\in \mathrm{edges}}\mathrm{dot}\left(S,i,j\right))$$

Formalization. D5/S3/Quantum/SpinChains/DiamondSpinBounds.isotropic (✓ std3).

Source. Repository-derived.

Commentary.

All five coefficient-one edges are present.

Definition 1.17 (The vertical diamond sum).

$$\forall (S:\mathbb{N}),(\mathrm{vertical}\left(S\right)=\sum _{(i,j)\in \mathrm{edges}}\mathrm{zz}\left(S,i,j\right))$$

Formalization. D5/S3/Quantum/SpinChains/DiamondSpinBounds.vertical (✓ std3).

Source. Repository-derived.

Commentary.

This is the diagonal sum over exactly the same five edges.

Definition 1.18 (The homogeneous complex quadratic form).

$$\forall (S:\mathbb{N}),(\forall (v:V\left(S\right)),(\forall (A:O\left(S\right)),(\mathrm{expect}\left(v,A\right)=\mathrm{inner}\left(v,A\cdot v\right))))$$

Formalization. D5/S3/Quantum/SpinChains/DiamondSpinBounds.expect (✓ std3).

Source. Repository-derived.

Commentary.

The inner product conjugates v in its first argument. No normalization is assumed.

Definition 1.19 (The middle configuration).

$$\forall (S:\mathbb{N}),(\forall (i:\mathrm{Fin}\left(4\right)),(\mathrm{middleConfiguration}\left(S,i\right)=S))$$

Formalization. D5/S3/Quantum/SpinChains/DiamondSpinBounds.middleConfiguration (✓ std3).

Source. Repository-derived.

Commentary.

Every coordinate is the basis index S, of local weight zero.

Definition 1.20 (The positive binomial product).

$$\forall (S:\mathbb{N}),(\forall (x:C\left(S\right)),(\mathrm{binomialProduct}\left(S,x\right)=\mathrm{ofReal}\left(\mathrm{binomialProductReal}\left(S,x\right)\right)))$$

Formalization. D5/S3/Quantum/SpinChains/DiamondSpinBounds.binomialProduct (✓ std3).

Source. Repository-derived.

Commentary.

It is the tensor product of the native binomial vectors at real parameter one.

Definition 1.21 (Its real coefficients).

$$\forall (S:\mathbb{N}),(\forall (x:C\left(S\right)),(\mathrm{binomialProductReal}\left(S,x\right)=\prod _{i\in \mathrm{Fin}\left(4\right)}\mathrm{sqrt}\left(\mathrm{choose}\left(2\cdot S,\mathrm{val}\left(x\left(i\right)\right)\right)\right)))$$

Formalization. D5/S3/Quantum/SpinChains/DiamondSpinBounds.binomialProductReal (✓ std3).

Source. Repository-derived.

Commentary.

Every coefficient is strictly positive, including at both endpoints.

Theorem 1.22 (Native spin relations and the whole-carrier pair bound).

$$\begin{array}{r}\forall (S:\mathbb{N}),((1\le S)\Rightarrow (\forall (i:\mathrm{Fin}\left(4\right)),(\forall (j:\mathrm{Fin}\left(4\right)),((i\ne j)\Rightarrow (\mathrm{PosSemidef}\left(\mathrm{ofNat}{\left(S\right)}^2\cdot 1-\mathrm{dot}\left(S,i,j\right)\right))))))\\ \forall (S:\mathbb{N}),(\forall (x:C\left(S\right)),(0<\mathrm{binomialProductReal}\left(S,x\right)))\\ \forall (S:\mathbb{N}),(\forall (x:C\left(S\right)),(\mathrm{binomialProduct}\left(S,x\right)=\mathrm{ofReal}\left(\mathrm{binomialProductReal}\left(S,x\right)\right)))\\ \forall (S:\mathbb{N}),(\forall (Q:O\left(S\right)),(\forall (A:O\left(S\right)),(\forall (B:O\left(S\right)),(\mathrm{comm}\left(Q,A\cdot B\right)=\mathrm{comm}\left(Q,A\right)\cdot B+A\cdot \mathrm{comm}\left(Q,B\right)))))\\ \forall (S:\mathbb{N}),(\mathrm{hamiltonian}\left(S\right)=\sum _{(i,j)\in \mathrm{edges}}(\mathrm{raising}\left(S,i\right)\cdot \mathrm{lowering}\left(S,j\right)+\mathrm{lowering}\left(S,i\right)\cdot \mathrm{raising}\left(S,j\right)))\\ \forall (S:\mathbb{N}),(\forall (i:\mathrm{Fin}\left(4\right)),(\forall (x:C\left(S\right)),(\left(\mathrm{lowering}\left(S,i\right)\cdot \mathrm{binomialProduct}\left(S\right)\right)\left(x\right)=\mathrm{ofNat}\left(\mathrm{val}\left(x\left(i\right)\right)\right)\cdot \mathrm{binomialProduct}\left(S,x\right))))\\ \forall (S:\mathbb{N}),(\forall (i:\mathrm{Fin}\left(4\right)),(\mathrm{comm}\left(\mathrm{totalLowering}\left(S\right),\mathrm{raising}\left(S,i\right)\right)=-2\cdot z\left(S,i\right)))\\ \forall (n:\mathbb{N}),((\mathrm{Jplus}\left(n\right){)}^{\ast }\cdot \mathrm{Jplus}\left(n\right)=\mathrm{diag}\left(r\mapsto \mathrm{ofNat}\left(\mathrm{val}\left(r\right)\right)\cdot \left(\mathrm{ofNat}\left(n\right)+1-\mathrm{ofNat}\left(\mathrm{val}\left(r\right)\right)\right)\right))\\ \forall (S:\mathbb{N}),(\forall (i:\mathrm{Fin}\left(4\right)),(\mathrm{comm}\left(\mathrm{totalLowering}\left(S\right),z\left(S,i\right)\right)=\mathrm{lowering}\left(S,i\right)))\\ \forall (S:\mathbb{N}),(\forall (i:\mathrm{Fin}\left(4\right)),(\forall (x:C\left(S\right)),(\left(\mathrm{raising}\left(S,i\right)\cdot \mathrm{binomialProduct}\left(S\right)\right)\left(x\right)=\left(2\cdot \mathrm{ofNat}\left(S\right)-\mathrm{ofNat}\left(\mathrm{val}\left(x\left(i\right)\right)\right)\right)\cdot \mathrm{binomialProduct}\left(S,x\right))))\\ \forall (n:\mathbb{N}),(\mathrm{Jplus}\left(n\right)\cdot (\mathrm{Jplus}\left(n\right){)}^{\ast }=\mathrm{diag}\left(r\mapsto \left(\mathrm{ofNat}\left(\mathrm{val}\left(r\right)\right)+1\right)\cdot \left(\mathrm{ofNat}\left(n\right)-\mathrm{ofNat}\left(\mathrm{val}\left(r\right)\right)\right)\right))\\ \forall (S:\mathbb{N}),(\mathrm{Hermitian}\left(\mathrm{restrictedHamiltonian}\left(S\right)\right))\\ \forall (S:\mathbb{N}),(\mathrm{singletSpace}\left(S\right)\subseteq \mathrm{zeroWeightSpace}\left(S\right))\\ \forall (S:\mathbb{N}),(\forall (v:V\left(S\right)),((v\in \mathrm{singletSpace}\left(S\right))\Rightarrow (\mathrm{expect}\left(v,\mathrm{hamiltonian}\left(S\right)\right)=\frac{4}{3}\cdot \mathrm{expect}\left(v,\mathrm{isotropic}\left(S\right)\right))))\\ \forall (S:\mathbb{N}),(\forall (i:\mathrm{Fin}\left(4\right)),(\forall (A:\mathrm{Matrix}\left(W\left(S\right),W\left(S\right),\mathbb{C}\right)),(\forall (v:V\left(S\right)),(\forall (x:C\left(S\right)),(\left(\mathrm{site}\left(S,i,A\right)\cdot v\right)\left(x\right)=\sum _{r\in W\left(S\right)}A\left(x\left(i\right),r\right)\cdot v\left(\mathrm{update}\left(x,i,r\right)\right))))))\\ \forall (S:\mathbb{N}),(\forall (i:\mathrm{Fin}\left(4\right)),(\forall (A:\mathrm{Matrix}\left(W\left(S\right),W\left(S\right),\mathbb{C}\right)),(\forall (B:\mathrm{Matrix}\left(W\left(S\right),W\left(S\right),\mathbb{C}\right)),(\mathrm{site}\left(S,i,A+B\right)=\mathrm{site}\left(S,i,A\right)+\mathrm{site}\left(S,i,B\right)))))\\ \forall (S:\mathbb{N}),(\forall (i:\mathrm{Fin}\left(4\right)),(\forall (A:\mathrm{Matrix}\left(W\left(S\right),W\left(S\right),\mathbb{C}\right)),((\mathrm{site}\left(S,i,A\right){)}^{\ast }=\mathrm{site}\left(S,i,(A{)}^{\ast }\right))))\\ \forall (S:\mathbb{N}),(\forall (i:\mathrm{Fin}\left(4\right)),(\forall (j:\mathrm{Fin}\left(4\right)),((i\ne j)\Rightarrow (\forall (A:\mathrm{Matrix}\left(W\left(S\right),W\left(S\right),\mathbb{C}\right)),(\forall (B:\mathrm{Matrix}\left(W\left(S\right),W\left(S\right),\mathbb{C}\right)),(\mathrm{site}\left(S,i,A\right)\cdot \mathrm{site}\left(S,j,B\right)=\mathrm{site}\left(S,j,B\right)\cdot \mathrm{site}\left(S,i,A\right)))))))\\ \forall (S:\mathbb{N}),(\forall (i:\mathrm{Fin}\left(4\right)),(\forall (A:\mathrm{Matrix}\left(W\left(S\right),W\left(S\right),\mathbb{C}\right)),(\forall (B:\mathrm{Matrix}\left(W\left(S\right),W\left(S\right),\mathbb{C}\right)),(\mathrm{site}\left(S,i,A\cdot B\right)=\mathrm{site}\left(S,i,A\right)\cdot \mathrm{site}\left(S,i,B\right)))))\\ \forall (S:\mathbb{N}),(\forall (i:\mathrm{Fin}\left(4\right)),(\forall (c:\mathbb{C}),(\forall (A:\mathrm{Matrix}\left(W\left(S\right),W\left(S\right),\mathbb{C}\right)),(\mathrm{site}\left(S,i,c\cdot A\right)=c\cdot \mathrm{site}\left(S,i,A\right)))))\\ \forall (S:\mathbb{N}),(\forall (i:\mathrm{Fin}\left(4\right)),(\forall (v:V\left(S\right)),(\forall (x:C\left(S\right)),(\left(z\left(S,i\right)\cdot v\right)\left(x\right)=\left(\mathrm{ofNat}\left(S\right)-\mathrm{ofNat}\left(\mathrm{val}\left(x\left(i\right)\right)\right)\right)\cdot v\left(x\right)))))\\ \forall (S:\mathbb{N}),(\forall (i:\mathrm{Fin}\left(4\right)),(z\left(S,i\right)=\mathrm{diag}\left(x\mapsto \mathrm{ofNat}\left(S\right)-\mathrm{ofNat}\left(\mathrm{val}\left(x\left(i\right)\right)\right)\right)))\\ \forall (S:\mathbb{N}),(\forall (v:V\left(S\right)),((v\in \mathrm{zeroWeightSpace}\left(S\right))\iff (\forall (x:C\left(S\right)),((\sum _{i\in \mathrm{Fin}\left(4\right)}\mathrm{val}\left(x\left(i\right)\right)\ne 4\cdot S)\Rightarrow (v\left(x\right)=0)))))\\ \forall (S:\mathbb{N}),(\forall (v:V\left(S\right)),((v\in \mathrm{zeroWeightSpace}\left(S\right))\Rightarrow (\mathrm{hamiltonian}\left(S\right)\cdot v\in \mathrm{zeroWeightSpace}\left(S\right))))\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/SpinChains/DiamondSpinBounds.native_relations (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed rows form one conjunction. In the two local ladder products diag maps r in Fin(n+1) to its displayed entry; in the site weight identity it maps x in C(S). The maps ofNat and ofReal embed scalars in the complex numbers. Write comm(A,B)=AB−BA and update(x,i,r) for replacement at site i. The conjunction records the exact site action, linearity, adjoints and commutation, the normalized ladder products, weight support and invariance, Hermiticity of the restriction, singlet expectation isotropy, and the pair order bound. Every spin, site, matrix and vector variable retains its full stated range.

A strictly positive product of binomial vectors is a Dᵢⱼ eigenvector of eigenvalue S². Adding S² times the identity to Dᵢⱼ gives an entrywise nonnegative matrix. The Perron comparison bound and the Hermitian spectral theorem yield Dᵢⱼ≤S²I for S≥1 on the whole complex carrier, with every coupling sector and multiplicity included.

Total-ladder commutators give ⟨v,Kv⟩=(4/3)⟨v,Iv⟩ for every singlet. This is an expectation identity; no vector equation Kv=(4/3)Iv is asserted. Both total ladders imply zero total weight, and weight invariance identifies the displayed submatrix with the complete Hermitian restriction.

References

• Truth anchor: D5/S3/Quantum/SpinChains/DiamondSpinBounds.binomialProduct
• Truth anchor: D5/S3/Quantum/SpinChains/DiamondSpinBounds.binomialProductReal
• Truth anchor: D5/S3/Quantum/SpinChains/DiamondSpinBounds.dot
• Truth anchor: D5/S3/Quantum/SpinChains/DiamondSpinBounds.edges
• Truth anchor: D5/S3/Quantum/SpinChains/DiamondSpinBounds.expect
• Truth anchor: D5/S3/Quantum/SpinChains/DiamondSpinBounds.hamiltonian
• Truth anchor: D5/S3/Quantum/SpinChains/DiamondSpinBounds.isotropic
• Truth anchor: D5/S3/Quantum/SpinChains/DiamondSpinBounds.lowering
• Truth anchor: D5/S3/Quantum/SpinChains/DiamondSpinBounds.middleConfiguration
• Truth anchor: D5/S3/Quantum/SpinChains/DiamondSpinBounds.native_relations
• Truth anchor: D5/S3/Quantum/SpinChains/DiamondSpinBounds.raising
• Truth anchor: D5/S3/Quantum/SpinChains/DiamondSpinBounds.restrictedHamiltonian
• Truth anchor: D5/S3/Quantum/SpinChains/DiamondSpinBounds.singletSpace
• Truth anchor: D5/S3/Quantum/SpinChains/DiamondSpinBounds.site
• Truth anchor: D5/S3/Quantum/SpinChains/DiamondSpinBounds.totalLowering
• Truth anchor: D5/S3/Quantum/SpinChains/DiamondSpinBounds.totalRaising
• Truth anchor: D5/S3/Quantum/SpinChains/DiamondSpinBounds.totalWeight
• Truth anchor: D5/S3/Quantum/SpinChains/DiamondSpinBounds.vertical
• Truth anchor: D5/S3/Quantum/SpinChains/DiamondSpinBounds.xy
• Truth anchor: D5/S3/Quantum/SpinChains/DiamondSpinBounds.z
• Truth anchor: D5/S3/Quantum/SpinChains/DiamondSpinBounds.zeroWeightSpace
• Truth anchor: D5/S3/Quantum/SpinChains/DiamondSpinBounds.zz
• Dependency: D5/S3/Combinatorics/Graph/PerronFrobenius/MCMCSupplier/LinearAlgebra/Matrix/PerronFrobenius/Dominance
• Dependency: D5/S3/Quantum/Contextuality/TemporalHardySpinAttainment
• Dependency: D5/S3/Quantum/Entanglement/PrecessionUniversalThresholdRefutation