← All papers
First page of Explicit matrix hitting points for noncommutative algebraic branching programs

Explicit matrix hitting points for noncommutative algebraic branching programs

Zhipeng Lu

math.RA Oct 11, 2026 · v1 cs.CC math.CO
A Lean 4/Mathlib artifact verifies key results, including the rigidity lemma, hitting-point equivalences in both characteristic regimes, and recognizable-series substitution.
We give a deterministic polynomial-resource black-box identity test for noncommutative algebraic branching programs (ABPs), using ordinary matrix evaluations of the output polynomial. Given an alphabet of size $m\ge1$ and an ABP vertex bound $S\ge1$, we construct one fixed tuple of integer matrices of order $R=(m+2)d(d+1)/2$, where $d=(m+2)S$, with entry bit length $O(d\log(d+1))$. Every nonzero polynomial computed by an ABP with at most $S$ vertices has a nonzero evaluation at this tuple. The construction accesses neither the hidden ABP nor its intermediate gates. A rectangular variant improves the order to $O(m^{3/2}S^2)$. Matrix order, description length, and all returned entries are counted; the total resources are polynomial. The result holds in characteristic zero and in characteristic $p>\binom d2$. The main ingredient is a fixed polynomial frame spanning the joint cyclic module of every matrix tuple from every prescribed vector. A compensating block makes a tagged encoding nilpotent of index at most three, while preserving the original cyclic module. A differential exterior-vector argument then gives a single triangular recurrence with polynomially many outputs. Its shared left-linear circuit is converted into actual integer query matrices by coefficient duality. Two-sided pairing further gives deterministic nonadaptive reconstruction of an equivalent ABP from polynomially many output-only matrix queries. The same frame gives polynomial-cardinality explicit trace separators for simultaneous-conjugation orbit closures, and a fixed nilpotent substitution for bounded-dimensional recognizable series. The latter also tests rational formulas whose given syntax is defined at the scalar origin. We provide complete proofs, construction costs, and exact implementation checks.

Deterministic black-box polynomial identity testing for noncommutative algebraic branching programs has had only quasipolynomial hitting sets. The goal is a polynomial-resource test that uses ordinary matrix evaluations of the output polynomial.

A fixed polynomial frame spans the joint cyclic module of every matrix tuple from every seed vector. A compensating block makes a tagged encoding nilpotent, and a differential exterior-vector rigidity argument yields a triangular recurrence. Coefficient duality turns the recurrence into explicit integer query matrices. Parts of the proofs are machine-checked in Lean 4 with Mathlib, and a Python emitter performs exact implementation checks.

Explicit integer matrices of order (m+2)d(d+1)/2 hit every nonzero ABP of at most S vertices, over characteristic zero and characteristic p > C(d,2); a rectangular variant has order O(m^{3/2}S^2). Further consequences are deterministic reconstruction, trace separators for orbit closures, and identity tests for recognizable series. The Lean artifact verifies the hitting equivalences and related lemmas.