Proof of `Multivariate polynomial recursive sequences`
What this proof establishes
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
The polyrec consistency problem is decidable (paper §5.4): the decision reduces to checking that all components of the companion Hadamard automaton's recognised series are commutative, each decided by (the meta-theorem applied to the effective prevariety of Hadamard-finite series).