← All papers
First page of Uniform adjacency-degree probes from differential rigidity

Uniform adjacency-degree probes from differential rigidity

Zhipeng Lu

math.CO Oct 11, 2026 · v1
Provides Lean 4/Mathlib proof-audit sources for the spanning-probe and tree-invariant constructions, plus checks that a Python emitter matches the Lean instruction arrays.
We construct a fixed triangular family of noncommutative polynomials that spans the joint cyclic module of a real symmetric pair from any prescribed vector. In dimension at most $N$, when the second matrix has spectral diameter at most $N-1$, the family has $N(N+1)/2$ members, degree at most $N-1$, and a shared arithmetic circuit of size $O(N^2)$. No rank-dependent choice of coefficients is made. The proof uses a rational differential connection with a small self-adjoint residue: a primitive polynomial exterior vector for an invariant subspace must have an integer degree smaller than one. For connected trees, the probes and the pointed adjacency–degree reconstruction theorem give one explicit self-adjoint polynomial $p_N\in\mathbb{Z}\langle a,d\rangle$ whose trace separates all trees of order at most $N$. Its circuit has $O(N^2)$ gates, formal degree at most $3N-2$, and polynomial bit complexity. Only the original adjacency and degree matrices, the identity, and ordinary matrix arithmetic are used. A separate integer sum-of-squares construction gives a fixed positive semidefinite representative on which the all-one vector is cyclic; its degree is $O(N^2)$. A linear trace-degree lower bound shows that the first construction has the correct asymptotic degree scale.

Can a small fixed family of noncommutative polynomials span the joint cyclic module of a real symmetric matrix pair from any seed vector, without input-dependent basis selection? Applied to trees, this asks whether there is a single explicit polynomial in the adjacency and degree matrices whose trace separates all trees of bounded order.

A triangular integer recurrence defines N(N+1)/2 polynomials of degree at most N-1, computed by a shared O(N^2) circuit. Their spanning property is proved through a rational differential connection with small self-adjoint residue: an invariant subspace must be constant, because a primitive exterior vector would otherwise have integer degree below one. Gram tables built from the probes, together with a pointed adjacency–degree reconstruction theorem, yield a single trace polynomial. The authors also give Lean 4/Mathlib proof-audit sources, with checks of the Python emitter against the Lean instruction arrays for N=1..15.

The construction gives an explicit self-adjoint p_N in Z<a,d> with O(N^2) gates and degree at most 3N-2 whose trace separates all trees of order at most N. A separate integer sum-of-squares representative has degree O(N^2). A spider-tree lower bound shows that linear degree is necessary.