Explicit matrix hitting points for noncommutative algebraic branching programs
Zhipeng Lu
math.RA
Oct 11, 2026 · v1
cs.CC math.CO
TL;DR
A Lean 4/Mathlib artifact verifies key results, including the rigidity lemma, hitting-point equivalences in both characteristic regimes, and recognizable-series substitution.
Abstract
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.
Problem
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.
Approach
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.
Results
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.