Adjacent units from the actual defect geometry
Abstract
Actual sign geometry supplies adjacent diagonal matrix units for the Anderson defect family.
For natural r at least three and m at least two, put L=rm and q=(m-1)r+1. On Fin L let U(i)=-1 exactly when i modulo r is zero or i=q, and U(i)=1 otherwise. Let B be the real subalgebra generated by the actual cycleGraph L Laplacian and diag(U). Write E_jj for Matrix.single j j 1. Addition of site indices is cyclic.
Theorem 1.1 (The node and its successor lie on the cycle).
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Walks/AndersonDefectSeed.defect_bounds (✓ std3). ∎
Source. Repository-derived.
Commentary.
This arithmetic bound is a consumed auxiliary fact used in both the seed construction and the full-family theorem.
Theorem 1.2 (Two actual adjacent diagonal units belong to the generated algebra).
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Walks/AndersonDefectSeed.defect_diagonal_seed (✓ std3). ∎
Source. Repository-derived.
Commentary.
The negative-site projector N=(I-diag(U))/2 lies in B. Its compression of cycle adjacency is exactly E_pq+E_qp for p=(m-1)r and q=p+1, because these are the only adjacent negative sites. Squaring isolates E_pp+E_qq.
The positive projector P=(I+diag(U))/2 transports this pair along two actual positive runs. Removing each preceding frontier leaves the sum of the next two diagonal units. The run before p has length r-1 and the run after q has length r-2. At frontier r-1 one unit remains. Its unique negative neighbour supplies the adjacent unit. The proof includes the cyclic wrap and m=2 geometry.
The full-family theorem consumes this seed through the existing cycle_diagonal_units_full supplier. This module supplies the actual seed and does not repeat that propagation proof.