Diagonal units propagate around a cycle
Abstract
Two adjacent standard diagonal units in the real cycle algebra force every matrix unit, scalar complex commutants, and only the two scalar orthogonal symmetries.
Let L be any natural number at least three, with sites in Fin L and addition taken modulo L. Let A be the ordinary simple-cycle adjacency matrix, Delta its graph Laplacian, and V = Matrix.diagonal v for an arbitrary real potential v. Every vertex has two distinct neighbours, including on the triangle, so Delta = 2I - A. Write B = Algebra.adjoin real {Delta,V}, the real unital matrix algebra generated by those two matrices. The same algebra is generated by A and V. Write E(i,k) = Matrix.single i k 1 and C(M) = M.map Complex.ofReal for the entrywise complex image of a real matrix.
Theorem 1.1 (Two adjacent diagonal units imply full algebra).
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Walks/CycleDiagonalUnitPropagation.cycle_diagonal_units_full (✓ std3). ∎
Source. Repository-derived.
Commentary.
Assume E(j,j) and E(j+1,j+1) belong to B for some cyclic site j. If E(k-1,k-1) and E(k,k) belong to B, put Q = I - E(k-1,k-1). The column A E(k,k) is E(k-1,k) + E(k+1,k), and the corresponding row is E(k,k-1) + E(k,k+1). Multiplying by Q removes the k-1 component. Hence Q A E(k,k) and E(k,k) A Q are E(k+1,k) and E(k,k+1), whose product is E(k+1,k+1). All operations remain inside the real algebra. Induction in the number of cyclic steps starting at j gives every diagonal unit, without a bound on L.
For every graph edge from i to k, E(i,i) A E(k,k) = E(i,k). A walk from i to k exists because the cycle is connected. The successive edge units multiply to E(i,k), with the length-zero walk giving E(i,i). Thus every standard matrix unit belongs to B. Expanding an arbitrary real matrix as the finite sum of its entries times E(i,k) gives B = the full real matrix algebra.
Entrywise complexification is a real algebra homomorphism. A complex matrix commuting with C(Delta) and C(V) therefore commutes with the image of every element of B, in particular every complex standard unit. Matrix.mem_range_scalar_iff_commute_single’ gives X = cI. Applying this to the complex image of a real orthogonal O and taking real parts gives O = aI with a real. Orthogonality gives a squared equal to one, so O is I or minus I. No distinct-value, generic-potential or two-valued-potential assumption is imposed.