A noncommutative arithmetic formula is a rooted tree whose leaves are variables or scalars
and whose binary gates perform addition or ordered multiplication. It computes a polynomial
in the free associative algebra: its monomials
are ordered words rather than commutative products. Size counts all vertices,
including scalar leaves, and subexpressions are not shared.
Matrix substitution sends a scalar 
to 
.
For example, 
vanishes under every scalar
substitution but can be nonzero under matrix
substitution.
A noncommutative rational formula additionally permits unary inverse gates. At a matrix tuple, evaluation is defined only when every inverse
operand is invertible. Over 
, call such a formula admissible if it has a defined rational
matrix evaluation of some positive dimension.
It is nonzero if at least
one defined evaluation is nonzero. Equivalent algebraic expressions can have different evaluation
domains.
