The equality (zeroness) problem is decidable for Hadamard automata over a finite alphabet (paper §5). The orbit-ideal chain $I_n$ stabilises by Hilbert's basis theorem ($orbitIdeal_stabilises$), and the stabilised ideal is a bi-ideal, so the zeroness of the recognised series is characterised by the finite statement $∀ p ∈ orbitSet A N, p ∈ K A$ ($zeroness_iff_orbitSet$). The kernel $K A$ is finitely generated ($gensKer$, by Noetherianity), so this finite statement is a batch of ideal-membership queries $p ∈ span ↑(gensKer A)$, each decided by $IdealMembershipDecidable$; the decision $d$ is the Boolean "and" of these queries over the (finite) orbit set.