Cyclic tridiagonal determinants and transfer traces

Abstract

A cyclic Jacobi determinant and its two-dimensional transfer evolution.

Definition 1.1 (Cyclic tridiagonal matrix).

$$\forall R\in \mathrm{Type},[\mathrm{CommRing}\left(R\right)]\forall N\in \mathrm{Nat},\forall d\in \mathrm{Nat}\to R,\mathrm{cycleDiag}\left(N,d\right)=\mathrm{Matrix}.\mathrm{diagonal}\left(\lambda i:\mathrm{Fin}\left(N\right)\mapsto d\left(\mathrm{val}\left(i\right)\right)\right)-\mathrm{SimpleGraph}.\mathrm{adjMatrix}\left(\mathrm{SimpleGraph}.\mathrm{cycleGraph}\left(N\right),R\right)$$

Formalization. D5/S3/Combinatorics/SpectralGraph/CyclicTridiagonalTransferTrace.cycleDiag (✓ std3).

Source. Repository-derived.

Commentary.

The diagonal potential matrix minus the adjacency matrix of the cycle graph. The determinant identity concerns sizes at least three.

Theorem 1.2 (Entries of the cyclic matrix).

$$\forall R\in \mathrm{Type},[\mathrm{CommRing}\left(R\right)]\forall n\in \mathrm{Nat},\forall d\in \mathrm{Nat}\to R,\forall i\in \mathrm{Fin}\left(n+3\right),\forall j\in \mathrm{Fin}\left(n+3\right),\mathrm{cycleDiag}\left(n+3,d\right)\left(i,j\right)=\mathrm{if}(i=j)\mathrm{then}d\left(\mathrm{val}\left(i\right)\right)\mathrm{else}\mathrm{if}(\mathrm{Nat}.\mathrm{mod}\left(\mathrm{val}\left(i\right)+1,n+3\right)=\mathrm{val}\left(j\right)\vee \mathrm{Nat}.\mathrm{mod}\left(\mathrm{val}\left(j\right)+1,n+3\right)=\mathrm{val}\left(i\right))\mathrm{then}-(1)\mathrm{else}0$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/SpectralGraph/CyclicTridiagonalTransferTrace.cycleDiag_apply (✓ std3). ∎

Source. Repository-derived.

Commentary.

For sizes at least three, the diagonal entries are d, cyclic off-diagonal entries are minus one, and all remaining entries are zero.

Definition 1.3 (One transfer step).

$$\forall K\in \mathrm{Type},[\mathrm{Ring}\left(K\right)]\forall d\in K,\mathrm{transfer}\left(d\right)=\left(\begin{array}{cc}d& -(1)\\ 1& 0\end{array}\right)$$

Formalization. D5/S3/Combinatorics/SpectralGraph/CyclicTridiagonalTransferTrace.transfer (✓ std3).

Source. Repository-derived.

Commentary.

The two coordinates carry consecutive values of a second-order recurrence.

Definition 1.4 (Ordered transfer product).

$$\forall K\in \mathrm{Type},[\mathrm{Ring}\left(K\right)]\forall d\in \mathrm{Nat}\to K,\mathrm{evolution}\left(d,0\right)=1\wedge (\forall n\in \mathrm{Nat},\mathrm{evolution}\left(d,n+1\right)=\mathrm{transfer}\left(d\left(n\right)\right)\cdot \mathrm{evolution}\left(d,n\right))$$

Formalization. D5/S3/Combinatorics/SpectralGraph/CyclicTridiagonalTransferTrace.evolution (✓ std3).

Source. Repository-derived.

Commentary.

The recursion multiplies the next step on the left. The variable n in the successor branch is bound by that pattern.

Theorem 1.5 (Determinant of one step).

$$\forall R\in \mathrm{Type},[\mathrm{CommRing}\left(R\right)]\forall x\in R,\mathrm{Matrix}.\det \left(\mathrm{transfer}\left(x\right)\right)=1$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/SpectralGraph/CyclicTridiagonalTransferTrace.transfer_det (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every transfer step has determinant one; this also determines the determinant of a finite product.

Theorem 1.6 (Splitting the transfer evolution).

$$\forall K\in \mathrm{Type},[\mathrm{Ring}\left(K\right)]\forall d\in \mathrm{Nat}\to K,\forall n\in \mathrm{Nat},\forall k\in \mathrm{Nat},\mathrm{evolution}\left(d,n+k\right)=\mathrm{evolution}\left(\lambda i:\mathrm{Nat}\mapsto d\left(n+i\right),k\right)\cdot \mathrm{evolution}\left(d,n\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/SpectralGraph/CyclicTridiagonalTransferTrace.evolution_add (✓ std3). ∎

Source. Repository-derived.

Commentary.

Splitting a sequence after n steps puts the later k steps on the left.

Theorem 1.7 (Determinant of the evolution).

$$\forall R\in \mathrm{Type},[\mathrm{CommRing}\left(R\right)]\forall d\in \mathrm{Nat}\to R,\forall n\in \mathrm{Nat},\mathrm{Matrix}.\det \left(\mathrm{evolution}\left(d,n\right)\right)=1$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/SpectralGraph/CyclicTridiagonalTransferTrace.evolution_det (✓ std3). ∎

Source. Repository-derived.

Commentary.

Multiplicativity of the determinant and induction preserve determinant one.

Theorem 1.8 (The cyclic determinant identity).

$$\forall R\in \mathrm{Type},[\mathrm{CommRing}\left(R\right)]\forall n\in \mathrm{Nat},\forall d\in \mathrm{Nat}\to R,\mathrm{Matrix}.\det \left(\mathrm{cycleDiag}\left(n+3,d\right)\right)=\mathrm{Matrix}.\mathrm{trace}\left(\mathrm{evolution}\left(d,n+3\right)\right)-2$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/SpectralGraph/CyclicTridiagonalTransferTrace.cycleDiag_det_transfer (✓ std3). ∎

Source. Repository-derived.

Commentary.

Impulse solutions form a lower unitriangular matrix. Multiplication reduces all interior rows to coordinate rows and leaves a two by two boundary block. Its determinant is the negative cyclic determinant. The two impulse solutions also give the entries of the transfer product, whose determinant is one; the boundary determinant consequently equals two minus the trace. These identities hold over every commutative ring.

References

• Truth anchor: D5/S3/Combinatorics/SpectralGraph/CyclicTridiagonalTransferTrace.cycleDiag
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/CyclicTridiagonalTransferTrace.cycleDiag_apply
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/CyclicTridiagonalTransferTrace.cycleDiag_det_transfer
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/CyclicTridiagonalTransferTrace.evolution
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/CyclicTridiagonalTransferTrace.evolution_add
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/CyclicTridiagonalTransferTrace.evolution_det
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/CyclicTridiagonalTransferTrace.transfer
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/CyclicTridiagonalTransferTrace.transfer_det